1.1 --- a/src/Pure/Thy/latex.ML	Tue Jun 24 19:43:19 2008 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Jun 24 19:43:20 2008 +0200
     1.3 @@ -91,7 +91,9 @@
     1.4  val output_syms_antiqs =
     1.5    Antiquote.scan_antiquotes #> map
     1.6    (fn Antiquote.Text s => output_syms s
     1.7 -    | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)) #>
     1.8 +    | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
     1.9 +    | Antiquote.Open _ => "{\\isaantiqopen}"
    1.10 +    | Antiquote.Close _ => "{\\isaantiqclose}") #>
    1.11    implode;
    1.12  
    1.13  end;

     2.1 --- a/src/Pure/Thy/thy_output.ML	Tue Jun 24 19:43:19 2008 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Jun 24 19:43:20 2008 +0200
     2.3 @@ -153,11 +153,13 @@
     2.4              options opts (fn () => command src node) ();  (*preview errors!*)
     2.5              PrintMode.with_modes (! modes @ Latex.modes)
     2.6                (Output.no_warnings (options opts (fn () => command src node))) ()
     2.7 -          end;
     2.8 +          end
     2.9 +      | expand (Antiquote.Open _) = ""
    2.10 +      | expand (Antiquote.Close _) = "";
    2.11      val ants = Antiquote.scan_antiquotes (str, pos);
    2.12    in
    2.13      if is_none node andalso exists Antiquote.is_antiq ants then
    2.14 -      error ("Cannot expand text antiquotations at top-level" ^ Position.str_of pos)
    2.15 +      error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)
    2.16      else implode (map expand ants)
    2.17    end;
    2.18