just one check of formal comments;

--- a/src/Pure/PIDE/command.ML	Sat Feb 03 14:39:17 2018 +0100
+++ b/src/Pure/PIDE/command.ML	Sat Feb 03 15:34:22 2018 +0100
@@ -195,22 +195,14 @@
       (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_token_comments ctxt tok =
+  (Thy_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); [])
+    handle exn =>
+      if Exn.is_interrupt exn then Exn.reraise exn
+      else Runtime.exn_messages exn;
 
-fun check_cmts ctxt span tr =
-  Toplevel.setmp_thread_position tr
-    (fn () =>
-      (span |> maps (fn tok =>
-        check_error (fn () => Thy_Output.check_token_comments ctxt tok))) @
-      (span |> maps (fn tok =>
-        if Token.kind_of tok = Token.Comment (SOME Comment.Comment) then
-          check_error (fn () =>
-            Thy_Output.output_document ctxt {markdown = false} (Token.input_of tok))
-        else [])))
-    ();
+fun check_span_comments ctxt span tr =
+  Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) ();
 
 fun report tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
@@ -248,7 +240,7 @@
       | SOME st' =>
           (case try Toplevel.presentation_context st' of
             NONE => []
-          | SOME ctxt' => check_cmts ctxt' span tr));
+          | SOME ctxt' => check_span_comments ctxt' span tr));
     val errs = errs1 @ errs2;
     val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
   in

--- a/src/Pure/Thy/thy_output.ML	Sat Feb 03 14:39:17 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Feb 03 15:34:22 2018 +0100
@@ -8,7 +8,6 @@
 sig
   val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
-  val check_token_comments: Proof.context -> Token.T -> unit
   val output_token: Proof.context -> Token.T -> Latex.text list
   val output_source: Proof.context -> string -> Latex.text list
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
@@ -149,9 +148,6 @@
       val _ = output_symbols_comment ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
 
-fun check_token_comments ctxt tok =
-  check_comments ctxt (Input.source_explode (Token.input_of tok));
-
 end;