# HG changeset patch
# User wenzelm
# Date 1452035055 -3600
# Node ID ea3360245939010f434ddbdc73d5b806619e3372
# Parent  5b0bec0583bbcfac9484c9f1ff966ecbe711b7f5
added ML antiquotation @{method};

diff -r 5b0bec0583bb -r ea3360245939 NEWS
--- 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.
diff -r 5b0bec0583bb -r ea3360245939 src/HOL/Eisbach/Tests.thy
--- 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
diff -r 5b0bec0583bb -r ea3360245939 src/Pure/ML/ml_antiquotations.ML
--- 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 *)