Antiquote.read/read_arguments;
authorwenzelm
Thu Aug 07 13:45:09 2008 +0200 (2008-08-07)
changeset 2777198499933a50f
parent 27770 10d84e124a2f
child 27772 b933c997eab3
Antiquote.read/read_arguments;
src/Pure/ML/ml_context.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/ML/ml_context.ML	Thu Aug 07 13:45:07 2008 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Thu Aug 07 13:45:09 2008 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  
     1.5  fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
     1.6    let
     1.7 -    val ants = Antiquote.scan_antiquotes (txt, pos);
     1.8 +    val ants = Antiquote.read (txt, pos);
     1.9      val ((ml_env, ml_body), opt_ctxt') =
    1.10        if not (exists Antiquote.is_antiq ants) then (("", Symbol.escape txt), opt_ctxt)
    1.11        else
    1.12 @@ -141,7 +141,7 @@
    1.13              | expand (Antiquote.Antiq (x, _)) (scope, background) =
    1.14                  let
    1.15                    val context = Stack.top scope;
    1.16 -                  val (f, context') = antiquotation (Antiquote.scan_arguments lex antiq x) context;
    1.17 +                  val (f, context') = antiquotation (Antiquote.read_arguments lex antiq x) context;
    1.18                    val (decl, background') = f {background = background, struct_name = struct_name};
    1.19                  in (decl, (Stack.map_top (K context') scope, background')) end
    1.20              | expand (Antiquote.Open _) (scope, background) =
     2.1 --- a/src/Pure/Thy/latex.ML	Thu Aug 07 13:45:07 2008 +0200
     2.2 +++ b/src/Pure/Thy/latex.ML	Thu Aug 07 13:45:09 2008 +0200
     2.3 @@ -89,7 +89,7 @@
     2.4  val output_syms = output_symbols o Symbol.explode;
     2.5  
     2.6  val output_syms_antiqs =
     2.7 -  Antiquote.scan_antiquotes #> map
     2.8 +  Antiquote.read #> map
     2.9    (fn Antiquote.Text s => output_syms s
    2.10      | Antiquote.Antiq ((s, _), _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
    2.11      | Antiquote.Open _ => "{\\isaantiqopen}"
     3.1 --- a/src/Pure/Thy/thy_output.ML	Thu Aug 07 13:45:07 2008 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Aug 07 13:45:09 2008 +0200
     3.3 @@ -149,14 +149,14 @@
     3.4    let
     3.5      fun expand (Antiquote.Text s) = s
     3.6        | expand (Antiquote.Antiq (x, _)) =
     3.7 -          let val (opts, src) = Antiquote.scan_arguments lex antiq x in
     3.8 +          let val (opts, src) = Antiquote.read_arguments lex antiq x in
     3.9              options opts (fn () => command src node) ();  (*preview errors!*)
    3.10              PrintMode.with_modes (! modes @ Latex.modes)
    3.11                (Output.no_warnings (options opts (fn () => command src node))) ()
    3.12            end
    3.13        | expand (Antiquote.Open _) = ""
    3.14        | expand (Antiquote.Close _) = "";
    3.15 -    val ants = Antiquote.scan_antiquotes (str, pos);
    3.16 +    val ants = Antiquote.read (str, pos);
    3.17    in
    3.18      if is_none node andalso exists Antiquote.is_antiq ants then
    3.19        error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)