disallow duplicate entries (weak version for merge);
authorwenzelm
Tue Apr 15 16:12:11 2008 +0200 (2008-04-15)
changeset 266541f711934f221
parent 26653 60e0cf6bef89
child 26655 750bab48223d
disallow duplicate entries (weak version for merge);
added hide;
src/Pure/facts.ML
     1.1 --- a/src/Pure/facts.ML	Tue Apr 15 16:12:05 2008 +0200
     1.2 +++ b/src/Pure/facts.ML	Tue Apr 15 16:12:11 2008 +0200
     1.3 @@ -28,10 +28,11 @@
     1.4    val props: T -> thm list
     1.5    val could_unify: T -> term -> thm list
     1.6    val merge: T * T -> T
     1.7 -  val del: string -> T -> T
     1.8    val add_global: NameSpace.naming -> string * thm list -> T -> T
     1.9    val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
    1.10    val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
    1.11 +  val del: string -> T -> T
    1.12 +  val hide: bool -> string -> T -> T
    1.13  end;
    1.14  
    1.15  structure Facts: FACTS =
    1.16 @@ -159,23 +160,18 @@
    1.17  
    1.18  fun err_dup_fact name = error ("Duplicate fact " ^ quote name);
    1.19  
    1.20 +fun eq_entry ((Static ths1, _), (Static ths2, _)) = is_equal (list_ord Thm.thm_ord (ths1, ths2))
    1.21 +  | eq_entry ((_, id1: serial), (_, id2)) = id1 = id2;
    1.22 +
    1.23  fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
    1.24    let
    1.25 -    (* FIXME authentic version
    1.26 -    val facts' = NameSpace.merge_tables (eq_snd (op =)) (facts1, facts2)
    1.27 -      handle Symtab.DUP dup => err_dup_fact dup; *)
    1.28 -    val facts' = NameSpace.merge_tables (K true) (facts1, facts2)
    1.29 +    val facts' = NameSpace.merge_tables eq_entry (facts1, facts2)
    1.30 +      handle Symtab.DUP dup => err_dup_fact dup;
    1.31      val props' = Net.merge (is_equal o prop_ord) (props1, props2);
    1.32    in make_facts facts' props' end;
    1.33  
    1.34  
    1.35 -(* static entries *)
    1.36 -
    1.37 -fun del name (Facts {facts = (space, tab), props}) =
    1.38 -  let
    1.39 -    val space' = NameSpace.hide true name space handle ERROR _ => space;
    1.40 -    val tab' = Symtab.delete_safe name tab;
    1.41 -  in make_facts (space', tab') props end;
    1.42 +(* add static entries *)
    1.43  
    1.44  fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
    1.45    let
    1.46 @@ -187,8 +183,7 @@
    1.47            val space' = NameSpace.declare naming name space;
    1.48            val entry = (name, (Static ths, serial ()));
    1.49            val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
    1.50 -            handle Symtab.DUP dup => (legacy_feature ("Duplicate fact " ^ quote dup ^
    1.51 -              Position.str_of (Position.thread_data ())); tab);
    1.52 +            handle Symtab.DUP dup => err_dup_fact dup;
    1.53          in (space', tab') end;
    1.54      val props' =
    1.55        if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
    1.56 @@ -199,7 +194,7 @@
    1.57  val add_local = add true;
    1.58  
    1.59  
    1.60 -(* dynamic entries *)
    1.61 +(* add dynamic entries *)
    1.62  
    1.63  fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
    1.64    let
    1.65 @@ -209,4 +204,16 @@
    1.66        handle Symtab.DUP dup => err_dup_fact dup;
    1.67    in make_facts (space', tab') props end;
    1.68  
    1.69 +
    1.70 +(* remove entries *)
    1.71 +
    1.72 +fun del name (Facts {facts = (space, tab), props}) =
    1.73 +  let
    1.74 +    val space' = NameSpace.hide true name space handle ERROR _ => space;
    1.75 +    val tab' = Symtab.delete_safe name tab;
    1.76 +  in make_facts (space', tab') props end;
    1.77 +
    1.78 +fun hide fully name (Facts {facts = (space, tab), props}) =
    1.79 +  make_facts (NameSpace.hide fully name space, tab) props;
    1.80 +
    1.81  end;