src/Pure/Thy/thy_output.ML
changeset 27771 98499933a50f
parent 27755 f7cdde18aeb3
child 27781 5a82ee34e9fc
     1.1 --- a/src/Pure/Thy/thy_output.ML	Thu Aug 07 13:45:07 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Aug 07 13:45:09 2008 +0200
     1.3 @@ -149,14 +149,14 @@
     1.4    let
     1.5      fun expand (Antiquote.Text s) = s
     1.6        | expand (Antiquote.Antiq (x, _)) =
     1.7 -          let val (opts, src) = Antiquote.scan_arguments lex antiq x in
     1.8 +          let val (opts, src) = Antiquote.read_arguments lex antiq x in
     1.9              options opts (fn () => command src node) ();  (*preview errors!*)
    1.10              PrintMode.with_modes (! modes @ Latex.modes)
    1.11                (Output.no_warnings (options opts (fn () => command src node))) ()
    1.12            end
    1.13        | expand (Antiquote.Open _) = ""
    1.14        | expand (Antiquote.Close _) = "";
    1.15 -    val ants = Antiquote.scan_antiquotes (str, pos);
    1.16 +    val ants = Antiquote.read (str, pos);
    1.17    in
    1.18      if is_none node andalso exists Antiquote.is_antiq ants then
    1.19        error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)