# HG changeset patch
# User wenzelm
# Date 1214329402 -7200
# Node ID b664e5bc95fd8c492f1cd22b8e31b5f4391fe754
# Parent  21719887bd234f44246a512bd5761df510feda5c
ml_code_antiq: proper scanner combinators;
ML_Antiquote.value;

diff -r 21719887bd23 -r b664e5bc95fd src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Tue Jun 24 19:43:21 2008 +0200
+++ b/src/Tools/code/code_target.ML	Tue Jun 24 19:43:22 2008 +0200
@@ -1843,14 +1843,11 @@
 
 (* instrumentalization by antiquotation *)
 
-fun ml_code_antiq (ctxt, args) = 
+val ml_code_antiq = (Scan.state >> Context.theory_of) -- Scan.repeat1 Args.term >> (fn (thy, ts) =>
   let
-    val thy = Context.theory_of ctxt;
-    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
     val cs = map (CodeUnit.check_const thy) ts;
     val (cs', program) = CodeThingol.consts_program thy cs;
-    val s = sml_code_of thy program cs' ^ " ()";
-  in (("codevals", s), (ctxt', args')) end;
+  in sml_code_of thy program cs' ^ " ()" end);
 
 
 (* code presentation *)
@@ -2294,7 +2291,7 @@
     | NONE => error ("Bad directive " ^ quote cmd)))
   handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 
-val _ = ML_Context.value_antiq "code" ml_code_antiq;
+val _ = ML_Antiquote.value "code" ml_code_antiq;
 
 
 (* serializer setup, including serializer defaults *)