clarified markup: more like outer syntax side-comment;

--- a/src/Pure/Syntax/lexicon.ML	Tue Jan 09 16:25:35 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Jan 09 17:09:34 2018 +0100
@@ -171,7 +171,6 @@
   | StringSy => Markup.inner_string
   | Cartouche => Markup.inner_cartouche
   | Comment => Markup.inner_comment
-  | Comment_Cartouche => Markup.inner_comment
   | _ => Markup.empty;
 
 fun report_of_token (Token (kind, s, (pos, _))) =

--- a/src/Pure/Thy/thy_output.ML	Tue Jan 09 16:25:35 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Jan 09 17:09:34 2018 +0100
@@ -128,8 +128,16 @@
 
 fun check_comments ctxt =
   read_symbols_comment #> (Option.app o List.app) (fn (is_comment, syms) =>
-    (output_symbols_comment ctxt {antiq = false} (is_comment, syms);
-     if is_comment then check_comments ctxt syms else ()));
+    let
+      val pos = #1 (Symbol_Pos.range syms);
+      val _ =
+        if is_comment then
+          Context_Position.reports ctxt
+            [(pos, Markup.language_document true),
+             (pos, Markup.cartouche)]
+        else ();
+      val _ = output_symbols_comment ctxt {antiq = false} (is_comment, syms);
+    in if is_comment then check_comments ctxt syms else () end);
 
 fun check_token_comments ctxt tok =
   check_comments ctxt (Input.source_explode (Token.input_of tok));

--- a/src/Pure/Tools/rail.ML	Tue Jan 09 16:25:35 2018 +0100
+++ b/src/Pure/Tools/rail.ML	Tue Jan 09 17:09:34 2018 +0100
@@ -84,7 +84,6 @@
 fun reports_of_token (Token ((pos, _), (Keyword, x))) =
       map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
   | reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
-  | reports_of_token (Token ((pos, _), (Comment, _))) = [(pos, Markup.inner_comment)]
   | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports [Antiquote.Antiq antiq]
   | reports_of_token _ = [];