equal
deleted
inserted
replaced
151 | expand (Antiquote.Antiq x) = |
151 | expand (Antiquote.Antiq x) = |
152 let val (opts, src) = Antiquote.scan_arguments lex antiq x in |
152 let val (opts, src) = Antiquote.scan_arguments lex antiq x in |
153 options opts (fn () => command src node) (); (*preview errors!*) |
153 options opts (fn () => command src node) (); (*preview errors!*) |
154 PrintMode.with_modes (! modes @ Latex.modes) |
154 PrintMode.with_modes (! modes @ Latex.modes) |
155 (Output.no_warnings (options opts (fn () => command src node))) () |
155 (Output.no_warnings (options opts (fn () => command src node))) () |
156 end; |
156 end |
|
157 | expand (Antiquote.Open _) = "" |
|
158 | expand (Antiquote.Close _) = ""; |
157 val ants = Antiquote.scan_antiquotes (str, pos); |
159 val ants = Antiquote.scan_antiquotes (str, pos); |
158 in |
160 in |
159 if is_none node andalso exists Antiquote.is_antiq ants then |
161 if is_none node andalso exists Antiquote.is_antiq ants then |
160 error ("Cannot expand text antiquotations at top-level" ^ Position.str_of pos) |
162 error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos) |
161 else implode (map expand ants) |
163 else implode (map expand ants) |
162 end; |
164 end; |
163 |
165 |
164 |
166 |
165 |
167 |