# HG changeset patch
# User wenzelm
# Date 1409144072 -7200
# Node ID aa6296d09e0eaef6d99dba5d4e4eabf26a901574
# Parent  9f3826352b52071d112259a095c6a219a76e42a5
more explicit Method.modifier with reported position;

diff -r 9f3826352b52 -r aa6296d09e0e src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/HOL/Tools/recdef.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -143,15 +143,15 @@
 val recdef_wfN = "recdef_wf";
 
 val recdef_modifiers =
- [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add): Method.modifier),
-  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add),
-  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del),
-  Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add),
-  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add),
-  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del),
-  Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add),
-  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add),
-  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del)] @
+ [Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
+  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+  Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add @{here}),
+  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
+  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here}),
+  Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add @{here}),
+  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add @{here}),
+  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del @{here})] @
   Clasimp.clasimp_modifiers;
 
 
diff -r 9f3826352b52 -r aa6296d09e0e src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Provers/clasimp.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -191,9 +191,9 @@
 val iffN = "iff";
 
 val iff_modifiers =
- [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add): Method.modifier),
-  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add'),
-  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del)];
+ [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add @{here}),
+  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' @{here}),
+  Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del @{here})];
 
 val clasimp_modifiers =
   Simplifier.simp_modifiers @ Splitter.split_modifiers @
diff -r 9f3826352b52 -r aa6296d09e0e src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Provers/classical.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -928,13 +928,13 @@
 (* automatic methods *)
 
 val cla_modifiers =
- [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
-  Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
-  Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
-  Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
-  Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
-  Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
-  Args.del -- Args.colon >> K (I, rule_del)];
+ [Args.$$$ destN -- Args.bang_colon >> K (Method.modifier (safe_dest NONE) @{here}),
+  Args.$$$ destN -- Args.colon >> K (Method.modifier (haz_dest NONE) @{here}),
+  Args.$$$ elimN -- Args.bang_colon >> K (Method.modifier (safe_elim NONE) @{here}),
+  Args.$$$ elimN -- Args.colon >> K (Method.modifier (haz_elim NONE) @{here}),
+  Args.$$$ introN -- Args.bang_colon >> K (Method.modifier (safe_intro NONE) @{here}),
+  Args.$$$ introN -- Args.colon >> K (Method.modifier (haz_intro NONE) @{here}),
+  Args.del -- Args.colon >> K (Method.modifier rule_del @{here})];
 
 fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
 fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
diff -r 9f3826352b52 -r aa6296d09e0e src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Provers/splitter.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -457,9 +457,9 @@
 (* methods *)
 
 val split_modifiers =
- [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier),
-  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
-  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
+ [Args.$$$ splitN -- Args.colon >> K (Method.modifier split_add @{here}),
+  Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}),
+  Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
 
 
 (* theory setup *)
diff -r 9f3826352b52 -r aa6296d09e0e src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Pure/Isar/method.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -67,7 +67,8 @@
   val method_closure: Proof.context -> Token.src -> Token.src
   val method_cmd: Proof.context -> Token.src -> Proof.context -> method
   val evaluate: text -> Proof.context -> method
-  type modifier = (Proof.context -> Proof.context) * attribute
+  type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
+  val modifier: attribute -> Position.T -> modifier
   val section: modifier parser list -> declaration context_parser
   val sections: modifier parser list -> declaration list context_parser
   type text_range = text * Position.range
@@ -448,13 +449,19 @@
 
 (** concrete syntax **)
 
-(* sections *)
+(* type modifier *)
+
+type modifier =
+  {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T};
 
-type modifier = (Proof.context -> Proof.context) * attribute;
+fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos};
+
+
+(* sections *)
 
 local
 
-fun sect modifier = Scan.depend (fn context =>
+fun sect (modifier : modifier parser) = Scan.depend (fn context =>
   let
     val ctxt = Context.proof_of context;
     fun prep_att src =
@@ -466,7 +473,7 @@
       Parse.xthm >> (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs));
   in
     Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier parse_thm) >>
-      (fn ((tok, (init, att)), thms) =>
+      (fn ((tok, {init, attribute, pos}), thms) =>
         let
           val decl =
             (case Token.get_value tok of
@@ -475,7 +482,11 @@
                 let
                   val facts =
                     Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
-                    |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K att)]), bs));
+                    |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
+                  val _ =
+                    Context_Position.report ctxt (Token.pos_of tok)
+                      (Markup.entity Markup.method_modifierN ""
+                        |> Markup.properties (Position.def_properties_of pos));
                   fun decl phi =
                     Context.mapping I init #>
                     Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
diff -r 9f3826352b52 -r aa6296d09e0e src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -72,6 +72,7 @@
   val fixedN: string val fixed: string -> T
   val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
+  val method_modifierN: string
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
@@ -365,7 +366,7 @@
 val (hiddenN, hidden) = markup_elem "hidden";
 
 
-(* formal entities *)
+(* misc entities *)
 
 val system_optionN = "system_option";
 
@@ -378,6 +379,8 @@
 val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 
+val method_modifierN = "method_modifier";
+
 
 (* inner syntax *)
 
diff -r 9f3826352b52 -r aa6296d09e0e src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Aug 27 14:54:32 2014 +0200
@@ -169,7 +169,7 @@
   val HIDDEN = "hidden"
 
 
-  /* logical entities */
+  /* misc entities */
 
   val CLASS = "class"
   val TYPE_NAME = "type_name"
diff -r 9f3826352b52 -r aa6296d09e0e src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Pure/simplifier.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -332,21 +332,23 @@
 (** method syntax **)
 
 val cong_modifiers =
- [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
-  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
-  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
+ [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add @{here}),
+  Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
+  Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here})];
 
 val simp_modifiers =
- [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
-  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
-  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
-  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (Raw_Simplifier.clear_simpset, simp_add)]
+ [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
+  Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+  Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
+    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
    @ cong_modifiers;
 
 val simp_modifiers' =
- [Args.add -- Args.colon >> K (I, simp_add),
-  Args.del -- Args.colon >> K (I, simp_del),
-  Args.$$$ onlyN -- Args.colon >> K (Raw_Simplifier.clear_simpset, simp_add)]
+ [Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+  Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+  Args.$$$ onlyN -- Args.colon >>
+    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
    @ cong_modifiers;
 
 val simp_options =
diff -r 9f3826352b52 -r aa6296d09e0e src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Sequents/prover.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -106,8 +106,8 @@
 
 fun method tac =
   Method.sections
-   [Args.$$$ "add" -- Args.bang_colon >> K (I, safe_add),
-    Args.$$$ "add" -- Args.colon >> K (I, unsafe_add)]
+   [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add @{here}),
+    Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add @{here})]
   >> K (SIMPLE_METHOD' o tac);
 
 
diff -r 9f3826352b52 -r aa6296d09e0e src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Tools/intuitionistic.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -73,18 +73,18 @@
 val elimN = "elim";
 val destN = "dest";
 
-fun modifier name kind kind' att =
+fun modifier name kind kind' att pos =
   Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
-    >> (pair (I: Proof.context -> Proof.context) o att);
+    >> (fn arg => Method.modifier (att arg) pos);
 
 val modifiers =
- [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
-  modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
-  modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
-  modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
-  modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
-  modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
-  Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
+ [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang @{here},
+  modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest @{here},
+  modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang @{here},
+  modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim @{here},
+  modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang @{here},
+  modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro @{here},
+  Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del @{here})];
 
 in
 
diff -r 9f3826352b52 -r aa6296d09e0e src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 27 14:54:32 2014 +0200
@@ -480,7 +480,9 @@
             Some(Text.Info(r, (t1 + t2, info)))
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
             val kind1 = Word.implode(Word.explode('_', kind))
-            val txt1 = kind1 + " " + quote(name)
+            val txt1 =
+              if (name == "") kind1
+              else kind1 + " " + quote(name)
             val t = prev.info._1
             val txt2 =
               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
diff -r 9f3826352b52 -r aa6296d09e0e src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/ZF/Tools/typechk.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -115,8 +115,8 @@
 val typecheck_setup =
   Method.setup @{binding typecheck}
     (Method.sections
-      [Args.add -- Args.colon >> K (I, TC_add),
-       Args.del -- Args.colon >> K (I, TC_del)]
+      [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}),
+       Args.del -- Args.colon >> K (Method.modifier TC_del @{here})]
       >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
     "ZF type-checking";