more explicit Method.modifier with reported position;
authorwenzelm
Wed Aug 27 14:54:32 2014 +0200 (2014-08-27)
changeset 58048aa6296d09e0e
parent 58047 9f3826352b52
child 58049 930727de976c
more explicit Method.modifier with reported position;
src/HOL/Tools/recdef.ML
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/Isar/method.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/simplifier.ML
src/Sequents/prover.ML
src/Tools/intuitionistic.ML
src/Tools/jEdit/src/rendering.scala
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Tools/recdef.ML	Wed Aug 27 12:32:42 2014 +0200
     1.2 +++ b/src/HOL/Tools/recdef.ML	Wed Aug 27 14:54:32 2014 +0200
     1.3 @@ -143,15 +143,15 @@
     1.4  val recdef_wfN = "recdef_wf";
     1.5  
     1.6  val recdef_modifiers =
     1.7 - [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add): Method.modifier),
     1.8 -  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add),
     1.9 -  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del),
    1.10 -  Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add),
    1.11 -  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add),
    1.12 -  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del),
    1.13 -  Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add),
    1.14 -  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add),
    1.15 -  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del)] @
    1.16 + [Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
    1.17 +  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
    1.18 +  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
    1.19 +  Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add @{here}),
    1.20 +  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
    1.21 +  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here}),
    1.22 +  Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add @{here}),
    1.23 +  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add @{here}),
    1.24 +  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del @{here})] @
    1.25    Clasimp.clasimp_modifiers;
    1.26  
    1.27  
     2.1 --- a/src/Provers/clasimp.ML	Wed Aug 27 12:32:42 2014 +0200
     2.2 +++ b/src/Provers/clasimp.ML	Wed Aug 27 14:54:32 2014 +0200
     2.3 @@ -191,9 +191,9 @@
     2.4  val iffN = "iff";
     2.5  
     2.6  val iff_modifiers =
     2.7 - [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add): Method.modifier),
     2.8 -  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add'),
     2.9 -  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del)];
    2.10 + [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add @{here}),
    2.11 +  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' @{here}),
    2.12 +  Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del @{here})];
    2.13  
    2.14  val clasimp_modifiers =
    2.15    Simplifier.simp_modifiers @ Splitter.split_modifiers @
     3.1 --- a/src/Provers/classical.ML	Wed Aug 27 12:32:42 2014 +0200
     3.2 +++ b/src/Provers/classical.ML	Wed Aug 27 14:54:32 2014 +0200
     3.3 @@ -928,13 +928,13 @@
     3.4  (* automatic methods *)
     3.5  
     3.6  val cla_modifiers =
     3.7 - [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
     3.8 -  Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
     3.9 -  Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
    3.10 -  Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
    3.11 -  Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
    3.12 -  Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
    3.13 -  Args.del -- Args.colon >> K (I, rule_del)];
    3.14 + [Args.$$$ destN -- Args.bang_colon >> K (Method.modifier (safe_dest NONE) @{here}),
    3.15 +  Args.$$$ destN -- Args.colon >> K (Method.modifier (haz_dest NONE) @{here}),
    3.16 +  Args.$$$ elimN -- Args.bang_colon >> K (Method.modifier (safe_elim NONE) @{here}),
    3.17 +  Args.$$$ elimN -- Args.colon >> K (Method.modifier (haz_elim NONE) @{here}),
    3.18 +  Args.$$$ introN -- Args.bang_colon >> K (Method.modifier (safe_intro NONE) @{here}),
    3.19 +  Args.$$$ introN -- Args.colon >> K (Method.modifier (haz_intro NONE) @{here}),
    3.20 +  Args.del -- Args.colon >> K (Method.modifier rule_del @{here})];
    3.21  
    3.22  fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
    3.23  fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
     4.1 --- a/src/Provers/splitter.ML	Wed Aug 27 12:32:42 2014 +0200
     4.2 +++ b/src/Provers/splitter.ML	Wed Aug 27 14:54:32 2014 +0200
     4.3 @@ -457,9 +457,9 @@
     4.4  (* methods *)
     4.5  
     4.6  val split_modifiers =
     4.7 - [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier),
     4.8 -  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
     4.9 -  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
    4.10 + [Args.$$$ splitN -- Args.colon >> K (Method.modifier split_add @{here}),
    4.11 +  Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}),
    4.12 +  Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
    4.13  
    4.14  
    4.15  (* theory setup *)
     5.1 --- a/src/Pure/Isar/method.ML	Wed Aug 27 12:32:42 2014 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Wed Aug 27 14:54:32 2014 +0200
     5.3 @@ -67,7 +67,8 @@
     5.4    val method_closure: Proof.context -> Token.src -> Token.src
     5.5    val method_cmd: Proof.context -> Token.src -> Proof.context -> method
     5.6    val evaluate: text -> Proof.context -> method
     5.7 -  type modifier = (Proof.context -> Proof.context) * attribute
     5.8 +  type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
     5.9 +  val modifier: attribute -> Position.T -> modifier
    5.10    val section: modifier parser list -> declaration context_parser
    5.11    val sections: modifier parser list -> declaration list context_parser
    5.12    type text_range = text * Position.range
    5.13 @@ -448,13 +449,19 @@
    5.14  
    5.15  (** concrete syntax **)
    5.16  
    5.17 -(* sections *)
    5.18 +(* type modifier *)
    5.19 +
    5.20 +type modifier =
    5.21 +  {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T};
    5.22  
    5.23 -type modifier = (Proof.context -> Proof.context) * attribute;
    5.24 +fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos};
    5.25 +
    5.26 +
    5.27 +(* sections *)
    5.28  
    5.29  local
    5.30  
    5.31 -fun sect modifier = Scan.depend (fn context =>
    5.32 +fun sect (modifier : modifier parser) = Scan.depend (fn context =>
    5.33    let
    5.34      val ctxt = Context.proof_of context;
    5.35      fun prep_att src =
    5.36 @@ -466,7 +473,7 @@
    5.37        Parse.xthm >> (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs));
    5.38    in
    5.39      Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier parse_thm) >>
    5.40 -      (fn ((tok, (init, att)), thms) =>
    5.41 +      (fn ((tok, {init, attribute, pos}), thms) =>
    5.42          let
    5.43            val decl =
    5.44              (case Token.get_value tok of
    5.45 @@ -475,7 +482,11 @@
    5.46                  let
    5.47                    val facts =
    5.48                      Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
    5.49 -                    |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K att)]), bs));
    5.50 +                    |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
    5.51 +                  val _ =
    5.52 +                    Context_Position.report ctxt (Token.pos_of tok)
    5.53 +                      (Markup.entity Markup.method_modifierN ""
    5.54 +                        |> Markup.properties (Position.def_properties_of pos));
    5.55                    fun decl phi =
    5.56                      Context.mapping I init #>
    5.57                      Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
     6.1 --- a/src/Pure/PIDE/markup.ML	Wed Aug 27 12:32:42 2014 +0200
     6.2 +++ b/src/Pure/PIDE/markup.ML	Wed Aug 27 14:54:32 2014 +0200
     6.3 @@ -72,6 +72,7 @@
     6.4    val fixedN: string val fixed: string -> T
     6.5    val caseN: string val case_: string -> T
     6.6    val dynamic_factN: string val dynamic_fact: string -> T
     6.7 +  val method_modifierN: string
     6.8    val tfreeN: string val tfree: T
     6.9    val tvarN: string val tvar: T
    6.10    val freeN: string val free: T
    6.11 @@ -365,7 +366,7 @@
    6.12  val (hiddenN, hidden) = markup_elem "hidden";
    6.13  
    6.14  
    6.15 -(* formal entities *)
    6.16 +(* misc entities *)
    6.17  
    6.18  val system_optionN = "system_option";
    6.19  
    6.20 @@ -378,6 +379,8 @@
    6.21  val (caseN, case_) = markup_string "case" nameN;
    6.22  val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
    6.23  
    6.24 +val method_modifierN = "method_modifier";
    6.25 +
    6.26  
    6.27  (* inner syntax *)
    6.28  
     7.1 --- a/src/Pure/PIDE/markup.scala	Wed Aug 27 12:32:42 2014 +0200
     7.2 +++ b/src/Pure/PIDE/markup.scala	Wed Aug 27 14:54:32 2014 +0200
     7.3 @@ -169,7 +169,7 @@
     7.4    val HIDDEN = "hidden"
     7.5  
     7.6  
     7.7 -  /* logical entities */
     7.8 +  /* misc entities */
     7.9  
    7.10    val CLASS = "class"
    7.11    val TYPE_NAME = "type_name"
     8.1 --- a/src/Pure/simplifier.ML	Wed Aug 27 12:32:42 2014 +0200
     8.2 +++ b/src/Pure/simplifier.ML	Wed Aug 27 14:54:32 2014 +0200
     8.3 @@ -332,21 +332,23 @@
     8.4  (** method syntax **)
     8.5  
     8.6  val cong_modifiers =
     8.7 - [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
     8.8 -  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
     8.9 -  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
    8.10 + [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add @{here}),
    8.11 +  Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
    8.12 +  Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here})];
    8.13  
    8.14  val simp_modifiers =
    8.15 - [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
    8.16 -  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
    8.17 -  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
    8.18 -  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (Raw_Simplifier.clear_simpset, simp_add)]
    8.19 + [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
    8.20 +  Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
    8.21 +  Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
    8.22 +  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
    8.23 +    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
    8.24     @ cong_modifiers;
    8.25  
    8.26  val simp_modifiers' =
    8.27 - [Args.add -- Args.colon >> K (I, simp_add),
    8.28 -  Args.del -- Args.colon >> K (I, simp_del),
    8.29 -  Args.$$$ onlyN -- Args.colon >> K (Raw_Simplifier.clear_simpset, simp_add)]
    8.30 + [Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
    8.31 +  Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
    8.32 +  Args.$$$ onlyN -- Args.colon >>
    8.33 +    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
    8.34     @ cong_modifiers;
    8.35  
    8.36  val simp_options =
     9.1 --- a/src/Sequents/prover.ML	Wed Aug 27 12:32:42 2014 +0200
     9.2 +++ b/src/Sequents/prover.ML	Wed Aug 27 14:54:32 2014 +0200
     9.3 @@ -106,8 +106,8 @@
     9.4  
     9.5  fun method tac =
     9.6    Method.sections
     9.7 -   [Args.$$$ "add" -- Args.bang_colon >> K (I, safe_add),
     9.8 -    Args.$$$ "add" -- Args.colon >> K (I, unsafe_add)]
     9.9 +   [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add @{here}),
    9.10 +    Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add @{here})]
    9.11    >> K (SIMPLE_METHOD' o tac);
    9.12  
    9.13  
    10.1 --- a/src/Tools/intuitionistic.ML	Wed Aug 27 12:32:42 2014 +0200
    10.2 +++ b/src/Tools/intuitionistic.ML	Wed Aug 27 14:54:32 2014 +0200
    10.3 @@ -73,18 +73,18 @@
    10.4  val elimN = "elim";
    10.5  val destN = "dest";
    10.6  
    10.7 -fun modifier name kind kind' att =
    10.8 +fun modifier name kind kind' att pos =
    10.9    Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
   10.10 -    >> (pair (I: Proof.context -> Proof.context) o att);
   10.11 +    >> (fn arg => Method.modifier (att arg) pos);
   10.12  
   10.13  val modifiers =
   10.14 - [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
   10.15 -  modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
   10.16 -  modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
   10.17 -  modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
   10.18 -  modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
   10.19 -  modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
   10.20 -  Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
   10.21 + [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang @{here},
   10.22 +  modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest @{here},
   10.23 +  modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang @{here},
   10.24 +  modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim @{here},
   10.25 +  modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang @{here},
   10.26 +  modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro @{here},
   10.27 +  Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del @{here})];
   10.28  
   10.29  in
   10.30  
    11.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 27 12:32:42 2014 +0200
    11.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 27 14:54:32 2014 +0200
    11.3 @@ -480,7 +480,9 @@
    11.4              Some(Text.Info(r, (t1 + t2, info)))
    11.5            case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
    11.6              val kind1 = Word.implode(Word.explode('_', kind))
    11.7 -            val txt1 = kind1 + " " + quote(name)
    11.8 +            val txt1 =
    11.9 +              if (name == "") kind1
   11.10 +              else kind1 + " " + quote(name)
   11.11              val t = prev.info._1
   11.12              val txt2 =
   11.13                if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
    12.1 --- a/src/ZF/Tools/typechk.ML	Wed Aug 27 12:32:42 2014 +0200
    12.2 +++ b/src/ZF/Tools/typechk.ML	Wed Aug 27 14:54:32 2014 +0200
    12.3 @@ -115,8 +115,8 @@
    12.4  val typecheck_setup =
    12.5    Method.setup @{binding typecheck}
    12.6      (Method.sections
    12.7 -      [Args.add -- Args.colon >> K (I, TC_add),
    12.8 -       Args.del -- Args.colon >> K (I, TC_del)]
    12.9 +      [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}),
   12.10 +       Args.del -- Args.colon >> K (Method.modifier TC_del @{here})]
   12.11        >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
   12.12      "ZF type-checking";
   12.13