# HG changeset patch
# User wenzelm
# Date 1516199453 -3600
# Node ID aad5c0982c3da3715a6f60359b910c75cd278cc4
# Parent  dfc93f2b01ea7d1023fb7be51116250f3713f801
tuned signature;

diff -r dfc93f2b01ea -r aad5c0982c3d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Jan 17 14:40:18 2018 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Jan 17 15:30:53 2018 +0100
@@ -17,6 +17,8 @@
   val output_ascii: string -> string
   val output_symbols: Symbol.symbol list -> string
   val output_syms: string -> string
+  val symbols: Symbol_Pos.T list -> text
+  val symbols_output: Symbol_Pos.T list -> text
   val begin_delim: string -> string
   val end_delim: string -> string
   val begin_tag: string -> string
@@ -198,6 +200,10 @@
 
 end;
 
+fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
+fun symbols_output syms =
+  text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
+
 
 (* tags *)
 
diff -r dfc93f2b01ea -r aad5c0982c3d src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Jan 17 14:40:18 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Jan 17 15:30:53 2018 +0100
@@ -71,11 +71,7 @@
 
 local
 
-fun output_latex syms =
-  [Latex.text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms))];
-
-fun output_symbols syms =
-  [Latex.text (Latex.output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms))];
+val output_symbols = single o Latex.symbols_output;
 
 val output_symbols_antiq =
   (fn Antiquote.Text syms => output_symbols syms
@@ -103,7 +99,7 @@
       output_symbols (Symbol_Pos.cartouche_content syms)
       |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
   | (SOME Comment.Latex, _) =>
-      output_latex (Symbol_Pos.cartouche_content syms));
+      [Latex.symbols (Symbol_Pos.cartouche_content syms)]);
 
 in