renamed Symtab.null to Symtab.empty;
authorwenzelm
Sun Dec 28 14:58:56 1997 +0100 (1997-12-28)
changeset 4489749600cb5573
parent 4488 3e56603fde06
child 4490 14cd07c16e02
renamed Symtab.null to Symtab.empty;
renamed Symtan.extend_new to Symtab.extend;
renamed Symtan.DUPLICATE to Symtab.DUP;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sun Dec 28 14:58:06 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Dec 28 14:58:56 1997 +0100
     1.3 @@ -263,7 +263,7 @@
     1.4  
     1.5  (* prepare data *)
     1.6  
     1.7 -val empty_data = Data Symtab.null;
     1.8 +val empty_data = Data Symtab.empty;
     1.9  
    1.10  fun merge_data (Data tab1, Data tab2) =
    1.11    let
    1.12 @@ -290,7 +290,7 @@
    1.13  
    1.14  fun init_data_sg sg (Data tab) kind e ext mrg prt =
    1.15    Data (Symtab.update_new ((kind, (e, (ext, mrg, prt))), tab))
    1.16 -    handle Symtab.DUPLICATE _ => err_dup_init sg kind;
    1.17 +    handle Symtab.DUP _ => err_dup_init sg kind;
    1.18  
    1.19  
    1.20  (* access data *)
    1.21 @@ -373,13 +373,14 @@
    1.22  
    1.23  (*add names*)
    1.24  fun add_names spaces kind names =
    1.25 -  let val space' = NameSpace.extend (names, space_of spaces kind) in
    1.26 +  let val space' = NameSpace.extend (space_of spaces kind, names) in
    1.27      overwrite (spaces, (kind, space'))
    1.28    end;
    1.29  
    1.30  (*make full names*)
    1.31  fun full path name =
    1.32 -  if NameSpace.qualified name then
    1.33 +  if name = "" then error "Attempt to declare empty name \"\""
    1.34 +  else if NameSpace.qualified name then
    1.35      error ("Attempt to declare qualified name " ^ quote name)
    1.36    else NameSpace.pack (path @ [name]);
    1.37  
    1.38 @@ -739,7 +740,7 @@
    1.39        else decls_of path Syntax.const_name consts;
    1.40    in
    1.41      (Syntax.extend_const_gram syn prmode consts, tsig,
    1.42 -      Symtab.extend_new (ctab, decls)
    1.43 +      Symtab.extend (ctab, decls)
    1.44          handle Symtab.DUPS cs => err_dup_consts cs,
    1.45        (path, add_names spaces constK (map fst decls)), data)
    1.46    end;
    1.47 @@ -935,11 +936,11 @@
    1.48  (** partial Pure signature **)
    1.49  
    1.50  val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
    1.51 -  Symtab.null, Syntax.pure_syn, [], [], empty_data, []);
    1.52 +  Symtab.empty, Syntax.pure_syn, [], [], empty_data, []);
    1.53  
    1.54  val pre_pure =
    1.55    create_sign (SgRef (Some (ref dummy_sg))) [] "#"
    1.56 -    (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), empty_data);
    1.57 +    (Syntax.pure_syn, Type.tsig0, Symtab.empty, ([], []), empty_data);
    1.58  
    1.59  
    1.60  end;