src/Pure/Thy/thy_output.ML
changeset 30683 e8ac1f9d9469
parent 30642 0c9f9c49d5df
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Mar 24 11:39:25 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Mar 24 11:57:41 2009 +0100
     1.3 @@ -148,8 +148,8 @@
     1.4  fun eval_antiquote lex state (txt, pos) =
     1.5    let
     1.6      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
     1.7 -      | expand (Antiquote.Antiq x) =
     1.8 -          let val (opts, src) = T.read_antiq lex antiq x in
     1.9 +      | expand (Antiquote.Antiq (ss, (pos, _))) =
    1.10 +          let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
    1.11              options opts (fn () => command src state) ();  (*preview errors!*)
    1.12              PrintMode.with_modes (! modes @ Latex.modes)
    1.13                (Output.no_warnings (options opts (fn () => command src state))) ()