OuterLex.read_antiq;
authorwenzelm
Thu Mar 19 15:22:53 2009 +0100 (2009-03-19)
changeset 3058805f81bbb2614
parent 30587 ad19c99529eb
child 30589 cbe27c4ef417
OuterLex.read_antiq;
src/Pure/ML/ml_context.ML
src/Pure/Thy/thy_output.ML
     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))) ()