--- 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";
--- 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;
--- 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 *)