1.1 --- a/src/Pure/ML/ml_context.ML Thu Mar 19 15:22:53 2009 +0100
1.2 +++ b/src/Pure/ML/ml_context.ML Thu Mar 19 15:22:53 2009 +0100
1.3 @@ -183,6 +183,7 @@
1.4 local
1.5
1.6 structure P = OuterParse;
1.7 +structure T = OuterLex;
1.8
1.9 val antiq =
1.10 P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
1.11 @@ -213,7 +214,7 @@
1.12 | expand (Antiquote.Antiq x) (scope, background) =
1.13 let
1.14 val context = Stack.top scope;
1.15 - val (f, context') = antiquotation (Antiquote.read_antiq lex antiq x) context;
1.16 + val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
1.17 val (decl, background') = f {background = background, struct_name = struct_name};
1.18 in (decl, (Stack.map_top (K context') scope, background')) end
1.19 | expand (Antiquote.Open _) (scope, background) =
2.1 --- a/src/Pure/Thy/thy_output.ML Thu Mar 19 15:22:53 2009 +0100
2.2 +++ b/src/Pure/Thy/thy_output.ML Thu Mar 19 15:22:53 2009 +0100
2.3 @@ -149,7 +149,7 @@
2.4 let
2.5 fun expand (Antiquote.Text s) = s
2.6 | expand (Antiquote.Antiq x) =
2.7 - let val (opts, src) = Antiquote.read_antiq lex antiq x in
2.8 + let val (opts, src) = T.read_antiq lex antiq x in
2.9 options opts (fn () => command src state) (); (*preview errors!*)
2.10 PrintMode.with_modes (! modes @ Latex.modes)
2.11 (Output.no_warnings (options opts (fn () => command src state))) ()