# 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); \ 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 *)