support for absolute namespace entry paths;
authorwenzelm
Wed Aug 15 22:20:30 2001 +0200 (2001-08-15)
changeset 115013b6415035d1a
parent 11500 a84130c7e6ab
child 11502 e80a712982e1
support for absolute namespace entry paths;
src/Pure/display.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/display.ML	Fri Aug 10 10:25:45 2001 +0200
     1.2 +++ b/src/Pure/display.ML	Wed Aug 15 22:20:30 2001 +0200
     1.3 @@ -211,7 +211,7 @@
     1.4    in
     1.5      [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
     1.6        Pretty.strs ("data:" :: Sign.data_kinds data),
     1.7 -      Pretty.strs ["name prefix:", NameSpace.pack path],
     1.8 +      Pretty.strs ["name prefix:", NameSpace.pack (if_none path ["-"])],
     1.9        Pretty.big_list "name spaces:" (map pretty_name_space spaces'),
    1.10        pretty_classes classes,
    1.11        Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)),
     2.1 --- a/src/Pure/sign.ML	Fri Aug 10 10:25:45 2001 +0200
     2.2 +++ b/src/Pure/sign.ML	Wed Aug 15 22:20:30 2001 +0200
     2.3 @@ -25,7 +25,7 @@
     2.4      tsig: Type.type_sig,
     2.5      const_tab: typ Symtab.table,
     2.6      syn: Syntax.syntax,
     2.7 -    path: string list,
     2.8 +    path: string list option,
     2.9      spaces: (string * NameSpace.T) list,
    2.10      data: data}
    2.11    val name_of: sg -> string
    2.12 @@ -178,7 +178,7 @@
    2.13      tsig: Type.type_sig,                        (*order-sorted signature of types*)
    2.14      const_tab: typ Symtab.table,                (*type schemes of constants*)
    2.15      syn: Syntax.syntax,                         (*syntax for parsing and printing*)
    2.16 -    path: string list,                          (*current name space entry prefix*)
    2.17 +    path: string list option,                   (*current name space entry prefix*)
    2.18      spaces: (string * NameSpace.T) list,        (*name spaces for consts, types etc.*)
    2.19      data: data}                                 (*anytype data*)
    2.20  and data =
    2.21 @@ -441,11 +441,12 @@
    2.22  fun hide_names x = change_space NameSpace.hide x;
    2.23  
    2.24  (*make full names*)
    2.25 -fun full path name =
    2.26 -  if name = "" then error "Attempt to declare empty name \"\""
    2.27 -  else if NameSpace.is_qualified name then
    2.28 -    error ("Attempt to declare qualified name " ^ quote name)
    2.29 -  else NameSpace.pack (path @ [name]);
    2.30 +fun full _ "" = error "Attempt to declare empty name \"\""
    2.31 +  | full None name = name
    2.32 +  | full (Some path) name =
    2.33 +      if NameSpace.is_qualified name then
    2.34 +        error ("Attempt to declare qualified name " ^ quote name)
    2.35 +      else NameSpace.pack (path @ [name]);
    2.36  
    2.37  (*base name*)
    2.38  val base_name = NameSpace.base;
    2.39 @@ -507,8 +508,10 @@
    2.40    val intern_tycons = intrn_tycons o spaces_of;
    2.41  
    2.42    val full_name = full o #path o rep_sg;
    2.43 -  fun full_name_path sg elems name =
    2.44 -    full (#path (rep_sg sg) @ NameSpace.unpack elems) name;
    2.45 +
    2.46 +  fun full_name_path sg elems =
    2.47 +    full (Some (if_none (#path (rep_sg sg)) [] @ NameSpace.unpack elems));
    2.48 +
    2.49  end;
    2.50  
    2.51  
    2.52 @@ -970,9 +973,11 @@
    2.53  fun ext_path (syn, tsig, ctab, (path, spaces), data) elems =
    2.54    let
    2.55      val path' =
    2.56 -      if elems = ".." andalso not (null path) then fst (split_last path)
    2.57 -      else if elems = "/" then []
    2.58 -      else path @ NameSpace.unpack elems;
    2.59 +      if elems = "//" then None
    2.60 +      else if elems = "/" then Some []
    2.61 +      else if elems = ".." andalso is_some path andalso path <> Some [] then
    2.62 +        Some (fst (split_last (the path)))
    2.63 +      else Some (if_none path [] @ NameSpace.unpack elems);
    2.64    in
    2.65      (syn, tsig, ctab, (path', spaces), data)
    2.66    end;
    2.67 @@ -1107,7 +1112,7 @@
    2.68            raise TERM ("Incompatible types for constant(s) " ^ commas_quote cs, []);
    2.69        val syn = Syntax.merge_syntaxes syn1 syn2;
    2.70  
    2.71 -      val path = [];
    2.72 +      val path = Some [];
    2.73        val kinds = distinct (map fst (spaces1 @ spaces2));
    2.74        val spaces =
    2.75          kinds ~~
    2.76 @@ -1126,11 +1131,11 @@
    2.77  (** partial Pure signature **)
    2.78  
    2.79  val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
    2.80 -  Symtab.empty, Syntax.pure_syn, [], [], empty_data, []);
    2.81 +  Symtab.empty, Syntax.pure_syn, Some [], [], empty_data, []);
    2.82  
    2.83  val pre_pure =
    2.84    create_sign (SgRef (Some (ref dummy_sg))) [] "#"
    2.85 -    (Syntax.pure_syn, Type.tsig0, Symtab.empty, ([], []), empty_data);
    2.86 +    (Syntax.pure_syn, Type.tsig0, Symtab.empty, (Some [], []), empty_data);
    2.87  
    2.88  
    2.89  end;
     3.1 --- a/src/Pure/theory.ML	Fri Aug 10 10:25:45 2001 +0200
     3.2 +++ b/src/Pure/theory.ML	Wed Aug 15 22:20:30 2001 +0200
     3.3 @@ -78,6 +78,7 @@
     3.4    val add_path: string -> theory -> theory
     3.5    val parent_path: theory -> theory
     3.6    val root_path: theory -> theory
     3.7 +  val absolute_path: theory -> theory
     3.8    val hide_space: string * xstring list -> theory -> theory
     3.9    val hide_space_i: string * string list -> theory -> theory
    3.10    val hide_classes: string list -> theory -> theory
    3.11 @@ -217,6 +218,7 @@
    3.12  val add_path         = ext_sign Sign.add_path;
    3.13  val parent_path      = add_path "..";
    3.14  val root_path        = add_path "/";
    3.15 +val absolute_path    = add_path "//";
    3.16  val add_space        = ext_sign Sign.add_space;
    3.17  val hide_space       = ext_sign Sign.hide_space;
    3.18  val hide_space_i     = ext_sign Sign.hide_space_i;