1.1 --- a/src/Doc/antiquote_setup.ML Thu Nov 06 11:44:41 2014 +0100
1.2 +++ b/src/Doc/antiquote_setup.ML Thu Nov 06 13:36:19 2014 +0100
1.3 @@ -191,6 +191,9 @@
1.4
1.5 fun no_check _ _ = true;
1.6
1.7 +fun is_keyword _ (name, _) =
1.8 + Keyword.is_keyword (Keyword.get_keywords ()) name;
1.9 +
1.10 fun check_command ctxt (name, pos) =
1.11 is_some (Keyword.command_keyword name) andalso
1.12 let
1.13 @@ -259,8 +262,8 @@
1.14 Theory.setup
1.15 (entity_antiqs no_check "" @{binding syntax} #>
1.16 entity_antiqs check_command "isacommand" @{binding command} #>
1.17 - entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
1.18 - entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
1.19 + entity_antiqs is_keyword "isakeyword" @{binding keyword} #>
1.20 + entity_antiqs is_keyword "isakeyword" @{binding element} #>
1.21 entity_antiqs (can o Method.check_name) "" @{binding method} #>
1.22 entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #>
1.23 entity_antiqs no_check "" @{binding fact} #>
2.1 --- a/src/HOL/Tools/ATP/atp_util.ML Thu Nov 06 11:44:41 2014 +0100
2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Thu Nov 06 13:36:19 2014 +0100
2.3 @@ -140,7 +140,7 @@
2.4 let val s = unyxml y in
2.5 y |> ((not (is_long_identifier (unquote_tvar s)) andalso
2.6 not (is_long_identifier (unquery_var s))) orelse
2.7 - Keyword.is_keyword s) ? quote
2.8 + Keyword.is_keyword (Keyword.get_keywords ()) s) ? quote
2.9 end
2.10
2.11 fun string_of_ext_time (plus, time) =
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 06 11:44:41 2014 +0100
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 06 13:36:19 2014 +0100
3.3 @@ -267,10 +267,10 @@
3.4 val {facts = chained, goal, ...} = Proof.goal state
3.5 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
3.6 val ho_atp = exists (is_ho_atp ctxt) provers
3.7 - val reserved = reserved_isar_keyword_table ()
3.8 + val keywords = Keyword.get_keywords ()
3.9 val css = clasimpset_rule_table_of ctxt
3.10 val all_facts =
3.11 - nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts concl_t
3.12 + nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t
3.13 val _ = () |> not blocking ? kill_provers
3.14 val _ =
3.15 (case find_first (not o is_prover_supported ctxt) provers of
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Nov 06 11:44:41 2014 +0100
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Nov 06 13:36:19 2014 +0100
4.3 @@ -21,7 +21,7 @@
4.4 val instantiate_inducts : bool Config.T
4.5 val no_fact_override : fact_override
4.6
4.7 - val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table ->
4.8 + val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table ->
4.9 Facts.ref * Token.src list -> ((string * stature) * thm) list
4.10 val backquote_thm : Proof.context -> thm -> string
4.11 val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
4.12 @@ -33,9 +33,9 @@
4.13 val fact_of_raw_fact : raw_fact -> fact
4.14 val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
4.15
4.16 - val all_facts : Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list ->
4.17 + val all_facts : Proof.context -> bool -> bool -> Keyword.keywords -> thm list -> thm list ->
4.18 status Termtab.table -> raw_fact list
4.19 - val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table ->
4.20 + val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords ->
4.21 status Termtab.table -> thm list -> term list -> term -> raw_fact list
4.22 val drop_duplicate_facts : raw_fact list -> raw_fact list
4.23 end;
4.24 @@ -66,12 +66,12 @@
4.25
4.26 val no_fact_override = {add = [], del = [], only = false}
4.27
4.28 -fun needs_quoting reserved s =
4.29 - Symtab.defined reserved s orelse
4.30 +fun needs_quoting keywords s =
4.31 + Keyword.is_keyword keywords s orelse
4.32 exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
4.33
4.34 -fun make_name reserved multi j name =
4.35 - (name |> needs_quoting reserved name ? quote) ^
4.36 +fun make_name keywords multi j name =
4.37 + (name |> needs_quoting keywords name ? quote) ^
4.38 (if multi then "(" ^ string_of_int j ^ ")" else "")
4.39
4.40 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
4.41 @@ -157,7 +157,7 @@
4.42 fun stature_of_thm global assms chained css name th =
4.43 (scope_of_thm global assms chained th, status_of_thm css name th)
4.44
4.45 -fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
4.46 +fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) =
4.47 let
4.48 val ths = Attrib.eval_thms ctxt [xthm]
4.49 val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
4.50 @@ -166,9 +166,9 @@
4.51 (case xref of
4.52 Facts.Fact s => backquote (simplify_spaces (unyxml s)) ^ bracket
4.53 | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
4.54 - | Facts.Named ((name, _), NONE) => make_name reserved (length ths > 1) (j + 1) name ^ bracket
4.55 + | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
4.56 | Facts.Named ((name, _), SOME intervals) =>
4.57 - make_name reserved true
4.58 + make_name keywords true
4.59 (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
4.60
4.61 fun add_nth th (j, rest) =
4.62 @@ -455,7 +455,7 @@
4.63 forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
4.64 end
4.65
4.66 -fun all_facts ctxt generous ho_atp reserved add_ths chained css =
4.67 +fun all_facts ctxt generous ho_atp keywords add_ths chained css =
4.68 let
4.69 val thy = Proof_Context.theory_of ctxt
4.70 val global_facts = Global_Theory.facts_of thy
4.71 @@ -514,7 +514,7 @@
4.72 name0
4.73 end
4.74 end
4.75 - |> make_name reserved multi j
4.76 + |> make_name keywords multi j
4.77 val stature = stature_of_thm global assms chained css name0 th
4.78 val new = ((get_name, stature), th)
4.79 in
4.80 @@ -530,7 +530,7 @@
4.81 |> op @
4.82 end
4.83
4.84 -fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t =
4.85 +fun nearly_all_facts ctxt ho_atp {add, del, only} keywords css chained hyp_ts concl_t =
4.86 if only andalso null add then
4.87 []
4.88 else
4.89 @@ -539,12 +539,12 @@
4.90 in
4.91 (if only then
4.92 maps (map (fn ((name, stature), th) => ((K name, stature), th))
4.93 - o fact_of_ref ctxt reserved chained css) add
4.94 + o fact_of_ref ctxt keywords chained css) add
4.95 else
4.96 let
4.97 val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
4.98 val facts =
4.99 - all_facts ctxt false ho_atp reserved add chained css
4.100 + all_facts ctxt false ho_atp keywords add chained css
4.101 |> filter_out ((member Thm.eq_thm_prop del orf
4.102 (Named_Theorems.member ctxt @{named_theorems no_atp} andf
4.103 not o member Thm.eq_thm_prop add)) o snd)
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 06 11:44:41 2014 +0100
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 06 13:36:19 2014 +0100
5.3 @@ -1467,7 +1467,8 @@
5.4 let
5.5 val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
5.6 val ctxt = ctxt |> Config.put instantiate_inducts false
5.7 - val facts = nearly_all_facts ctxt false fact_override Symtab.empty css chained [] @{prop True}
5.8 + val facts =
5.9 + nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True}
5.10 |> sort (crude_thm_ord o pairself snd o swap)
5.11 val num_facts = length facts
5.12 val prover = hd provers
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Nov 06 11:44:41 2014 +0100
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Nov 06 13:36:19 2014 +0100
6.3 @@ -17,7 +17,6 @@
6.4 val parse_bool_option : bool -> string -> string -> bool option
6.5 val parse_time : string -> string -> Time.time
6.6 val subgoal_count : Proof.state -> int
6.7 - val reserved_isar_keyword_table : unit -> unit Symtab.table
6.8 val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
6.9 string list option
6.10 val thms_of_name : Proof.context -> string -> thm list
6.11 @@ -79,9 +78,6 @@
6.12
6.13 val subgoal_count = Try.subgoal_count
6.14
6.15 -fun reserved_isar_keyword_table () =
6.16 - Symtab.make_set (Scan.dest_lexicon (Scan.merge_lexicons (Keyword.get_lexicons ())));
6.17 -
6.18 exception TOO_MANY of unit
6.19
6.20 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to
7.1 --- a/src/Pure/Isar/keyword.ML Thu Nov 06 11:44:41 2014 +0100
7.2 +++ b/src/Pure/Isar/keyword.ML Thu Nov 06 13:36:19 2014 +0100
7.3 @@ -43,8 +43,7 @@
7.4 val add: string * T option -> keywords -> keywords
7.5 val define: string * T option -> unit
7.6 val get_keywords: unit -> keywords
7.7 - val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
7.8 - val is_keyword: string -> bool
7.9 + val is_keyword: keywords -> string -> bool
7.10 val command_keyword: string -> T option
7.11 val command_files: string -> Path.T -> Path.T list
7.12 val command_tags: string -> string list
7.13 @@ -182,18 +181,15 @@
7.14
7.15 end;
7.16
7.17 -fun get_lexicons () =
7.18 - let val keywords = get_keywords ()
7.19 - in (minor_keywords keywords, major_keywords keywords) end;
7.20 -
7.21 fun get_commands () = commands (get_keywords ());
7.22
7.23
7.24 (* lookup *)
7.25
7.26 -fun is_keyword s =
7.27 +fun is_keyword keywords s =
7.28 let
7.29 - val (minor, major) = get_lexicons ();
7.30 + val minor = minor_keywords keywords;
7.31 + val major = major_keywords keywords;
7.32 val syms = Symbol.explode s;
7.33 in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
7.34