clarified modules;

--- a/src/Pure/Thy/document_antiquotations.ML	Sat Jan 06 16:56:07 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Sat Jan 06 21:05:51 2018 +0100
@@ -101,7 +101,7 @@
           val indentation =
             Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
         in
-          implode (map Latex.output_token toks) |>
+          implode (map Thy_Output.output_token toks) |>
            (if Config.get ctxt Thy_Output.display then
               split_lines #> map (prefix indentation) #> cat_lines #>
               Latex.environment "isabelle"

--- a/src/Pure/Thy/latex.ML	Sat Jan 06 16:56:07 2018 +0100
+++ b/src/Pure/Thy/latex.ML	Sat Jan 06 21:05:51 2018 +0100
@@ -19,8 +19,8 @@
   val is_latex_control: Symbol.symbol -> bool
   val embed_raw: string -> string
   val output_symbols: Symbol.symbol list -> string
+  val output_symbols_pos: Symbol_Pos.T list -> string
   val output_syms: string -> string
-  val output_token: Token.T -> string
   val begin_delim: string -> string
   val end_delim: string -> string
   val begin_tag: string -> string
@@ -200,47 +200,12 @@
     | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
   else implode (map output_sym syms);
 
+val output_symbols_pos = output_symbols o map Symbol_Pos.symbol;
 val output_syms = output_symbols o Symbol.explode;
 
-val output_syms_antiq =
-  (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
-    | Antiquote.Control {name = (name, _), body, ...} =>
-        "\\isaantiqcontrol{" ^ output_symbols (Symbol.explode name) ^ "}" ^
-        output_symbols (map Symbol_Pos.symbol body)
-    | Antiquote.Antiq {body, ...} =>
-        enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
-          (output_symbols (map Symbol_Pos.symbol body)));
-
 end;
 
 
-(* output token *)
-
-fun output_token tok =
-  let
-    val s = Token.content_of tok;
-    val output =
-      if Token.is_kind Token.Comment tok then ""
-      else if Token.is_command tok then
-        "\\isacommand{" ^ output_syms s ^ "}"
-      else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
-        "\\isakeyword{" ^ output_syms s ^ "}"
-      else if Token.is_kind Token.String tok then
-        enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
-      else if Token.is_kind Token.Alt_String tok then
-        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
-      else if Token.is_kind Token.Verbatim tok then
-        let
-          val ants = Antiquote.read (Token.input_of tok);
-          val out = implode (map output_syms_antiq ants);
-        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
-      else if Token.is_kind Token.Cartouche tok then
-        enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
-      else output_syms s;
-  in output end
-  handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
-
-
 (* tags *)
 
 val begin_delim = enclose_name "%\n\\isadelim" "\n";

--- a/src/Pure/Thy/thy_output.ML	Sat Jan 06 16:56:07 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Jan 06 21:05:51 2018 +0100
@@ -25,6 +25,7 @@
   val integer: string -> int
   val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
   val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list
+  val output_token: Token.T -> string
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
     Token.T list -> Latex.text list
   val pretty_text: Proof.context -> string -> Pretty.T
@@ -245,6 +246,48 @@
 
 (*NB: arranging white space around command spans is a black art*)
 
+
+(* Isar tokens *)
+
+local
+
+val output_syms_antiq =
+  (fn Antiquote.Text ss => Latex.output_symbols_pos ss
+    | Antiquote.Control {name = (name, _), body, ...} =>
+        "\\isaantiqcontrol{" ^ Latex.output_symbols (Symbol.explode name) ^ "}" ^
+        Latex.output_symbols_pos body
+    | Antiquote.Antiq {body, ...} =>
+        enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (Latex.output_symbols_pos body));
+
+in
+
+fun output_token tok =
+  let
+    val s = Token.content_of tok;
+    val output =
+      if Token.is_kind Token.Comment tok then ""
+      else if Token.is_command tok then
+        "\\isacommand{" ^ Latex.output_syms s ^ "}"
+      else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
+        "\\isakeyword{" ^ Latex.output_syms s ^ "}"
+      else if Token.is_kind Token.String tok then
+        enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (Latex.output_syms s)
+      else if Token.is_kind Token.Alt_String tok then
+        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (Latex.output_syms s)
+      else if Token.is_kind Token.Verbatim tok then
+        let
+          val ants = Antiquote.read (Token.input_of tok);
+          val out = implode (map output_syms_antiq ants);
+        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
+      else if Token.is_kind Token.Cartouche tok then
+        enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (Latex.output_syms s)
+      else Latex.output_syms s;
+  in output end
+  handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
+
+end;
+
+
 (* presentation tokens *)
 
 datatype token =
@@ -265,7 +308,7 @@
 fun present_token state tok =
   (case tok of
     No_Token => []
-  | Basic_Token tok => [Latex.text (Latex.output_token tok, Token.pos_of tok)]
+  | Basic_Token tok => [Latex.text (output_token tok, Token.pos_of tok)]
   | Markup_Token (cmd, source) =>
       Latex.string ("%\n\\isamarkup" ^ cmd ^ "{") ::
         output_text state {markdown = false} source @ [Latex.string "%\n}\n"]