modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
authorwenzelm
Tue Feb 25 14:34:18 2014 +0100 (2014-02-25)
changeset 55742a989bdaf8121
parent 55741 b969263fcf02
child 55743 225a060e7445
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
removed obsolete Method.Source_i;
proper context for global data;
tuned messages;
src/Doc/antiquote_setup.ML
src/HOL/Tools/try0.ML
src/Pure/General/name_space.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Feb 25 12:53:08 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Feb 25 14:34:18 2014 +0100
     1.3 @@ -212,7 +212,7 @@
     1.4    entity_antiqs (K command_check) "isacommand" "command" #>
     1.5    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
     1.6    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
     1.7 -  entity_antiqs (thy_check Method.check) "" "method" #>
     1.8 +  entity_antiqs (can o Method.check_name) "" "method" #>
     1.9    entity_antiqs (thy_check Attrib.check) "" "attribute" #>
    1.10    entity_antiqs no_check "" "fact" #>
    1.11    entity_antiqs no_check "" "variable" #>
     2.1 --- a/src/HOL/Tools/try0.ML	Tue Feb 25 12:53:08 2014 +0100
     2.2 +++ b/src/HOL/Tools/try0.ML	Tue Feb 25 14:34:18 2014 +0100
     2.3 @@ -55,9 +55,10 @@
     2.4    #> Scan.read Token.stopper Method.parse
     2.5    #> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
     2.6  
     2.7 -fun apply_named_method_on_first_goal thy =
     2.8 +fun apply_named_method_on_first_goal ctxt =
     2.9    parse_method
    2.10 -  #> Method.method thy
    2.11 +  #> Method.check_source ctxt
    2.12 +  #> Method.the_method ctxt
    2.13    #> Method.Basic
    2.14    #> curry Method.Select_Goals 1
    2.15    #> Proof.refine;
    2.16 @@ -77,7 +78,7 @@
    2.17          ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
    2.18           (if all_goals andalso nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
    2.19          I (#goal o Proof.goal)
    2.20 -        (apply_named_method_on_first_goal (Proof.theory_of st) (name ^ attrs)) st
    2.21 +        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)) st
    2.22      end
    2.23    else
    2.24      NONE;
     3.1 --- a/src/Pure/General/name_space.ML	Tue Feb 25 12:53:08 2014 +0100
     3.2 +++ b/src/Pure/General/name_space.ML	Tue Feb 25 14:34:18 2014 +0100
     3.3 @@ -1,8 +1,8 @@
     3.4  (*  Title:      Pure/General/name_space.ML
     3.5      Author:     Markus Wenzel, TU Muenchen
     3.6  
     3.7 -Generic name spaces with declared and hidden entries.  Unknown names
     3.8 -are considered global; no support for absolute addressing.
     3.9 +Generic name spaces with declared and hidden entries; no support for
    3.10 +absolute addressing.
    3.11  *)
    3.12  
    3.13  type xstring = string;    (*external names*)
    3.14 @@ -120,7 +120,7 @@
    3.15  
    3.16  fun the_entry (Name_Space {kind, entries, ...}) name =
    3.17    (case Symtab.lookup entries name of
    3.18 -    NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
    3.19 +    NONE => error (undefined kind name)
    3.20    | SOME (_, entry) => entry);
    3.21  
    3.22  fun entry_ord space = int_ord o pairself (#id o the_entry space);
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Feb 25 12:53:08 2014 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 25 14:34:18 2014 +0100
     4.3 @@ -809,7 +809,7 @@
     4.4  val _ =
     4.5    Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
     4.6      (Scan.succeed (Toplevel.unknown_theory o
     4.7 -      Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
     4.8 +      Toplevel.keep (Method.print_methods o Toplevel.context_of)));
     4.9  
    4.10  val _ =
    4.11    Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
     5.1 --- a/src/Pure/Isar/method.ML	Tue Feb 25 12:53:08 2014 +0100
     5.2 +++ b/src/Pure/Isar/method.ML	Tue Feb 25 14:34:18 2014 +0100
     5.3 @@ -46,9 +46,8 @@
     5.4    val raw_tactic: string * Position.T -> Proof.context -> method
     5.5    type src = Args.src
     5.6    datatype text =
     5.7 +    Source of src |
     5.8      Basic of Proof.context -> method |
     5.9 -    Source of src |
    5.10 -    Source_i of src |
    5.11      Then of text list |
    5.12      Orelse of text list |
    5.13      Try of text |
    5.14 @@ -61,11 +60,10 @@
    5.15    val done_text: text
    5.16    val sorry_text: bool -> text
    5.17    val finish_text: text option * bool -> text
    5.18 -  val print_methods: theory -> unit
    5.19 -  val check: theory -> xstring * Position.T -> string
    5.20 -  val intern: theory -> xstring -> string
    5.21 -  val method: theory -> src -> Proof.context -> method
    5.22 -  val method_i: theory -> src -> Proof.context -> method
    5.23 +  val print_methods: Proof.context -> unit
    5.24 +  val the_method: Proof.context -> src -> Proof.context -> method
    5.25 +  val check_name: Proof.context -> xstring * Position.T -> string
    5.26 +  val check_source: Proof.context -> src -> src
    5.27    val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    5.28    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
    5.29    val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
    5.30 @@ -284,9 +282,8 @@
    5.31  type src = Args.src;
    5.32  
    5.33  datatype text =
    5.34 +  Source of src |
    5.35    Basic of Proof.context -> method |
    5.36 -  Source of src |
    5.37 -  Source_i of src |
    5.38    Then of text list |
    5.39    Orelse of text list |
    5.40    Try of text |
    5.41 @@ -314,10 +311,11 @@
    5.42    fun merge data : T = Name_Space.merge_tables data;
    5.43  );
    5.44  
    5.45 -fun print_methods thy =
    5.46 +val get_methods = Methods.get o Proof_Context.theory_of;
    5.47 +
    5.48 +fun print_methods ctxt =
    5.49    let
    5.50 -    val ctxt = Proof_Context.init_global thy;
    5.51 -    val meths = Methods.get thy;
    5.52 +    val meths = get_methods ctxt;
    5.53      fun prt_meth (name, (_, "")) = Pretty.mark_str name
    5.54        | prt_meth (name, (_, comment)) =
    5.55            Pretty.block
    5.56 @@ -330,25 +328,26 @@
    5.57  fun add_method name meth comment thy = thy
    5.58    |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
    5.59  
    5.60 -
    5.61 -(* get methods *)
    5.62 -
    5.63 -fun check thy = #1 o Name_Space.check (Context.Theory thy) (Methods.get thy);
    5.64 -
    5.65 -val intern = Name_Space.intern o #1 o Methods.get;
    5.66 -
    5.67 -fun method_i thy =
    5.68 -  let
    5.69 -    val (space, tab) = Methods.get thy;
    5.70 -    fun meth src =
    5.71 +fun the_method ctxt =
    5.72 +  let val (_, tab) = get_methods ctxt in
    5.73 +    fn src =>
    5.74        let val ((name, _), pos) = Args.dest_src src in
    5.75          (case Symtab.lookup tab name of
    5.76 -          NONE => error ("Unknown proof method: " ^ quote name ^ Position.here pos)
    5.77 -        | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src))
    5.78 -      end;
    5.79 -  in meth end;
    5.80 +          NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
    5.81 +        | SOME (method, _) => method src)
    5.82 +      end
    5.83 +  end;
    5.84 +
    5.85 +
    5.86 +(* check *)
    5.87  
    5.88 -fun method thy = method_i thy o Args.map_name (intern thy);
    5.89 +fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
    5.90 +
    5.91 +fun check_source ctxt src =
    5.92 +  let
    5.93 +    val ((xname, toks), pos) = Args.dest_src src;
    5.94 +    val name = check_name ctxt (xname, pos);
    5.95 +  in Args.src ((name, toks), pos) end;
    5.96  
    5.97  
    5.98  (* method setup *)
    5.99 @@ -406,7 +405,6 @@
   5.100  
   5.101  fun meth4 x =
   5.102   (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
   5.103 -  (* FIXME implicit "cartouche" method (experimental, undocumented) *)
   5.104    Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
   5.105      Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
   5.106    Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
     6.1 --- a/src/Pure/Isar/proof.ML	Tue Feb 25 12:53:08 2014 +0100
     6.2 +++ b/src/Pure/Isar/proof.ML	Tue Feb 25 14:34:18 2014 +0100
     6.3 @@ -392,13 +392,13 @@
     6.4    Rule_Cases.make_common
     6.5      (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
     6.6  
     6.7 -fun apply_method current_context meth state =
     6.8 +fun apply_method current_context method state =
     6.9    let
    6.10      val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
    6.11        find_goal state;
    6.12      val ctxt = if current_context then context_of state else goal_ctxt;
    6.13    in
    6.14 -    Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
    6.15 +    Method.apply method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
    6.16        state
    6.17        |> map_goal
    6.18            (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
    6.19 @@ -416,13 +416,13 @@
    6.20        |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state')))))
    6.21      |> Seq.maps (apply_method true (K Method.succeed)));
    6.22  
    6.23 -fun apply_text cc text state =
    6.24 +fun apply_text current_context text state =
    6.25    let
    6.26 -    val thy = theory_of state;
    6.27 +    val ctxt = context_of state;
    6.28  
    6.29 -    fun eval (Method.Basic m) = apply_method cc m
    6.30 -      | eval (Method.Source src) = apply_method cc (Method.method thy src)
    6.31 -      | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
    6.32 +    fun eval (Method.Basic m) = apply_method current_context m
    6.33 +      | eval (Method.Source src) =
    6.34 +          apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src))
    6.35        | eval (Method.Then txts) = Seq.EVERY (map eval txts)
    6.36        | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
    6.37        | eval (Method.Try txt) = Seq.TRY (eval txt)