# HG changeset patch
# User wenzelm
# Date 1218725574 -7200
# Node ID a28b3cd0077b0145260e070b44d6a46d28264aba
# Parent  6e6a159671d439efa4786ca2edfa6bd08accb78f
ML_Context.add_antiq: pass position;

diff -r 6e6a159671d4 -r a28b3cd0077b src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Aug 14 16:52:52 2008 +0200
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Aug 14 16:52:54 2008 +0200
@@ -42,14 +42,14 @@
 (* specific antiquotations *)
 
 fun macro name scan = ML_Context.add_antiq name
-  (scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
+  (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
     (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));
 
 fun inline name scan = ML_Context.add_antiq name
-  (scan >> (fn s => fn {struct_name, background} => (K ("", s), background)));
+  (fn _ => scan >> (fn s => fn {struct_name, background} => (K ("", s), background)));
 
 fun declaration kind name scan = ML_Context.add_antiq name
-  (scan >> (fn s => fn {struct_name, background} =>
+  (fn _ => scan >> (fn s => fn {struct_name, background} =>
     let
       val (a, background') = variant name background;
       val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
diff -r 6e6a159671d4 -r a28b3cd0077b src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Aug 14 16:52:52 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Aug 14 16:52:54 2008 +0200
@@ -27,7 +27,7 @@
     {struct_name: string, background: Proof.context} ->
       (Proof.context -> string * string) * Proof.context
   val add_antiq: string ->
-    (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) -> unit
+    (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) -> unit
   val trace: bool ref
   val eval_wrapper: (string -> unit) * (string -> 'a) -> bool -> Position.T -> string -> unit
   val eval: bool -> Position.T -> string -> unit
@@ -91,7 +91,8 @@
 local
 
 val global_parsers = ref (Symtab.empty:
-  (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table);
+  (Position.T -> Context.generic * Args.T list -> antiq * (Context.generic * Args.T list))
+    Symtab.table);
 
 in
 
@@ -105,7 +106,7 @@
   let val ((name, _), pos) = Args.dest_src src in
     (case Symtab.lookup (! global_parsers) name of
       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
-    | SOME scan => Args.context_syntax "ML antiquotation" scan src ctxt)
+    | SOME scan => Args.context_syntax "ML antiquotation" (scan pos) src ctxt)
   end;
 
 end;
diff -r 6e6a159671d4 -r a28b3cd0077b src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Thu Aug 14 16:52:52 2008 +0200
+++ b/src/Tools/code/code_target.ML	Thu Aug 14 16:52:54 2008 +0200
@@ -2321,7 +2321,7 @@
     | NONE => error ("Bad directive " ^ quote cmd)))
   handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 
-val _ = ML_Context.add_antiq "code" (Args.term >> ml_code_antiq);
+val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
 
 
 (* serializer setup, including serializer defaults *)