# HG changeset patch # User wenzelm # Date 1415277379 -3600 # Node ID 82a71046dce8660f80cbc289c33b65b194bc14b1 # Parent 8d36bc5eaed322101b993cb1dc5fd46b4160f624 prefer explicit Keyword.keywords; diff -r 8d36bc5eaed3 -r 82a71046dce8 src/Doc/antiquote_setup.ML --- 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} #> diff -r 8d36bc5eaed3 -r 82a71046dce8 src/HOL/Tools/ATP/atp_util.ML --- 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) = diff -r 8d36bc5eaed3 -r 82a71046dce8 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 diff -r 8d36bc5eaed3 -r 82a71046dce8 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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) diff -r 8d36bc5eaed3 -r 82a71046dce8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 8d36bc5eaed3 -r 82a71046dce8 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 diff -r 8d36bc5eaed3 -r 82a71046dce8 src/Pure/Isar/keyword.ML --- 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;