# HG changeset patch
# User wenzelm
# Date 1444936661 -7200
# Node ID 0e4c257358cf6b24f735d11af0c6a0f878699b7d
# Parent  c86286ae9fe5f5fc13c0b5d74edd4b2db3adbe96
clarified modules;

diff -r c86286ae9fe5 -r 0e4c257358cf src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Oct 15 17:29:37 2015 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Oct 15 21:17:41 2015 +0200
@@ -11,12 +11,7 @@
     Symbol.symbol list -> string
   val output_symbols: Symbol.symbol list -> string
   val output_ctrl_symbols: Symbol.symbol list -> string
-  val output_basic: Token.T -> string
-  val output_markup: string -> string -> string
-  val output_markup_env: string -> string -> string
-  val output_verbatim: string -> string
-  val markup_true: string
-  val markup_false: string
+  val output_token: Token.T -> string
   val begin_delim: string -> string
   val end_delim: string -> string
   val begin_tag: string -> string
@@ -32,7 +27,7 @@
 structure Latex: LATEX =
 struct
 
-(* literal ASCII *)
+(* output verbatim ASCII *)
 
 val output_ascii =
   translate_string
@@ -44,7 +39,7 @@
           then enclose "{\\char`\\" "}" s else s);
 
 
-(* symbol output *)
+(* output symbols *)
 
 local
 
@@ -125,9 +120,9 @@
 end;
 
 
-(* token output *)
+(* output token *)
 
-fun output_basic tok =
+fun output_token tok =
   let val s = Token.content_of tok in
     if Token.is_kind Token.Comment tok then ""
     else if Token.is_command tok then
@@ -148,20 +143,8 @@
     else output_syms s
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
-val output_text =
-  Symbol.trim_blanks #> Symbol.explode #> output_ctrl_symbols;
 
-fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text txt ^ "%\n}\n";
-
-fun output_markup_env cmd txt =
-  "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
-  output_text txt ^
-  "%\n\\end{isamarkup" ^ cmd ^ "}%\n";
-
-fun output_verbatim txt = "%\n" ^ Symbol.trim_blanks txt ^ "\n";
-
-val markup_true = "\\isamarkuptrue%\n";
-val markup_false = "\\isamarkupfalse%\n";
+(* tags *)
 
 val begin_delim = enclose "%\n\\isadelim" "\n";
 val end_delim = enclose "%\n\\endisadelim" "\n";
diff -r c86286ae9fe5 -r 0e4c257358cf 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;