added ML antiquotation @{method};
authorwenzelm
Wed Jan 06 00:04:15 2016 +0100 (2016-01-06 ago)
changeset 62075ea3360245939
parent 62074 5b0bec0583bb
child 62076 1add21f7cabc
added ML antiquotation @{method};
NEWS
src/HOL/Eisbach/Tests.thy
src/Pure/ML/ml_antiquotations.ML
     1.1 --- a/NEWS	Tue Jan 05 23:28:43 2016 +0100
     1.2 +++ b/NEWS	Wed Jan 06 00:04:15 2016 +0100
     1.3 @@ -679,6 +679,9 @@
     1.4  
     1.5  * Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
     1.6  
     1.7 +* Antiquotation @{method NAME} inlines the (checked) name of the given
     1.8 +Isar proof method.
     1.9 +
    1.10  * Pretty printing of Poly/ML compiler output in Isabelle has been
    1.11  improved: proper treatment of break offsets and blocks with consistent
    1.12  breaks.
     2.1 --- a/src/HOL/Eisbach/Tests.thy	Tue Jan 05 23:28:43 2016 +0100
     2.2 +++ b/src/HOL/Eisbach/Tests.thy	Wed Jan 06 00:04:15 2016 +0100
     2.3 @@ -505,7 +505,7 @@
     2.4    Args.term -- Args.term --
     2.5    (Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
     2.6      (fn ((x, y), r) => fn ctxt =>
     2.7 -      Method_Closure.apply_method ctxt "Tests.test_method" [x, y] [r] [] ctxt);
     2.8 +      Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt);
     2.9  \<close>
    2.10  
    2.11  lemma
     3.1 --- a/src/Pure/ML/ml_antiquotations.ML	Tue Jan 05 23:28:43 2016 +0100
     3.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Wed Jan 06 00:04:15 2016 +0100
     3.3 @@ -85,7 +85,11 @@
     3.4      "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
     3.5  
     3.6    ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
     3.7 -    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
     3.8 +    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
     3.9 +
    3.10 +  ML_Antiquotation.inline @{binding method}
    3.11 +    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    3.12 +      ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
    3.13  
    3.14  
    3.15  (* type classes *)