close quotes terminate comments

tools/Holmake/HolLex

@@ -37,22 +37,23 @@ and antiq
 and qdecl
   = QuoteAntiq of int * antiq
   | DefinitionLabel of int * string
+  | QuoteComment of int * int
 
 and qbody = QBody of {start: int, toks: qdecl list, stop: int}
 
 datatype token
   = Decl of decl * token option (* from INITIAL *)
   | CloseParen of int (* from INITIAL *)
   | QED of int (* from INITIAL *)
-  | EndTok of int (* from INITIAL, quote *)
-  | Comment (* from comment *)
+  | EndTok of int (* from INITIAL, quote, holcomment *)
+  | Comment of int (* from comment, holcomment *)
   | Antiq of antiq * token option (* from ANTIQ *)
   | StringEnd of int (* from string *)
   | HolStrLitEnd of int * string (* from holstrlit *)
-  | ProofLine of int * string (* from quote *)
-  | TerminationTok of int (* from quote *)
-  | QuoteEnd of int * string (* from quote *)
-  | FullQuoteEnd of int * string (* from quote *)
+  | ProofLine of int * string (* from quote, holcomment *)
+  | TerminationTok of int (* from quote, holcomment *)
+  | QuoteEnd of int * string (* from quote, holcomment *)
+  | FullQuoteEnd of int * string (* from quote, holcomment *)
   | QDecl of qdecl * token option (* from quote *)
   | EOF of int (* from every state *)
 
@@ -61,18 +62,26 @@ type lexresult = token
 datatype state = STATE of {
   parseError: int * int -> string -> unit,
   pardepth: int ref,
-  comdepth: int ref
+  comdepth: int ref,
+  comstart: (int * int) option ref
 }
 
 fun noDecls pos = Decls {start = pos, decls = [], stop = pos}
 
 exception Unreachable
 datatype 'a test_result = TestOk of 'a | TestBad | TestSkip
 
-fun parseQuoteBody (STATE {parseError, ...}) continue pos test = let
+fun forceCloseComment (STATE {parseError, comdepth, comstart, ...}) =
+  case !comstart of
+    SOME pos => (parseError pos "unterminated comment"; comdepth := 0; comstart := NONE)
+  | _ => ()
+
+fun parseQuoteBody (arg as STATE {parseError, ...}) continue pos test = let
   fun go buf lookahead = let
     val tk = case lookahead of SOME tk => tk | NONE => continue()
-    fun finish stop = QBody {start = #2 pos, toks = rev buf, stop = stop}
+    fun finish stop = (
+      forceCloseComment arg;
+      QBody {start = #2 pos, toks = rev buf, stop = stop})
     fun cont (p, t) strong =
       case test tk of
         TestBad =>
@@ -164,8 +173,8 @@ fun eof (_:state) = EOF
 
 %%
 %structure HolLex
-%s string stringlbrk comment quote holstrlit holstrlitlbrk ANTIQ;
-%arg (UserDeclarations.STATE {pardepth, comdepth, parseError});
+%s string stringlbrk comment holcomment quote holstrlit holstrlitlbrk ANTIQ;
+%arg (UserDeclarations.STATE {pardepth, comdepth, comstart, parseError});
 %full
 %posarg
 %eofpos
@@ -215,7 +224,7 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]
 <INITIAL>"(*" => (
   comdepth := 1; YYBEGIN comment;
   case continue() of
-    Comment => (YYBEGIN INITIAL; continue())
+    Comment _ => (YYBEGIN INITIAL; continue())
   | EOF p => (parseError (yypos, yyend) "unterminated comment"; EOF p)
   | _ => raise Unreachable
 );
@@ -325,8 +334,9 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]
 
 <stringlbrk>"\\" => (YYBEGIN string; continue());
 
-<comment>"(*" => (inc comdepth; continue());
-<comment>"*)" => (dec comdepth; if !comdepth < 1 then Comment else continue());
+<comment,holcomment>"(*" => (inc comdepth; continue());
+<comment,holcomment>"*)" =>
+  (dec comdepth; if !comdepth < 1 then (comstart := NONE; Comment yyend) else continue());
 <comment>[^\n()*]{1,10} => (continue());
 
 <quote>{ProofLine} => (ProofLine (yypos, yytext));
@@ -351,16 +361,15 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]
   val n = yypos + #2 (Substring.base ss)
   in QDecl (DefinitionLabel (n, Substring.string ss), NONE) end);
 <quote>"(*" => (
-  comdepth := 1; YYBEGIN comment;
+  comdepth := 1; comstart := SOME (yypos, yyend); YYBEGIN holcomment;
   case continue() of
-    Comment => (YYBEGIN quote; continue())
-  | EOF p => (parseError (yypos, yyend) "unterminated comment"; EOF p)
-  | _ => raise Unreachable
+    Comment stop => (YYBEGIN quote; QDecl (QuoteComment (yypos, stop), NONE))
+  | tk => tk
 );
-<quote>{quoteend} => (QuoteEnd (yypos, yytext));
-<quote>{newline}"End" => (EndTok (yyend-3));
-<quote>{newline}"Termination" => (TerminationTok (yyend-11));
-<quote>{fullquoteend} => (FullQuoteEnd (yypos, yytext));
+<quote,holcomment>{quoteend} => (QuoteEnd (yypos, yytext));
+<quote,holcomment>{newline}"End" => (EndTok (yyend-3));
+<quote,holcomment>{newline}"Termination" => (TerminationTok (yyend-11));
+<quote,holcomment>{fullquoteend} => (FullQuoteEnd (yypos, yytext));
 <quote>"^" => (
   YYBEGIN ANTIQ;
   case continue() of

tools/Holmake/HolParser.sml

@@ -24,7 +24,7 @@ in
 
   fun mkParser {read, parseError, pos} = let
     val lex = HolLex.makeLexer (read, pos) (H.STATE {
-      comdepth = ref 0, pardepth = ref 0, parseError = parseError})
+      comdepth = ref 0, comstart = ref NONE, pardepth = ref 0, parseError = parseError})
     val lookahead = ref NONE
     fun go () =
       case (case !lookahead of SOME tk => tk | NONE => lex ()) of
@@ -342,6 +342,7 @@ structure ToSML = struct
           aux ",local]")
     fun doQuoteCore start ds stop f = case ds of
         [] => quote (start, stop)
+      | QuoteComment _ :: rest => doQuoteCore start rest stop f
       | QuoteAntiq (_, BadAntiq _) :: rest => doQuoteCore start rest stop f
       | QuoteAntiq (p, Ident (idstart, id)) :: rest => (
         quote (start, p);
@@ -363,20 +364,20 @@ structure ToSML = struct
         | SOME g => (quote (start, p); g l; doQuoteCore (p + size t) rest stop f)
     and doQuote (QBody {start, toks, stop}) =
       (aux "[QUOTE \""; doQuoteCore start toks stop NONE; aux "\"]")
-    and doQuoteConj (QBody {start, toks, stop}) f = (
-      aux "[QUOTE \"(";
-      case toks of
-        DefinitionLabel (l as (p, t)) :: rest => let
-        val _ = locpragma start
-        val first = ref true
-        fun strcode1 (p as (_, s)) = (
-          if !first then first := Substring.isEmpty (Substring.dropl Char.isSpace s) else ();
-          strcode0 p)
-        val _ = wrap strcode1 (start, p)
-        val _ = f (!first) l
-        in doQuoteCore (p + size t) rest stop (SOME (f false)) end
-      | _ => doQuoteCore start toks stop (SOME (f false));
-      aux ")\"]")
+    and doQuoteConj (QBody {start, toks, stop}) f = let
+      val first = ref true
+      val strcode1 = wrap (fn (p as (_, s)) => (
+        if !first then first := Substring.isEmpty (Substring.dropl Char.isSpace s) else ();
+        strcode0 p))
+      fun doQuote0 start toks =
+        case toks of
+          DefinitionLabel (l as (p, t)) :: rest => (
+          strcode1 (start, p); f (!first) l;
+          doQuoteCore (p + size t) rest stop (SOME (f false)))
+        | QuoteComment (p, stop) :: rest =>
+          (strcode1 (start, p); strcode (p, stop); doQuote0 stop rest)
+        | _ => doQuoteCore start toks stop (SOME (f false))
+      in aux "[QUOTE \"("; locpragma start; doQuote0 start (PolyML.print toks); aux ")\"]" end
     and doDecl eager pos d = case d of
         DefinitionDecl {head = (p, head), quote, termination, stop, ...} => let
         val {keyword, name, attrs, name_attrs} = parseDefinitionPfx head

tools/Holmake/tests/quote-filter/expected-mosml

@@ -4,7 +4,7 @@
 [QUOTE " (*#loc 4 2*)foo = #\"^`\""]
 [QUOTE " (*#loc 5 2*)\"\\\"\""]
 (Parse.Term [QUOTE " (*#loc 6 3*)\009"])
-(Parse.Term [QUOTE " (*#loc 7 3*)(* foo *)"])
+(Parse.Term [QUOTE " (*#loc 7 3*)(* foo"])
 [QUOTE " (*#loc 8 2*)^^"]
 "\"" (Parse.Term [QUOTE " (*#loc 9 8*)foo"])
 "\\" [QUOTE " (*#loc 10 7*)foo"]
@@ -24,7 +24,8 @@
 [QUOTE " (*#loc 24 2*)", ANTIQUOTE (fromMLnum nm), QUOTE " (*#loc 24 17*) (* *) "];
 (* (*  *) `;*)
 
-val (even_rules,even_ind,even_cases) = IndDefLib.xHol_reln "even" [QUOTE "( (*#loc 27 16*)\n\
+val (even_rules,even_ind,even_cases) = IndDefLib.xHol_reln "even" [QUOTE "( (*#loc 27 16*)[...]
+\n\
 \ (*#loc 28 12*) even 0\n\
 \) /\\ ( (*#loc 29 5*) (!n. even n ==> odd (n + 1))\n\
 \) /\\ ( (*#loc 30 12*)\n\
@@ -35,9 +36,10 @@ val foo = TotalDefn.qDefine "foo" [QUOTE " (*#loc 34 16*)\n\
 \  foo x = if x < 2 then 1 else x * foo (x - 1)\n\
 \"] NONE; val foo_ind = DB.fetch "-" "foo_ind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;;
 
-val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = IndDefLib.xHol_reln "compile_rel" [QUOTE "( (*#loc 38 23*)\n\
+val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = IndDefLib.xHol_reln "compile_rel" [QUOTE "( (*#loc 38 23*)[...]
+\n\
 \  (* (*  *) *)\n\
-\) /\\ ( (*#loc 40 8*)\n\
+\ (*#loc 40 8*)\n\
 \  compile_rel foo bar\n\
 \) /\\ ( (*#loc 42 8*)\n\
 \  compile_rel foo bar\n\
@@ -61,15 +63,17 @@ val sexpPEG_start = boolLib.save_thm("sexpPEG_start[simp]", SIMP_CONV(srw_ss())[
 );val _ = bossLib.Datatype [QUOTE " (*#loc 61 11*) foo = bar\n\
 \"];
 
-val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 64 16*)\n\
+val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 64 16*)[...]
+\n\
 \   !x y. x < y ==> reln (x + 1) y\n\
 \) /\\ ( (*#loc 66 5*)\n\
 \   !x y. reln x y ==> reln y x\n\
 \) /\\ ( (*#loc 68 9*)\n\
 \   !x. reln x 0\n\
-\)"]; val reln_strongind = DB.fetch "-" "reln_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 2 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
+\)"]; val reln_strongind = DB.fetch "-" "reln_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 3 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
-val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 72 16*)\n\
+val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 72 16*)[...]
+\n\
 \ (*#loc 73 10*) !x y. x < y ==> reln (x + 1) y\n\
 \) /\\ ( (*#loc 74 8*)\n\
 \   (!x y. reln x y ==> reln y x) /\\\n\
@@ -87,13 +91,9 @@ val thmname = boolLib.save_thm("thmname", expression
 );val _ = bar_x [QUOTE " (*#loc 87 13*)\n\
 \  another quotation (* with unfinished comment\n\
 \  and bare \" with ^foo and ^\n\
-\End\n\
-\\n\
-\Quote another_one:\n\
-\  jk this is the end of the comment *)\n\
 \"];
 
-val x = 91 + 10;
+val x = 92 + 10;
 val   y = 11
-val s = ""
+val s = ""  
 val s' = "foo.sml" (* #(FNAME) *)

tools/Holmake/tests/quote-filter/expected-poly

@@ -4,7 +4,7 @@
 [QUOTE " (*#loc 4 2*)foo = #\"^`\""]
 [QUOTE " (*#loc 5 2*)\"\\\"\""]
 (Parse.Term [QUOTE " (*#loc 6 3*)\009"])
-(Parse.Term [QUOTE " (*#loc 7 3*)(* foo *)"])
+(Parse.Term [QUOTE " (*#loc 7 3*)(* foo"])
 [QUOTE " (*#loc 8 2*)^^"]
 "\"" (Parse.Term [QUOTE " (*#loc 9 8*)foo"])
 "\\" [QUOTE " (*#loc 10 7*)foo"]
@@ -24,7 +24,8 @@
 [QUOTE " (*#loc 24 2*)", ANTIQUOTE (fromMLnum nm), QUOTE " (*#loc 24 17*) (* *) "];
 (* (*  *) `;*)
 
-val (even_rules,even_ind,even_cases) = IndDefLib.xHol_reln "even" [QUOTE "( (*#loc 27 16*)\n\
+val (even_rules,even_ind,even_cases) = IndDefLib.xHol_reln "even" [QUOTE "( (*#loc 27 16*)[...]
+\n\
 \ (*#loc 28 12*) even 0\n\
 \) /\\ ( (*#loc 29 5*) (!n. even n ==> odd (n + 1))\n\
 \) /\\ ( (*#loc 30 12*)\n\
@@ -35,9 +36,10 @@ val foo = TotalDefn.qDefine "foo" [QUOTE " (*#loc 34 16*)\n\
 \  foo x = if x < 2 then 1 else x * foo (x - 1)\n\
 \"] NONE; val _ = CompilerSpecific.quietbind "val foo_ind = DB.fetch \"-\" \"foo_ind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;";
 
-val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = IndDefLib.xHol_reln "compile_rel" [QUOTE "( (*#loc 38 23*)\n\
+val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = IndDefLib.xHol_reln "compile_rel" [QUOTE "( (*#loc 38 23*)[...]
+\n\
 \  (* (*  *) *)\n\
-\) /\\ ( (*#loc 40 8*)\n\
+\ (*#loc 40 8*)\n\
 \  compile_rel foo bar\n\
 \) /\\ ( (*#loc 42 8*)\n\
 \  compile_rel foo bar\n\
@@ -61,15 +63,17 @@ val sexpPEG_start = boolLib.save_thm("sexpPEG_start[simp]", SIMP_CONV(srw_ss())[
 );val _ = bossLib.Datatype [QUOTE " (*#loc 61 11*) foo = bar\n\
 \"];
 
-val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 64 16*)\n\
+val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 64 16*)[...]
+\n\
 \   !x y. x < y ==> reln (x + 1) y\n\
 \) /\\ ( (*#loc 66 5*)\n\
 \   !x y. reln x y ==> reln y x\n\
 \) /\\ ( (*#loc 68 9*)\n\
 \   !x. reln x 0\n\
-\)"]; val _ = CompilerSpecific.quietbind "val reln_strongind = DB.fetch \"-\" \"reln_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 2 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
+\)"]; val _ = CompilerSpecific.quietbind "val reln_strongind = DB.fetch \"-\" \"reln_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 3 reln_rules handle HOL_ERR _ => boolTheory.TRUTH);
 
-val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 72 16*)\n\
+val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 72 16*)[...]
+\n\
 \ (*#loc 73 10*) !x y. x < y ==> reln (x + 1) y\n\
 \) /\\ ( (*#loc 74 8*)\n\
 \   (!x y. reln x y ==> reln y x) /\\\n\
@@ -87,13 +91,9 @@ val thmname = boolLib.save_thm("thmname", expression
 );val _ = bar_x [QUOTE " (*#loc 87 13*)\n\
 \  another quotation (* with unfinished comment\n\
 \  and bare \" with ^foo and ^\n\
-\End\n\
-\\n\
-\Quote another_one:\n\
-\  jk this is the end of the comment *)\n\
 \"];
 
-val x = 91 + 10;
+val x = 92 + 10;
 val   y = 11
-val s = ""
+val s = ""  
 val s' = "foo.sml" (* #(FNAME) *)

tools/Holmake/tests/quote-filter/input

@@ -4,7 +4,7 @@
 `foo = #"^`"`
 `"\""`
 ``	``
-``(* foo *)``
+``(* foo``
 `^^`
 "\"" ``foo``
 "\\" `foo`
@@ -89,10 +89,6 @@ Quote bar_x:
   and bare " with ^foo and ^
 End
 
-Quote another_one:
-  jk this is the end of the comment *)
-End
-
 val x = #(LINE) + 10;
 val #(LINE=11) y = #(LINE)
 val s = #(FNAME) #(FNAME=foo.sml)