# HG changeset patch # User wenzelm # Date 883317536 -3600 # Node ID 749600cb5573a50ac6ff00fda8e751f411076f19 # Parent 3e56603fde068243d7c34cd16386cccec2805227 renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend; renamed Symtan.DUPLICATE to Symtab.DUP; diff -r 3e56603fde06 -r 749600cb5573 src/Pure/sign.ML --- a/src/Pure/sign.ML Sun Dec 28 14:58:06 1997 +0100 +++ b/src/Pure/sign.ML Sun Dec 28 14:58:56 1997 +0100 @@ -263,7 +263,7 @@ (* prepare data *) -val empty_data = Data Symtab.null; +val empty_data = Data Symtab.empty; fun merge_data (Data tab1, Data tab2) = let @@ -290,7 +290,7 @@ fun init_data_sg sg (Data tab) kind e ext mrg prt = Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab)) - handle Symtab.DUPLICATE _ => err_dup_init sg kind; + handle Symtab.DUP _ => err_dup_init sg kind; (* access data *) @@ -373,13 +373,14 @@ (*add names*) fun add_names spaces kind names = - let val space' = NameSpace.extend (names, space_of spaces kind) in + let val space' = NameSpace.extend (space_of spaces kind, names) in overwrite (spaces, (kind, space')) end; (*make full names*) fun full path name = - if NameSpace.qualified name then + if name = "" then error "Attempt to declare empty name \"\"" + else if NameSpace.qualified name then error ("Attempt to declare qualified name " ^ quote name) else NameSpace.pack (path @ [name]); @@ -739,7 +740,7 @@ else decls_of path Syntax.const_name consts; in (Syntax.extend_const_gram syn prmode consts, tsig, - Symtab.extend_new (ctab, decls) + Symtab.extend (ctab, decls) handle Symtab.DUPS cs => err_dup_consts cs, (path, add_names spaces constK (map fst decls)), data) end; @@ -935,11 +936,11 @@ (** partial Pure signature **) val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0, - Symtab.null, Syntax.pure_syn, [], [], empty_data, []); + Symtab.empty, Syntax.pure_syn, [], [], empty_data, []); val pre_pure = create_sign (SgRef (Some (ref dummy_sg))) [] "#" - (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), empty_data); + (Syntax.pure_syn, Type.tsig0, Symtab.empty, ([], []), empty_data); end;