# HG changeset patch
# User wenzelm
# Date 1218109509 -7200
# Node ID 98499933a50f7b97094885c0f0d5d48021ad0917
# Parent  10d84e124a2f5fa8c290e9073e711610830af4fd
Antiquote.read/read_arguments;

diff -r 10d84e124a2f -r 98499933a50f src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Aug 07 13:45:07 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Aug 07 13:45:09 2008 +0200
@@ -123,7 +123,7 @@
 
 fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
   let
-    val ants = Antiquote.scan_antiquotes (txt, pos);
+    val ants = Antiquote.read (txt, pos);
     val ((ml_env, ml_body), opt_ctxt') =
       if not (exists Antiquote.is_antiq ants) then (("", Symbol.escape txt), opt_ctxt)
       else
@@ -141,7 +141,7 @@
             | expand (Antiquote.Antiq (x, _)) (scope, background) =
                 let
                   val context = Stack.top scope;
-                  val (f, context') = antiquotation (Antiquote.scan_arguments lex antiq x) context;
+                  val (f, context') = antiquotation (Antiquote.read_arguments 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) =
diff -r 10d84e124a2f -r 98499933a50f src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Thu Aug 07 13:45:07 2008 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Aug 07 13:45:09 2008 +0200
@@ -89,7 +89,7 @@
 val output_syms = output_symbols o Symbol.explode;
 
 val output_syms_antiqs =
-  Antiquote.scan_antiquotes #> map
+  Antiquote.read #> map
   (fn Antiquote.Text s => output_syms s
     | Antiquote.Antiq ((s, _), _) => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms s)
     | Antiquote.Open _ => "{\\isaantiqopen}"
diff -r 10d84e124a2f -r 98499933a50f src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Aug 07 13:45:07 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Aug 07 13:45:09 2008 +0200
@@ -149,14 +149,14 @@
   let
     fun expand (Antiquote.Text s) = s
       | expand (Antiquote.Antiq (x, _)) =
-          let val (opts, src) = Antiquote.scan_arguments lex antiq x in
+          let val (opts, src) = Antiquote.read_arguments lex antiq x in
             options opts (fn () => command src node) ();  (*preview errors!*)
             PrintMode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings (options opts (fn () => command src node))) ()
           end
       | expand (Antiquote.Open _) = ""
       | expand (Antiquote.Close _) = "";
-    val ants = Antiquote.scan_antiquotes (str, pos);
+    val ants = Antiquote.read (str, pos);
   in
     if is_none node andalso exists Antiquote.is_antiq ants then
       error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)