# HG changeset patch
# User wenzelm
# Date 1217974341 -7200
# Node ID f7cdde18aeb3d67db4e5be27a76f32af97e470d3
# Parent  36df922b82d48af14853ae412e9aadba0d9d77de
adapted Antiq;

diff -r 36df922b82d4 -r f7cdde18aeb3 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Aug 06 00:12:02 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed Aug 06 00:12:21 2008 +0200
@@ -138,7 +138,7 @@
           fun no_decl _ = ("", "");
 
           fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
-            | expand (Antiquote.Antiq x) (scope, background) =
+            | expand (Antiquote.Antiq (x, _)) (scope, background) =
                 let
                   val context = Stack.top scope;
                   val (f, context') = antiquotation (Antiquote.scan_arguments lex antiq x) context;
diff -r 36df922b82d4 -r f7cdde18aeb3 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Aug 06 00:12:02 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Wed Aug 06 00:12:21 2008 +0200
@@ -91,7 +91,7 @@
 val output_syms_antiqs =
   Antiquote.scan_antiquotes #> map
   (fn Antiquote.Text s => output_syms s
-    | Antiquote.Antiq (s, _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
+    | Antiquote.Antiq ((s, _), _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
     | Antiquote.Open _ => "{\\isaantiqopen}"
     | Antiquote.Close _ => "{\\isaantiqclose}") #>
   implode;
diff -r 36df922b82d4 -r f7cdde18aeb3 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Aug 06 00:12:02 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed Aug 06 00:12:21 2008 +0200
@@ -148,7 +148,7 @@
 fun eval_antiquote lex node (str, pos) =
   let
     fun expand (Antiquote.Text s) = s
-      | expand (Antiquote.Antiq x) =
+      | expand (Antiquote.Antiq (x, _)) =
           let val (opts, src) = Antiquote.scan_arguments lex antiq x in
             options opts (fn () => command src node) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)