# HG changeset patch
# User wenzelm
# Date 1214329400 -7200
# Node ID d44490b0619004b0a9306883f9338ab535ec3a0e
# Parent  4b28b80dd1f85f6f20ada23b08429ff145a8a1da
Antiquote.Open/Close;

diff -r 4b28b80dd1f8 -r d44490b06190 src/Pure/Thy/latex.ML
--- 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;
diff -r 4b28b80dd1f8 -r d44490b06190 src/Pure/Thy/thy_output.ML
--- 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;