Tweak Quote-syntax's handling of ^ character

Bring it more in line with the handling of "normal" quotations. Closes #1313
HOL-Theorem-Prover · Sep 30, 2024 · b433fd5 · b433fd5
1 parent 8397f82
commit b433fd5
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 12 deletions.
diff --git a/tools/Holmake/QuoteFilter b/tools/Holmake/QuoteFilter
@@ -755,23 +755,19 @@ ProofLine =
 );
 <holstrlitlbrk> . => ((yypos, yytext));
 
-<quote,tmquote,tyquote,defnquote,datatypequote>"^"+{ws} => ((yypos, (ECHO yyarg yytext)));
-<quote,tmquote,tyquote,defnquote,datatypequote>"^"+{newline} => (
+<quote,tmquote,tyquote,defnquote,datatypequote,rawquote>"^"+{ws} => ((yypos, (ECHO yyarg yytext)));
+<quote,tmquote,tyquote,defnquote,datatypequote,rawquote>"^"+{newline} => (
   (yypos,
    if quotefix then yytext
    else ECHO yyarg (String.substring(yytext,0,size yytext - 1) ^
                     qnewline yyarg (yypos,yytext)))
 );
-<rawquote>"^"+{ws} => (
+<datatypequote,rawquote,defnquote>"^"+{newline}"End" => (
   (yypos,
-   if quotefix then yytext
-   else ECHO yyarg (String.substring(yytext,1,size yytext - 1)))
-);
-<rawquote>"^"+{ws} => (
-  (yypos,
-   if quotefix then yytext
-   else ECHO yyarg (String.substring(yytext,1,size yytext - 2) ^
-                    qnewline yyarg (yypos,yytext)))
+   (YYBEGIN INITIAL;
+    nextline yyarg (yypos + size yytext);
+    if quotefix then yytext
+    else String.substring(yytext,0,size yytext - 4) ^ "\"\n];"))
 );
 <quote,tmquote,tyquote,defnquote,datatypequote,rawquote>"^^" => (
   (yypos, if quotefix then yytext else ECHO yyarg "^")

diff --git a/tools/Holmake/tests/quote-filter/input b/tools/Holmake/tests/quote-filter/input
@@ -86,5 +86,5 @@ Theorem thmname = expression
 
 Quote bar_x:
   another quotation (* with unfinished comment 
-  and bare " with ^foo and ^^
+  and bare " with ^foo and ^
 End