# HG changeset patch
# User wenzelm
# Date 1515329685 -3600
# Node ID d7c6054b2ab1ac1a439142189ee5a53ffc6ee5e0
# Parent  ba226b87c69e24ab45a343c3d6b5d7a70bcc3352
clarified output: avoid extra space;

diff -r ba226b87c69e -r d7c6054b2ab1 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Jan 07 13:45:21 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Jan 07 13:54:45 2018 +0100
@@ -246,10 +246,6 @@
 
 (* output tokens with comments *)
 
-fun output_markup state cmd source =
-  Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
-    (output_text state {markdown = false} source);
-
 local
 
 fun output_symbols syms =
@@ -257,8 +253,9 @@
 
 fun output_symbols_comment state (is_comment, syms) =
   if is_comment then
-    output_markup state "cmt"
-      (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms))
+    Latex.enclose_body ("%\n\\isamarkupcmt{") "}"
+      (output_text state {markdown = false}
+        (Input.source true (Symbol_Pos.implode syms) (Symbol_Pos.range syms)))
   else output_symbols syms;
 
 val scan_symbols_comment =
@@ -338,7 +335,9 @@
   (case tok of
     No_Token => []
   | Basic_Token tok => output_token state tok
-  | Markup_Token (cmd, source) => output_markup state cmd source
+  | Markup_Token (cmd, source) =>
+      Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
+        (output_text state {markdown = false} source)
   | Markup_Env_Token (cmd, source) =>
       [Latex.environment_block ("isamarkup" ^ cmd) (output_text state {markdown = true} source)]
   | Raw_Token source =>