# HG changeset patch
# User wenzelm
# Date 1515270316 -3600
# Node ID f243af7b5be35297a281ff9a1e6d16506b428722
# Parent  95f5f4bec7af617091201f3990098f6b741df001
clarified signature;

diff -r 95f5f4bec7af -r f243af7b5be3 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Sat Jan 06 21:05:51 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Sat Jan 06 21:25:16 2018 +0100
@@ -101,7 +101,7 @@
           val indentation =
             Latex.output_symbols (replicate (Config.get ctxt Thy_Output.indent) Symbol.space);
         in
-          implode (map Thy_Output.output_token toks) |>
+          Latex.output_text (maps Thy_Output.output_token toks) |>
            (if Config.get ctxt Thy_Output.display then
               split_lines #> map (prefix indentation) #> cat_lines #>
               Latex.environment "isabelle"
diff -r 95f5f4bec7af -r f243af7b5be3 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Jan 06 21:05:51 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Jan 06 21:25:16 2018 +0100
@@ -25,7 +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 output_token: Token.T -> Latex.text list
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list ->
     Token.T list -> Latex.text list
   val pretty_text: Proof.context -> string -> Pretty.T
@@ -282,7 +282,7 @@
       else if Token.is_kind Token.Cartouche tok then
         enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (Latex.output_syms s)
       else Latex.output_syms s;
-  in output end
+  in [Latex.text (output, Token.pos_of tok)] end
   handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
 end;
@@ -308,7 +308,7 @@
 fun present_token state tok =
   (case tok of
     No_Token => []
-  | Basic_Token tok => [Latex.text (output_token tok, Token.pos_of tok)]
+  | Basic_Token tok => output_token tok
   | Markup_Token (cmd, source) =>
       Latex.string ("%\n\\isamarkup" ^ cmd ^ "{") ::
         output_text state {markdown = false} source @ [Latex.string "%\n}\n"]