# HG changeset patch # User wenzelm # Date 1462911906 -7200 # Node ID 8326aa594273ccaea5290e879707443d984cb8e9 # Parent e9ad90ce926c4bbfa15538396871b962946a4c24 find dynamic facts as well, but static ones are preferred; tuned; diff -r e9ad90ce926c -r 8326aa594273 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue May 10 15:48:37 2016 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue May 10 22:25:06 2016 +0200 @@ -63,7 +63,7 @@ val background_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context val facts_of: Proof.context -> Facts.T val facts_of_fact: Proof.context -> string -> Facts.T - val markup_extern_fact: Proof.context -> string -> Markup.T * xstring + val markup_extern_fact: Proof.context -> string -> Markup.T list * xstring val pretty_term_abbrev: Proof.context -> term -> Pretty.T val pretty_fact: Proof.context -> string * thm list -> Pretty.T val check_class: Proof.context -> xstring * Position.T -> class * Position.report list @@ -410,7 +410,13 @@ end; fun markup_extern_fact ctxt name = - Facts.markup_extern ctxt (facts_of_fact ctxt name) name; + let + val facts = facts_of_fact ctxt name; + val (markup, xname) = Facts.markup_extern ctxt facts name; + val markups = + if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name] + else [markup]; + in (markups, xname) end; @@ -419,7 +425,7 @@ fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); fun pretty_fact_name ctxt a = - Pretty.block [Pretty.mark_str (markup_extern_fact ctxt a), Pretty.str ":"]; + Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"]; fun pretty_fact ctxt = let diff -r e9ad90ce926c -r 8326aa594273 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Tue May 10 15:48:37 2016 +0200 +++ b/src/Pure/Tools/find_theorems.ML Tue May 10 22:25:06 2016 +0200 @@ -335,10 +335,12 @@ val qual_ord = int_ord o apply2 Long_Name.qualification; val txt_ord = int_ord o apply2 size; -fun nicer_name (x, i) (y, j) = - (case hidden_ord (x, y) of EQUAL => - (case index_ord (i, j) of EQUAL => - (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) +fun nicer_name ((a, x), i) ((b, y), j) = + (case bool_ord (a, b) of EQUAL => + (case hidden_ord (x, y) of EQUAL => + (case index_ord (i, j) of EQUAL => + (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) + | ord => ord) | ord => ord) | ord => ord) <> GREATER; @@ -357,8 +359,10 @@ fun nicer_shortest ctxt = let fun extern_shortest name = - Name_Space.extern_shortest ctxt - (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name; + let + val facts = Proof_Context.facts_of_fact ctxt name; + val space = Facts.space_of facts; + in (Facts.is_dynamic facts name, Name_Space.extern_shortest ctxt space name) end; fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = nicer_name (extern_shortest x, i) (extern_shortest y, j) @@ -389,8 +393,8 @@ val local_facts = Proof_Context.facts_of ctxt; val global_facts = Global_Theory.facts_of thy; in - (Facts.dest_static false [global_facts] local_facts @ - Facts.dest_static false [] global_facts) + (Facts.dest_all (Context.Proof ctxt) false [global_facts] local_facts @ + Facts.dest_all (Context.Proof ctxt) false [] global_facts) |> maps Facts.selections |> map (apsnd transfer) end; @@ -459,7 +463,7 @@ Facts.Named ((name, _), sel) => (name, sel) | Facts.Fact _ => raise Fail "Illegal literal fact"); in - [Pretty.mark (#1 (Proof_Context.markup_extern_fact ctxt name)) (Pretty.str name), + [Pretty.marks_str (#1 (Proof_Context.markup_extern_fact ctxt name), name), Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1] end; diff -r e9ad90ce926c -r 8326aa594273 src/Pure/facts.ML --- a/src/Pure/facts.ML Tue May 10 15:48:37 2016 +0200 +++ b/src/Pure/facts.ML Tue May 10 22:25:06 2016 +0200 @@ -28,12 +28,14 @@ val intern: T -> xstring -> string val extern: Proof.context -> T -> string -> xstring val markup_extern: Proof.context -> T -> string -> Markup.T * xstring + val defined: T -> string -> bool + val is_dynamic: T -> string -> bool val lookup: Context.generic -> T -> string -> (bool * thm list) option val retrieve: Context.generic -> T -> xstring * Position.T -> {name: string, static: bool, thms: thm list} - val defined: T -> string -> bool val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a val dest_static: bool -> T list -> T -> (string * thm list) list + val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list val props: T -> thm list val could_unify: T -> term -> thm list val merge: T * T -> T @@ -168,6 +170,11 @@ val defined = Name_Space.defined o facts_of; +fun is_dynamic facts name = + (case Name_Space.lookup (facts_of facts) name of + SOME (Dynamic _) => true + | _ => false); + fun lookup context facts name = (case Name_Space.lookup (facts_of facts) name of NONE => NONE @@ -191,18 +198,31 @@ end; -(* static content *) +(* content *) + +local + +fun included verbose prev_facts facts name = + not (exists (fn prev => defined prev name) prev_facts orelse + not verbose andalso is_concealed facts name); + +in fun fold_static f = - Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of; + Name_Space.fold_table (fn (a, Static ths) => f (a, ths) | _ => I) o facts_of; fun dest_static verbose prev_facts facts = - fold_static (fn (name, ths) => - if exists (fn prev => defined prev name) prev_facts orelse - not verbose andalso is_concealed facts name then I - else cons (name, ths)) facts [] + fold_static (fn (a, ths) => included verbose prev_facts facts a ? cons (a, ths)) facts [] |> sort_by #1; +fun dest_all context verbose prev_facts facts = + Name_Space.fold_table (fn (a, fact) => + let val ths = (case fact of Static ths => ths | Dynamic f => f context) + in included verbose prev_facts facts a ? cons (a, ths) end) (facts_of facts) [] + |> sort_by #1; + +end; + (* indexed props *)