src/Pure/Thy/thy_output.ML

--- a/src/Pure/Thy/thy_output.ML	Thu Oct 15 17:29:37 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Oct 15 21:17:41 2015 +0200
@@ -218,14 +218,6 @@
   | Markup_Env_Token of string * Input.source
   | Verbatim_Token of Input.source;
 
-fun output_token state =
-  let val eval = eval_antiquote state in
-    fn No_Token => ""
-     | Basic_Token tok => Latex.output_basic tok
-     | Markup_Token (cmd, source) => Latex.output_markup cmd (eval source)
-     | Markup_Env_Token (cmd, source) => Latex.output_markup_env cmd (eval source)
-     | Verbatim_Token source => Latex.output_verbatim (eval source)
-  end;
 
 fun basic_token pred (Basic_Token tok) = pred tok
   | basic_token _ _ = false;
@@ -236,6 +228,27 @@
 val newline_token = basic_token Token.is_newline;
 
 
+(* output token *)
+
+val output_text =
+  Symbol.trim_blanks #> Symbol.explode #> Latex.output_ctrl_symbols;
+
+fun output_token state =
+  let
+    val eval = eval_antiquote state;
+    fun output No_Token = ""
+      | output (Basic_Token tok) = Latex.output_token tok
+      | output (Markup_Token (cmd, source)) =
+          "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text (eval source) ^ "%\n}\n"
+      | output (Markup_Env_Token (cmd, source)) =
+          "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
+          output_text (eval source) ^
+          "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
+      | output (Verbatim_Token source) =
+          "%\n" ^ Symbol.trim_blanks (eval source) ^ "\n";
+  in output end;
+
+
 (* command spans *)
 
 type command = string * Position.T * string list;   (*name, position, tags*)
@@ -342,6 +355,9 @@
 
 local
 
+val markup_true = "\\isamarkuptrue%\n";
+val markup_false = "\\isamarkupfalse%\n";
+
 val space_proper =
   Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper;
 
@@ -393,7 +409,7 @@
       >> (fn ((cmd_mod, cmd), tags) =>
         map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
           [(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
-            (Basic_Token cmd, (Latex.markup_false, d)))]));
+            (Basic_Token cmd, (markup_false, d)))]));
 
     val cmt = Scan.peek (fn d =>
       Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.document_source) >>
@@ -404,8 +420,8 @@
 
     val tokens =
       (ignored ||
-        markup Keyword.is_document_heading Markup_Token Latex.markup_true ||
-        markup Keyword.is_document_body Markup_Env_Token Latex.markup_true ||
+        markup Keyword.is_document_heading Markup_Token markup_true ||
+        markup Keyword.is_document_body Markup_Env_Token markup_true ||
         markup Keyword.is_document_raw (Verbatim_Token o #2) "") >> single ||
       command ||
       (cmt || other) >> single;