1signature KernelSig =
2sig
3
4  type kernelname = {Thy : string, Name : string}
5  val name_compare : kernelname * kernelname -> order
6  val name_toString : kernelname -> string
7  val name_toMLString : kernelname -> string
8
9  eqtype kernelid
10
11  val id_compare : kernelid * kernelid -> order
12  val name_of_id : kernelid -> kernelname
13  val id_toString : kernelid -> string
14  val new_id : kernelname -> kernelid
15  val uptodate_id : kernelid -> bool
16  val retire_id : kernelid -> unit
17  val name_of : kernelid -> string
18  val seg_of : kernelid -> string
19
20  type 'a symboltable
21  exception NotFound
22  val new_table : unit -> 'a symboltable
23  val insert : 'a symboltable * kernelname * 'a -> kernelid
24  val find : 'a symboltable * kernelname -> kernelid * 'a
25  val peek : 'a symboltable * kernelname -> (kernelid * 'a) option
26
27  val numItems : 'a symboltable -> int
28  val listItems : 'a symboltable -> (kernelname * (kernelid * 'a)) list
29  val listThy : 'a symboltable -> string -> (kernelname * (kernelid * 'a)) list
30  val listName : 'a symboltable -> string -> (kernelname * (kernelid * 'a)) list
31
32  val app : (kernelname * (kernelid * 'a) -> unit) -> 'a symboltable -> unit
33  val foldl : (kernelname * (kernelid * 'a) * 'b -> 'b) -> 'b ->
34              'a symboltable -> 'b
35  val retire_name : 'a symboltable * kernelname -> unit
36  val uptodate_name : 'a symboltable * kernelname -> bool
37  val del_segment : 'a symboltable * string -> unit
38
39end
40