OuterLex.read_antiq;
authorwenzelm
Thu, 19 Mar 2009 15:22:53 +0100
changeset 30588 05f81bbb2614
parent 30587 ad19c99529eb
child 30589 cbe27c4ef417
OuterLex.read_antiq;
src/Pure/ML/ml_context.ML
src/Pure/Thy/thy_output.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 19 15:22:53 2009 +0100
@@ -183,6 +183,7 @@
 local
 
 structure P = OuterParse;
+structure T = OuterLex;
 
 val antiq =
   P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
@@ -213,7 +214,7 @@
             | expand (Antiquote.Antiq x) (scope, background) =
                 let
                   val context = Stack.top scope;
-                  val (f, context') = antiquotation (Antiquote.read_antiq lex antiq x) context;
+                  val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
                   val (decl, background') = f {background = background, struct_name = struct_name};
                 in (decl, (Stack.map_top (K context') scope, background')) end
             | expand (Antiquote.Open _) (scope, background) =
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:22:53 2009 +0100
@@ -149,7 +149,7 @@
   let
     fun expand (Antiquote.Text s) = s
       | expand (Antiquote.Antiq x) =
-          let val (opts, src) = Antiquote.read_antiq lex antiq x in
+          let val (opts, src) = T.read_antiq lex antiq x in
             options opts (fn () => command src state) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings (options opts (fn () => command src state))) ()