src/Pure/facts.ML
changeset 33163 351fc13613f2
parent 33096 db3c18fd9708
child 35408 b48ab741683b
equal deleted inserted replaced
33162:d11b89e7afd9 33163:351fc13613f2
    19   val select: ref -> thm list -> thm list
    19   val select: ref -> thm list -> thm list
    20   val selections: string * thm list -> (ref * thm) list
    20   val selections: string * thm list -> (ref * thm) list
    21   type T
    21   type T
    22   val empty: T
    22   val empty: T
    23   val space_of: T -> Name_Space.T
    23   val space_of: T -> Name_Space.T
       
    24   val is_concealed: T -> string -> bool
    24   val intern: T -> xstring -> string
    25   val intern: T -> xstring -> string
    25   val extern: T -> string -> xstring
    26   val extern: T -> string -> xstring
    26   val lookup: Context.generic -> T -> string -> (bool * thm list) option
    27   val lookup: Context.generic -> T -> string -> (bool * thm list) option
    27   val defined: T -> string -> bool
    28   val defined: T -> string -> bool
    28   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    29   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
    42 struct
    43 struct
    43 
    44 
    44 (** fact references **)
    45 (** fact references **)
    45 
    46 
    46 fun the_single _ [th] : thm = th
    47 fun the_single _ [th] : thm = th
    47   | the_single name _ = error ("Single theorem expected " ^ quote name);
    48   | the_single name _ = error ("Expected singleton fact " ^ quote name);
    48 
    49 
    49 
    50 
    50 (* datatype interval *)
    51 (* datatype interval *)
    51 
    52 
    52 datatype interval =
    53 datatype interval =
   124 datatype T = Facts of
   125 datatype T = Facts of
   125  {facts: fact Name_Space.table,
   126  {facts: fact Name_Space.table,
   126   props: thm Net.net};
   127   props: thm Net.net};
   127 
   128 
   128 fun make_facts facts props = Facts {facts = facts, props = props};
   129 fun make_facts facts props = Facts {facts = facts, props = props};
       
   130 
   129 val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
   131 val empty = make_facts (Name_Space.empty_table "fact") Net.empty;
   130 
   132 
   131 
   133 
   132 (* named facts *)
   134 (* named facts *)
   133 
   135 
   134 fun facts_of (Facts {facts, ...}) = facts;
   136 fun facts_of (Facts {facts, ...}) = facts;
   135 
   137 
   136 val space_of = #1 o facts_of;
   138 val space_of = #1 o facts_of;
   137 val table_of = #2 o facts_of;
   139 val table_of = #2 o facts_of;
       
   140 
       
   141 val is_concealed = Name_Space.is_concealed o space_of;
   138 
   142 
   139 val intern = Name_Space.intern o space_of;
   143 val intern = Name_Space.intern o space_of;
   140 val extern = Name_Space.extern o space_of;
   144 val extern = Name_Space.extern o space_of;
   141 
   145 
   142 val defined = Symtab.defined o table_of;
   146 val defined = Symtab.defined o table_of;
   214 
   218 
   215 (* remove entries *)
   219 (* remove entries *)
   216 
   220 
   217 fun del name (Facts {facts = (space, tab), props}) =
   221 fun del name (Facts {facts = (space, tab), props}) =
   218   let
   222   let
   219     val space' = Name_Space.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
   223     val space' = Name_Space.hide true name space handle ERROR _ => space;
   220     val tab' = Symtab.delete_safe name tab;
   224     val tab' = Symtab.delete_safe name tab;
   221   in make_facts (space', tab') props end;
   225   in make_facts (space', tab') props end;
   222 
   226 
   223 fun hide fully name (Facts {facts = (space, tab), props}) =
   227 fun hide fully name (Facts {facts = (space, tab), props}) =
   224   make_facts (Name_Space.hide fully name space, tab) props;
   228   make_facts (Name_Space.hide fully name space, tab) props;