# HG changeset patch
# User wenzelm
# Date 1515330999 -3600
# Node ID dfee70a24f0c77f6c8a43341978024060aa1fc2c
# Parent  d7c6054b2ab1ac1a439142189ee5a53ffc6ee5e0
tuned;

diff -r d7c6054b2ab1 -r dfee70a24f0c src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Jan 07 13:54:45 2018 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Jan 07 14:16:39 2018 +0100
@@ -19,7 +19,6 @@
   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 begin_delim: string -> string
   val end_delim: string -> string
@@ -202,7 +201,6 @@
     | 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;
 
 end;
diff -r d7c6054b2ab1 -r dfee70a24f0c src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Jan 07 13:54:45 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Jan 07 14:16:39 2018 +0100
@@ -264,13 +264,13 @@
     Scan.option (Symbol_Pos.scan_cartouche_content "Document token error: ")
       >> (fn (syms, NONE) => (false, syms) | (_, SOME syms) => (true, syms));
 
-val output_syms_antiq =
-  (fn Antiquote.Text ss => Latex.output_symbols_pos ss
+val output_symbols_antiq =
+  (fn Antiquote.Text syms => output_symbols syms
     | Antiquote.Control {name = (name, _), body, ...} =>
-        "\\isaantiqcontrol{" ^ Latex.output_symbols (Symbol.explode name) ^ "}" ^
-        Latex.output_symbols_pos body
+        Latex.string ("\\isaantiqcontrol{" ^ Latex.output_symbols (Symbol.explode name) ^ "}") ::
+          output_symbols body
     | Antiquote.Antiq {body, ...} =>
-        enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (Latex.output_symbols_pos body));
+        Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
 
 in
 
@@ -294,11 +294,8 @@
       else if Token.is_kind Token.Alt_String tok then
         output_body state "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" syms
       else if Token.is_kind Token.Verbatim tok then
-        let
-          val pos = Token.pos_of tok;
-          val ants = Antiquote.read (Token.input_of tok);
-          val out = implode (map output_syms_antiq ants);
-        in [Latex.text (enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out, pos)] end
+        Latex.enclose_body "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
+          (maps output_symbols_antiq (Antiquote.read (Token.input_of tok)))
       else if Token.is_kind Token.Cartouche tok then
         output_body state "{\\isacartoucheopen}" "{\\isacartoucheclose}" syms
       else output_body state "" "" syms;