--- a/src/Doc/antiquote_setup.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Thu Nov 06 13:36:19 2014 +0100
@@ -191,6 +191,9 @@
fun no_check _ _ = true;
+fun is_keyword _ (name, _) =
+ Keyword.is_keyword (Keyword.get_keywords ()) name;
+
fun check_command ctxt (name, pos) =
is_some (Keyword.command_keyword name) andalso
let
@@ -259,8 +262,8 @@
Theory.setup
(entity_antiqs no_check "" @{binding syntax} #>
entity_antiqs check_command "isacommand" @{binding command} #>
- entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
- entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
+ entity_antiqs is_keyword "isakeyword" @{binding keyword} #>
+ entity_antiqs is_keyword "isakeyword" @{binding element} #>
entity_antiqs (can o Method.check_name) "" @{binding method} #>
entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #>
entity_antiqs no_check "" @{binding fact} #>
--- a/src/HOL/Tools/ATP/atp_util.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Nov 06 13:36:19 2014 +0100
@@ -140,7 +140,7 @@
let val s = unyxml y in
y |> ((not (is_long_identifier (unquote_tvar s)) andalso
not (is_long_identifier (unquery_var s))) orelse
- Keyword.is_keyword s) ? quote
+ Keyword.is_keyword (Keyword.get_keywords ()) s) ? quote
end
fun string_of_ext_time (plus, time) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 06 13:36:19 2014 +0100
@@ -267,10 +267,10 @@
val {facts = chained, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
val ho_atp = exists (is_ho_atp ctxt) provers
- val reserved = reserved_isar_keyword_table ()
+ val keywords = Keyword.get_keywords ()
val css = clasimpset_rule_table_of ctxt
val all_facts =
- nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts concl_t
+ nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t
val _ = () |> not blocking ? kill_provers
val _ =
(case find_first (not o is_prover_supported ctxt) provers of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Nov 06 13:36:19 2014 +0100
@@ -21,7 +21,7 @@
val instantiate_inducts : bool Config.T
val no_fact_override : fact_override
- val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table ->
+ val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table ->
Facts.ref * Token.src list -> ((string * stature) * thm) list
val backquote_thm : Proof.context -> thm -> string
val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
@@ -33,9 +33,9 @@
val fact_of_raw_fact : raw_fact -> fact
val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
- val all_facts : Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list ->
+ val all_facts : Proof.context -> bool -> bool -> Keyword.keywords -> thm list -> thm list ->
status Termtab.table -> raw_fact list
- val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table ->
+ val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords ->
status Termtab.table -> thm list -> term list -> term -> raw_fact list
val drop_duplicate_facts : raw_fact list -> raw_fact list
end;
@@ -66,12 +66,12 @@
val no_fact_override = {add = [], del = [], only = false}
-fun needs_quoting reserved s =
- Symtab.defined reserved s orelse
+fun needs_quoting keywords s =
+ Keyword.is_keyword keywords s orelse
exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
-fun make_name reserved multi j name =
- (name |> needs_quoting reserved name ? quote) ^
+fun make_name keywords multi j name =
+ (name |> needs_quoting keywords name ? quote) ^
(if multi then "(" ^ string_of_int j ^ ")" else "")
fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
@@ -157,7 +157,7 @@
fun stature_of_thm global assms chained css name th =
(scope_of_thm global assms chained th, status_of_thm css name th)
-fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
+fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
@@ -166,9 +166,9 @@
(case xref of
Facts.Fact s => backquote (simplify_spaces (unyxml s)) ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
- | Facts.Named ((name, _), NONE) => make_name reserved (length ths > 1) (j + 1) name ^ bracket
+ | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
| Facts.Named ((name, _), SOME intervals) =>
- make_name reserved true
+ make_name keywords true
(nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
fun add_nth th (j, rest) =
@@ -455,7 +455,7 @@
forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
end
-fun all_facts ctxt generous ho_atp reserved add_ths chained css =
+fun all_facts ctxt generous ho_atp keywords add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -514,7 +514,7 @@
name0
end
end
- |> make_name reserved multi j
+ |> make_name keywords multi j
val stature = stature_of_thm global assms chained css name0 th
val new = ((get_name, stature), th)
in
@@ -530,7 +530,7 @@
|> op @
end
-fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t =
+fun nearly_all_facts ctxt ho_atp {add, del, only} keywords css chained hyp_ts concl_t =
if only andalso null add then
[]
else
@@ -539,12 +539,12 @@
in
(if only then
maps (map (fn ((name, stature), th) => ((K name, stature), th))
- o fact_of_ref ctxt reserved chained css) add
+ o fact_of_ref ctxt keywords chained css) add
else
let
val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
val facts =
- all_facts ctxt false ho_atp reserved add chained css
+ all_facts ctxt false ho_atp keywords add chained css
|> filter_out ((member Thm.eq_thm_prop del orf
(Named_Theorems.member ctxt @{named_theorems no_atp} andf
not o member Thm.eq_thm_prop add)) o snd)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 06 13:36:19 2014 +0100
@@ -1467,7 +1467,8 @@
let
val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val ctxt = ctxt |> Config.put instantiate_inducts false
- val facts = nearly_all_facts ctxt false fact_override Symtab.empty css chained [] @{prop True}
+ val facts =
+ nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True}
|> sort (crude_thm_ord o pairself snd o swap)
val num_facts = length facts
val prover = hd provers
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Nov 06 13:36:19 2014 +0100
@@ -17,7 +17,6 @@
val parse_bool_option : bool -> string -> string -> bool option
val parse_time : string -> string -> Time.time
val subgoal_count : Proof.state -> int
- val reserved_isar_keyword_table : unit -> unit Symtab.table
val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
string list option
val thms_of_name : Proof.context -> string -> thm list
@@ -79,9 +78,6 @@
val subgoal_count = Try.subgoal_count
-fun reserved_isar_keyword_table () =
- Symtab.make_set (Scan.dest_lexicon (Scan.merge_lexicons (Keyword.get_lexicons ())));
-
exception TOO_MANY of unit
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to
--- a/src/Pure/Isar/keyword.ML Thu Nov 06 11:44:41 2014 +0100
+++ b/src/Pure/Isar/keyword.ML Thu Nov 06 13:36:19 2014 +0100
@@ -43,8 +43,7 @@
val add: string * T option -> keywords -> keywords
val define: string * T option -> unit
val get_keywords: unit -> keywords
- val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
- val is_keyword: string -> bool
+ val is_keyword: keywords -> string -> bool
val command_keyword: string -> T option
val command_files: string -> Path.T -> Path.T list
val command_tags: string -> string list
@@ -182,18 +181,15 @@
end;
-fun get_lexicons () =
- let val keywords = get_keywords ()
- in (minor_keywords keywords, major_keywords keywords) end;
-
fun get_commands () = commands (get_keywords ());
(* lookup *)
-fun is_keyword s =
+fun is_keyword keywords s =
let
- val (minor, major) = get_lexicons ();
+ val minor = minor_keywords keywords;
+ val major = major_keywords keywords;
val syms = Symbol.explode s;
in Scan.is_literal minor syms orelse Scan.is_literal major syms end;