# HG changeset patch
# User wenzelm
# Date 1409144133 -7200
# Node ID 930727de976c3656b1df3d5a73bf7e1092887b61
# Parent  b5cdfb352814072081b9097c457d73dacc149502# Parent  aa6296d09e0eaef6d99dba5d4e4eabf26a901574
merged

diff -r b5cdfb352814 -r 930727de976c src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/HOL/Tools/recdef.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Provers/clasimp.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Provers/classical.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Provers/splitter.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/General/symbol_pos.ML	Wed Aug 27 14:55:33 2014 +0200
@@ -41,6 +41,7 @@
   val implode_range: Position.T -> Position.T -> T list -> text * Position.range
   val explode: text * Position.T -> T list
   type source = {delimited: bool, text: text, pos: Position.T}
+  val source_explode: source -> T list
   val source_content: source -> string * Position.T
   val scan_ident: T list -> T list * T list
   val is_identifier: string -> bool
@@ -261,6 +262,8 @@
 
 type source = {delimited: bool, text: text, pos: Position.T};
 
+fun source_explode {delimited = _, text, pos} = explode (text, pos);
+
 fun source_content {delimited = _, text, pos} =
   let val syms = explode (text, pos) in (content syms, pos) end;
 
diff -r b5cdfb352814 -r 930727de976c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Aug 27 14:55:33 2014 +0200
@@ -48,6 +48,8 @@
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
+  val check_attribs: Proof.context -> Token.src list -> Token.src list
+  val read_attribs: Proof.context -> Symbol_Pos.source -> Token.src list
   val transform_facts: morphism ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list
@@ -276,6 +278,25 @@
 end;
 
 
+(* read attribute source *)
+
+fun check_attribs ctxt raw_srcs =
+  let
+    val srcs = map (check_src ctxt) raw_srcs;
+    val _ = map (attribute ctxt) srcs;
+  in srcs end;
+
+fun read_attribs ctxt source =
+  let
+    val syms = Symbol_Pos.source_explode source;
+    val lex = #1 (Keyword.get_lexicons ());
+  in
+    (case Token.read lex Parse.attribs (syms, #pos source) of
+      [raw_srcs] => check_attribs ctxt raw_srcs
+    | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
+  end;
+
+
 (* transform fact expressions *)
 
 fun transform_facts phi = map (fn ((a, atts), bs) =>
diff -r b5cdfb352814 -r 930727de976c src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Isar/method.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Isar/token.ML	Wed Aug 27 14:55:33 2014 +0200
@@ -86,9 +86,10 @@
   val source: {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
-  val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
+  val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a list
+  val read_antiq: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
@@ -585,28 +586,33 @@
 end;
 
 
-(* read_antiq *)
-
-fun read_antiq lex scan (syms, pos) =
-  let
-    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
-      "@{" ^ Symbol_Pos.content syms ^ "}");
-
-    val res =
-      Source.of_list syms
-      |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
-      |> source_proper
-      |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
-      |> Source.exhaust;
-  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
-
-
 
 (** parsers **)
 
 type 'a parser = T list -> 'a * T list;
 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
 
+
+(* read source *)
+
+fun read lex scan (syms, pos) =
+  Source.of_list syms
+  |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+  |> source_proper
+  |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
+  |> Source.exhaust;
+
+fun read_antiq lex scan (syms, pos) =
+  let
+    fun err msg =
+      cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
+        "@{" ^ Symbol_Pos.content syms ^ "}");
+    val res = read lex scan (syms, pos) handle ERROR msg => err msg;
+  in (case res of [x] => x | _ => err "") end;
+
+
+(* wrapped syntax *)
+
 fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
   let
     val args1 = map init_assignable args0;
diff -r b5cdfb352814 -r 930727de976c src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Aug 27 14:55:33 2014 +0200
@@ -52,6 +52,16 @@
           ML_Syntax.atomic (ML_Syntax.print_term t))));
 
 
+(* embedded source *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.value @{binding source}
+    (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} =>
+      "{delimited = " ^ Bool.toString delimited ^
+      ", text = " ^ ML_Syntax.print_string text ^
+      ", pos = " ^ ML_Syntax.print_position pos ^ "}")));
+
+
 (* ML support *)
 
 val _ = Theory.setup
diff -r b5cdfb352814 -r 930727de976c src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML	Wed Aug 27 14:55:33 2014 +0200
@@ -44,10 +44,10 @@
     (fn _ => fn raw_srcs => fn ctxt =>
       let
         val i = serial ();
-        val srcs = map (Attrib.check_src ctxt) raw_srcs;
-        val _ = map (Attrib.attribute ctxt) srcs;
+
         val (a, ctxt') = ctxt
-          |> ML_Antiquotation.variant "attributes" ||> put_attributes (i, srcs);
+          |> ML_Antiquotation.variant "attributes"
+          ||> put_attributes (i, Attrib.check_attribs ctxt raw_srcs);
         val ml =
           ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
             string_of_int i ^ ";\n", "Isabelle." ^ a);
diff -r b5cdfb352814 -r 930727de976c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Aug 27 14:55:33 2014 +0200
@@ -169,7 +169,7 @@
   val HIDDEN = "hidden"
 
 
-  /* logical entities */
+  /* misc entities */
 
   val CLASS = "class"
   val TYPE_NAME = "type_name"
diff -r b5cdfb352814 -r 930727de976c src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Aug 27 14:55:33 2014 +0200
@@ -185,10 +185,10 @@
   let
     fun parse_tree tree =
       let
-        val {delimited, text, pos} = token_source tree;
-        val syms = Symbol_Pos.explode (text, pos);
-        val _ = Context_Position.report ctxt pos (markup delimited);
-      in parse (syms, pos) end;
+        val source = token_source tree;
+        val syms = Symbol_Pos.source_explode source;
+        val _ = Context_Position.report ctxt (#pos source) (markup (#delimited source));
+      in parse (syms, #pos source) end;
   in
     (case YXML.parse_body str handle Fail msg => error msg of
       body as [tree as XML.Elem ((name, _), _)] =>
diff -r b5cdfb352814 -r 930727de976c src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Aug 27 14:55:33 2014 +0200
@@ -461,11 +461,11 @@
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
-    val {text, pos, ...} = Syntax.read_token str;
-    val syms = Symbol_Pos.explode (text, pos);
+    val source = Syntax.read_token str;
+    val syms = Symbol_Pos.source_explode source;
     val ast =
-      parse_asts ctxt true root (syms, pos)
-      |> uncurry (report_result ctxt pos)
+      parse_asts ctxt true root (syms, #pos source)
+      |> uncurry (report_result ctxt (#pos source))
       |> decode [];
     val _ = Context_Position.reports_text ctxt (! reports);
   in ast end;
diff -r b5cdfb352814 -r 930727de976c src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/simplifier.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Sequents/prover.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Tools/intuitionistic.ML	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 27 14:55:33 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 b5cdfb352814 -r 930727de976c src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Wed Aug 27 13:05:59 2014 +0200
+++ b/src/ZF/Tools/typechk.ML	Wed Aug 27 14:55:33 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";