adapted Antiq;
authorwenzelm
Wed Aug 06 00:12:21 2008 +0200 (2008-08-06)
changeset 27755f7cdde18aeb3
parent 27754 36df922b82d4
child 27756 24d0e890b432
adapted Antiq;
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	Wed Aug 06 00:12:02 2008 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Wed Aug 06 00:12:21 2008 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4            fun no_decl _ = ("", "");
     1.5  
     1.6            fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
     1.7 -            | expand (Antiquote.Antiq x) (scope, background) =
     1.8 +            | expand (Antiquote.Antiq (x, _)) (scope, background) =
     1.9                  let
    1.10                    val context = Stack.top scope;
    1.11                    val (f, context') = antiquotation (Antiquote.scan_arguments lex antiq x) context;
     2.1 --- a/src/Pure/Thy/latex.ML	Wed Aug 06 00:12:02 2008 +0200
     2.2 +++ b/src/Pure/Thy/latex.ML	Wed Aug 06 00:12:21 2008 +0200
     2.3 @@ -91,7 +91,7 @@
     2.4  val output_syms_antiqs =
     2.5    Antiquote.scan_antiquotes #> map
     2.6    (fn Antiquote.Text s => output_syms s
     2.7 -    | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
     2.8 +    | Antiquote.Antiq ((s, _), _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
     2.9      | Antiquote.Open _ => "{\\isaantiqopen}"
    2.10      | Antiquote.Close _ => "{\\isaantiqclose}") #>
    2.11    implode;
     3.1 --- a/src/Pure/Thy/thy_output.ML	Wed Aug 06 00:12:02 2008 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Aug 06 00:12:21 2008 +0200
     3.3 @@ -148,7 +148,7 @@
     3.4  fun eval_antiquote lex node (str, pos) =
     3.5    let
     3.6      fun expand (Antiquote.Text s) = s
     3.7 -      | expand (Antiquote.Antiq x) =
     3.8 +      | expand (Antiquote.Antiq (x, _)) =
     3.9            let val (opts, src) = Antiquote.scan_arguments lex antiq x in
    3.10              options opts (fn () => command src node) ();  (*preview errors!*)
    3.11              PrintMode.with_modes (! modes @ Latex.modes)