104 | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym |
104 | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym |
105 | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym |
105 | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym |
106 | Symbol.Malformed s => error (Symbol.malformed_msg s) |
106 | Symbol.Malformed s => error (Symbol.malformed_msg s) |
107 | Symbol.EOF => error "Bad EOF symbol"); |
107 | Symbol.EOF => error "Bad EOF symbol"); |
108 |
108 |
|
109 val scan_latex_length = |
|
110 Scan.many1 (fn (s, _) => Symbol.not_eof s andalso not (is_latex_control s)) |
|
111 >> (Symbol.length o map Symbol_Pos.symbol) || |
|
112 Scan.one (is_latex_control o Symbol_Pos.symbol) -- |
|
113 Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0; |
|
114 |
109 fun scan_latex known = |
115 fun scan_latex known = |
110 Scan.one (is_latex_control o Symbol_Pos.symbol) |-- |
116 Scan.one (is_latex_control o Symbol_Pos.symbol) |-- |
111 Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) || |
117 Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) || |
112 Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol); |
118 Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol); |
113 |
119 |
114 fun read_latex known syms = |
120 fun read scan syms = |
115 (case Scan.read Symbol_Pos.stopper (Scan.repeat (scan_latex known)) |
121 Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms); |
116 (map (rpair Position.none) syms) of |
|
117 SOME ss => implode ss |
|
118 | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms))); |
|
119 |
122 |
120 in |
123 in |
121 |
124 |
|
125 fun length_symbols syms = |
|
126 fold Integer.add (these (read scan_latex_length syms)) 0; |
|
127 |
122 fun output_known_symbols known syms = |
128 fun output_known_symbols known syms = |
123 if exists is_latex_control syms then read_latex known syms |
129 if exists is_latex_control syms then |
|
130 (case read (scan_latex known) syms of |
|
131 SOME ss => implode ss |
|
132 | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms))) |
124 else implode (map (output_known_sym known) syms); |
133 else implode (map (output_known_sym known) syms); |
125 |
134 |
126 val output_symbols = output_known_symbols (K true, K true); |
135 val output_symbols = output_known_symbols (K true, K true); |
127 val output_syms = output_symbols o Symbol.explode; |
136 val output_syms = output_symbols o Symbol.explode; |
128 |
137 |
199 val latexN = "latex"; |
208 val latexN = "latex"; |
200 val modes = [latexN, Symbol.xsymbolsN]; |
209 val modes = [latexN, Symbol.xsymbolsN]; |
201 |
210 |
202 fun latex_output str = |
211 fun latex_output str = |
203 let val syms = Symbol.explode str |
212 let val syms = Symbol.explode str |
204 in (output_symbols syms, Symbol.length syms) end; |
213 in (output_symbols syms, length_symbols syms) end; |
205 |
214 |
206 fun latex_markup (s, _) = |
215 fun latex_markup (s, _) = |
207 if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N |
216 if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N |
208 then ("\\isacommand{", "}") |
217 then ("\\isacommand{", "}") |
209 else if s = Markup.keyword2N |
218 else if s = Markup.keyword2N |