check formal comments recursively, within arbitrary cartouches (unknown sublanguages);

--- a/src/Pure/ML/ml_file.ML	Mon Jan 08 15:50:11 2018 +0100
+++ b/src/Pure/ML/ml_file.ML	Mon Jan 08 15:51:29 2018 +0100
@@ -18,6 +18,11 @@
     val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
     val provide = Resources.provide (src_path, digest);
     val source = Input.source true (cat_lines lines) (pos, pos);
+
+    val _ =
+      Thy_Output.check_comments (Toplevel.generic_theory_toplevel gthy)
+        (Input.source_explode source);
+
     val flags =
       {SML = SML, exchange = false, redirect = true, verbose = true,
         debug = debug, writeln = writeln, warning = warning};

--- a/src/Pure/PIDE/command.ML	Mon Jan 08 15:50:11 2018 +0100
+++ b/src/Pure/PIDE/command.ML	Mon Jan 08 15:51:29 2018 +0100
@@ -195,14 +195,19 @@
       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   else Toplevel.command_errors int tr st;
 
+fun check_error e =
+  (e (); []) handle exn =>
+    if Exn.is_interrupt exn then Exn.reraise exn
+    else Runtime.exn_messages exn;
+
 fun check_cmts span tr st' =
   Toplevel.setmp_thread_position tr
     (fn () =>
-      Outer_Syntax.side_comments span |> maps (fn cmt =>
-        (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
-          handle exn =>
-            if Exn.is_interrupt exn then Exn.reraise exn
-            else Runtime.exn_messages exn)) ();
+      (span |> maps (fn tok =>
+        check_error (fn () => Thy_Output.check_token_comments st' tok))) @
+      (Outer_Syntax.side_comments span |> maps (fn tok =>
+        check_error (fn () => Thy_Output.output_text st' {markdown = false} (Token.input_of tok)))))
+    ();
 
 fun report tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();

--- a/src/Pure/Thy/thy_output.ML	Mon Jan 08 15:50:11 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Jan 08 15:51:29 2018 +0100
@@ -25,6 +25,8 @@
   val integer: string -> int
   val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
   val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
+  val check_comments: Toplevel.state -> Symbol_Pos.T list -> unit
+  val check_token_comments: Toplevel.state -> Token.T -> unit
   val output_token: Toplevel.state -> Token.T -> Latex.text list
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
     Token.T list -> Latex.text list
@@ -305,6 +307,14 @@
   in output end
   handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
+fun check_comments state =
+  read_symbols_comment #> (Option.app o List.app) (fn (is_comment, syms) =>
+    (output_symbols_comment state {antiq = false} (is_comment, syms);
+     if is_comment then check_comments state syms else ()));
+
+fun check_token_comments state tok =
+  check_comments state (Input.source_explode (Token.input_of tok));
+
 end;