--- a/src/Pure/Thy/latex.ML Tue Jun 24 19:43:19 2008 +0200
+++ b/src/Pure/Thy/latex.ML Tue Jun 24 19:43:20 2008 +0200
@@ -91,7 +91,9 @@
val output_syms_antiqs =
Antiquote.scan_antiquotes #> map
(fn Antiquote.Text s => output_syms s
- | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #>
+ | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
+ | Antiquote.Open _ => "{\\isaantiqopen}"
+ | Antiquote.Close _ => "{\\isaantiqclose}") #>
implode;
end;
--- a/src/Pure/Thy/thy_output.ML Tue Jun 24 19:43:19 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Jun 24 19:43:20 2008 +0200
@@ -153,11 +153,13 @@
options opts (fn () => command src node) (); (*preview errors!*)
PrintMode.with_modes (! modes @ Latex.modes)
(Output.no_warnings (options opts (fn () => command src node))) ()
- end;
+ end
+ | expand (Antiquote.Open _) = ""
+ | expand (Antiquote.Close _) = "";
val ants = Antiquote.scan_antiquotes (str, pos);
in
if is_none node andalso exists Antiquote.is_antiq ants then
- error ("Cannot expand text antiquotations at top-level" ^ Position.str_of pos)
+ error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)
else implode (map expand ants)
end;