--- a/NEWS Tue Jan 05 23:28:43 2016 +0100
+++ b/NEWS Wed Jan 06 00:04:15 2016 +0100
@@ -679,6 +679,9 @@
* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
+* Antiquotation @{method NAME} inlines the (checked) name of the given
+Isar proof method.
+
* Pretty printing of Poly/ML compiler output in Isabelle has been
improved: proper treatment of break offsets and blocks with consistent
breaks.
--- a/src/HOL/Eisbach/Tests.thy Tue Jan 05 23:28:43 2016 +0100
+++ b/src/HOL/Eisbach/Tests.thy Wed Jan 06 00:04:15 2016 +0100
@@ -505,7 +505,7 @@
Args.term -- Args.term --
(Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
(fn ((x, y), r) => fn ctxt =>
- Method_Closure.apply_method ctxt "Tests.test_method" [x, y] [r] [] ctxt);
+ Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt);
\<close>
lemma
--- a/src/Pure/ML/ml_antiquotations.ML Tue Jan 05 23:28:43 2016 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Wed Jan 06 00:04:15 2016 +0100
@@ -85,7 +85,11 @@
"Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
- "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
+ "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+
+ ML_Antiquotation.inline @{binding method}
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+ ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
(* type classes *)