simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
added command 'print_ML_antiquotations';
--- a/NEWS Wed Mar 12 21:29:46 2014 +0100
+++ b/NEWS Wed Mar 12 21:58:48 2014 +0100
@@ -437,6 +437,10 @@
theory merge). Note that the softer Thm.eq_thm_prop is often more
appropriate than Thm.eq_thm.
+* Simplified programming interface to define ML antiquotations, see
+ML_Context.antiquotation, to make it more close to the analogous
+Thy_Output.antiquotation. Minor INCOMPATIBILTY.
+
*** System ***
--- a/etc/isar-keywords-ZF.el Wed Mar 12 21:29:46 2014 +0100
+++ b/etc/isar-keywords-ZF.el Wed Mar 12 21:58:48 2014 +0100
@@ -116,6 +116,7 @@
"pretty_setmargin"
"prf"
"primrec"
+ "print_ML_antiquotations"
"print_abbrevs"
"print_antiquotations"
"print_ast_translation"
@@ -285,6 +286,7 @@
"locale_deps"
"pr"
"prf"
+ "print_ML_antiquotations"
"print_abbrevs"
"print_antiquotations"
"print_attributes"
--- a/etc/isar-keywords.el Wed Mar 12 21:29:46 2014 +0100
+++ b/etc/isar-keywords.el Wed Mar 12 21:58:48 2014 +0100
@@ -170,6 +170,7 @@
"primcorec"
"primcorecursive"
"primrec"
+ "print_ML_antiquotations"
"print_abbrevs"
"print_antiquotations"
"print_ast_translation"
@@ -400,6 +401,7 @@
"nitpick"
"pr"
"prf"
+ "print_ML_antiquotations"
"print_abbrevs"
"print_antiquotations"
"print_attributes"
--- a/src/Pure/Isar/isar_syn.ML Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Mar 12 21:58:48 2014 +0100
@@ -842,11 +842,18 @@
Toplevel.keep (Method.print_methods o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
+ Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
+ "print document antiquotations"
(Scan.succeed (Toplevel.unknown_context o
Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
val _ =
+ Outer_Syntax.improper_command @{command_spec "print_ML_antiquotations"}
+ "print ML antiquotations"
+ (Scan.succeed (Toplevel.unknown_context o
+ Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
+
+val _ =
Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
(Scan.succeed Isar_Cmd.thy_deps);
--- a/src/Pure/ML/ml_antiquote.ML Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Wed Mar 12 21:58:48 2014 +0100
@@ -37,18 +37,15 @@
(* specific antiquotations *)
fun inline name scan =
- ML_Context.add_antiq name
- (Scan.depend (fn context => Scan.pass context scan >> (fn s => (context, K ("", s)))));
+ ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
fun value name scan =
- ML_Context.add_antiq name
- (Scan.depend (fn context => Scan.pass context scan >> (fn s =>
- let
- val ctxt = Context.the_proof context;
- val (a, ctxt') = variant (Binding.name_of name) ctxt;
- val env = "val " ^ a ^ " = " ^ s ^ ";\n";
- val body = "Isabelle." ^ a;
- in (Context.Proof ctxt', (K (env, body))) end)));
+ ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt =>
+ let
+ val (a, ctxt') = variant (Binding.name_of name) ctxt;
+ val env = "val " ^ a ^ " = " ^ s ^ ";\n";
+ val body = "Isabelle." ^ a;
+ in (K (env, body), ctxt') end);
--- a/src/Pure/ML/ml_context.ML Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Wed Mar 12 21:58:48 2014 +0100
@@ -23,9 +23,10 @@
val get_stored_thm: unit -> thm
val ml_store_thms: string * thm list -> unit
val ml_store_thm: string * thm -> unit
- type antiq = Proof.context -> string * string
- val add_antiq: binding -> antiq context_parser -> theory -> theory
- val check_antiq: Proof.context -> xstring * Position.T -> string
+ val print_antiquotations: Proof.context -> unit
+ type decl = Proof.context -> string * string
+ val antiquotation: binding -> 'a context_parser ->
+ (Args.src -> 'a -> Proof.context -> decl * Proof.context) -> theory -> theory
val trace_raw: Config.raw
val trace: bool Config.T
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
@@ -95,28 +96,36 @@
(** ML antiquotations **)
-(* antiquotation commands *)
-
-type antiq = Proof.context -> string * string;
+(* theory data *)
-structure Antiq_Parsers = Theory_Data
+type decl = Proof.context -> string * string; (*final context -> ML env, ML body*)
+structure Antiquotations = Theory_Data
(
- type T = antiq context_parser Name_Space.table;
+ type T = (Args.src -> Proof.context -> decl * Proof.context) Name_Space.table;
val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
val extend = I;
fun merge data : T = Name_Space.merge_tables data;
);
-val get_antiqs = Antiq_Parsers.get o Proof_Context.theory_of;
+val get_antiquotations = Antiquotations.get o Proof_Context.theory_of;
+
+fun add_antiquotation name f thy = thy
+ |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
-fun add_antiq name scan thy = thy
- |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
+fun print_antiquotations ctxt =
+ Pretty.big_list "ML antiquotations:"
+ (map (Pretty.mark_str o #1) (Name_Space.markup_table ctxt (get_antiquotations ctxt)))
+ |> Pretty.writeln;
-fun check_antiq ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_antiqs ctxt);
+fun apply_antiquotation src ctxt =
+ let val (src', f) = Args.check_src ctxt (get_antiquotations ctxt) src
+ in f src' ctxt end;
-fun antiquotation src ctxt =
- let val (src', scan) = Args.check_src ctxt (get_antiqs ctxt) src
- in Args.syntax scan src' ctxt end;
+fun antiquotation name scan body =
+ add_antiquotation name
+ (fn src => fn orig_ctxt =>
+ let val (x, _) = Args.syntax scan src orig_ctxt
+ in body src x orig_ctxt end);
(* parsing and evaluation *)
@@ -159,7 +168,8 @@
fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
| expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
let
- val (decl, ctxt') = antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
+ val (decl, ctxt') =
+ apply_antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
in (decl', ctxt') end;
@@ -210,10 +220,12 @@
eval verbose (#pos source) (ML_Lex.read_source source);
fun eval_in ctxt verbose pos ants =
- Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) ();
+ Context.setmp_thread_data (Option.map Context.Proof ctxt)
+ (fn () => eval verbose pos ants) ();
fun eval_source_in ctxt verbose source =
- Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval_source verbose source) ();
+ Context.setmp_thread_data (Option.map Context.Proof ctxt)
+ (fn () => eval_source verbose source) ();
fun expression pos bind body ants =
exec (fn () => eval false pos
--- a/src/Pure/ML/ml_thms.ML Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML Wed Mar 12 21:58:48 2014 +0100
@@ -35,11 +35,9 @@
(* attribute source *)
val _ = Theory.setup
- (ML_Context.add_antiq @{binding attributes}
- (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
+ (ML_Context.antiquotation @{binding attributes} (Scan.lift Parse_Spec.attribs)
+ (fn _ => fn raw_srcs => fn ctxt =>
let
- val ctxt = Context.the_proof context;
-
val i = serial ();
val srcs = map (Attrib.check_src ctxt) raw_srcs;
val _ = map (Attrib.attribute ctxt) srcs;
@@ -48,15 +46,13 @@
val ml =
("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
string_of_int i ^ ";\n", "Isabelle." ^ a);
- in (Context.Proof ctxt', K ml) end))));
+ in (K ml, ctxt') end));
(* fact references *)
-fun thm_binding kind is_single context thms =
+fun thm_binding kind is_single thms ctxt =
let
- val ctxt = Context.the_proof context;
-
val initial = null (get_thmss ctxt);
val (name, ctxt') = ML_Antiquote.variant kind ctxt;
val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
@@ -69,15 +65,11 @@
val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
in (ml_env, ml_body) end
else ("", ml_body);
- in (Context.Proof ctxt'', decl) end;
+ in (decl, ctxt'') end;
val _ = Theory.setup
- (ML_Context.add_antiq @{binding thm}
- (Scan.depend (fn context =>
- Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
- ML_Context.add_antiq @{binding thms}
- (Scan.depend (fn context =>
- Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
+ (ML_Context.antiquotation @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
+ ML_Context.antiquotation @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
(* ad-hoc goals *)
@@ -87,29 +79,26 @@
val goal = Scan.unless (by || and_) Args.name_inner_syntax;
val _ = Theory.setup
- (ML_Context.add_antiq @{binding lemma}
- (Scan.depend (fn context =>
- Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
- (by |-- Method.parse -- Scan.option Method.parse)
- >> (fn ((is_open, raw_propss), (m1, m2)) =>
- let
- val ctxt = Context.proof_of context;
-
- val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
+ (ML_Context.antiquotation @{binding lemma}
+ (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
+ (by |-- Method.parse -- Scan.option Method.parse)))
+ (fn _ => fn ((is_open, raw_propss), (m1, m2)) => fn ctxt =>
+ let
+ val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
- val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
- val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
- fun after_qed res goal_ctxt =
- Proof_Context.put_thms false (Auto_Bind.thisN,
- SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
+ val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
+ val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
+ fun after_qed res goal_ctxt =
+ Proof_Context.put_thms false (Auto_Bind.thisN,
+ SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
- val ctxt' = ctxt
- |> Proof.theorem NONE after_qed propss
- |> Proof.global_terminal_proof (m1, m2);
- val thms =
- Proof_Context.get_fact ctxt'
- (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
- in thm_binding "lemma" (length (flat propss) = 1) context thms end))));
+ val ctxt' = ctxt
+ |> Proof.theorem NONE after_qed propss
+ |> Proof.global_terminal_proof (m1, m2);
+ val thms =
+ Proof_Context.get_fact ctxt'
+ (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
+ in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
end;
--- a/src/Pure/Pure.thy Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/Pure.thy Wed Mar 12 21:58:48 2014 +0100
@@ -78,14 +78,15 @@
and "finally" "ultimately" :: prf_chain % "proof"
and "back" :: prf_script % "proof"
and "Isabelle.command" :: control
- and "help" "print_commands" "print_options"
- "print_context" "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
+ and "help" "print_commands" "print_options" "print_context"
+ "print_theory" "print_syntax" "print_abbrevs" "print_defn_rules"
"print_theorems" "print_locales" "print_classes" "print_locale"
"print_interps" "print_dependencies" "print_attributes"
"print_simpset" "print_rules" "print_trans_rules" "print_methods"
- "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"
- "print_binds" "print_facts" "print_cases" "print_statement" "thm"
- "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
+ "print_antiquotations" "print_ML_antiquotations" "thy_deps"
+ "locale_deps" "class_deps" "thm_deps" "print_binds" "print_facts"
+ "print_cases" "print_statement" "thm" "prf" "full_prf" "prop"
+ "term" "typ" "print_codesetup" "unused_thms"
:: diag
and "cd" :: control
and "pwd" :: diag
--- a/src/Pure/Thy/thy_output.ML Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Mar 12 21:58:48 2014 +0100
@@ -112,11 +112,11 @@
|> Pretty.chunks |> Pretty.writeln
end;
-fun antiquotation name scan out =
+fun antiquotation name scan body =
add_command name
(fn src => fn state => fn ctxt =>
let val (x, ctxt') = Args.syntax scan src ctxt
- in out {source = src, state = state, context = ctxt'} x end);
+ in body {source = src, state = state, context = ctxt'} x end);
--- a/src/Tools/Code/code_runtime.ML Wed Mar 12 21:29:46 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML Wed Mar 12 21:58:48 2014 +0100
@@ -257,15 +257,12 @@
in
-fun ml_code_antiq context raw_const =
+fun ml_code_antiq raw_const ctxt =
let
- val ctxt = Context.the_proof context;
val thy = Proof_Context.theory_of ctxt;
-
val const = Code.check_const thy raw_const;
val is_first = is_first_occ ctxt;
- val ctxt' = register_const const ctxt;
- in (Context.Proof ctxt', print_code is_first const) end;
+ in (print_code is_first const, register_const const ctxt) end;
end; (*local*)
@@ -356,9 +353,8 @@
(** Isar setup **)
-val _ = Theory.setup
- (ML_Context.add_antiq @{binding code}
- (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)));
+val _ =
+ Theory.setup (ML_Context.antiquotation @{binding code} Args.term (fn _ => ml_code_antiq));
local