--- 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";