src/Pure/Thy/thy_output.ML

--- a/src/Pure/Thy/thy_output.ML	Sun Jan 14 15:31:02 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Jan 14 16:21:29 2018 +0100
@@ -71,6 +71,9 @@
 
 local
 
+fun output_latex syms =
+  [Latex.text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms))];
+
 fun output_symbols syms =
   [Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))];
 
@@ -98,7 +101,9 @@
       end
   | (SOME Comment.Cancel, _) =>
       output_symbols (Symbol_Pos.cartouche_content syms)
-      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}");
+      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
+  | (SOME Comment.Latex, _) =>
+      output_latex (Symbol_Pos.cartouche_content syms));
 
 in
 
@@ -129,13 +134,9 @@
   Comment.read_body #> (Option.app o List.app) (fn (comment, syms) =>
     let
       val pos = #1 (Symbol_Pos.range syms);
-      val markup =
-        comment |> Option.map
-          (fn Comment.Comment => Markup.language_document true
-            | Comment.Cancel => Markup.language_text true);
       val _ =
-        markup |> Option.app (fn m =>
-          Context_Position.reports ctxt [(pos, m), (pos, Markup.cartouche)]);
+        comment |> Option.app (fn kind =>
+          Context_Position.reports ctxt [(pos, Comment.markup kind), (pos, Markup.cartouche)]);
       val _ = output_symbols_comment ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);