--- a/src/Pure/General/name_space.ML Fri Dec 21 23:16:17 2001 +0100
+++ b/src/Pure/General/name_space.ML Fri Dec 21 23:17:12 2001 +0100
@@ -12,7 +12,7 @@
signature NAME_SPACE =
sig
- val separator: string (*single char!*)
+ val separator: string (*single char*)
val hidden: string -> string
val append: string -> string -> string
val unpack: string -> string list
@@ -25,7 +25,7 @@
val empty: T
val extend: T * string list -> T
val merge: T * T -> T
- val hide: T * string list -> T
+ val hide: bool -> T * string list -> T
val intern: T -> string -> string
val extern: T -> string -> string
val long_names: bool ref
@@ -112,15 +112,16 @@
(* hide *)
-fun hide_aux (name, tab) =
+fun hide_aux fully (name, tab) =
if not (is_qualified name) then
error ("Attempt to hide global name " ^ quote name)
else if is_hidden name then
error ("Attempt to hide hidden name " ^ quote name)
else (change' add name (name,
- foldl (fn (tb, xname) => change del xname (name, tb)) (tab, accesses name)));
+ foldl (fn (tb, xname) => change del xname (name, tb))
+ (tab, if fully then accesses name else [base name])));
-fun hide (NameSpace tab, names) = NameSpace (foldr hide_aux (names, tab));
+fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) (names, tab));
(* intern / extern names *)
--- a/src/Pure/sign.ML Fri Dec 21 23:16:17 2001 +0100
+++ b/src/Pure/sign.ML Fri Dec 21 23:17:12 2001 +0100
@@ -142,8 +142,8 @@
val add_trrules_i: ast Syntax.trrule list -> sg -> sg
val add_path: string -> sg -> sg
val add_space: string * string list -> sg -> sg
- val hide_space: string * string list -> sg -> sg
- val hide_space_i: string * string list -> sg -> sg
+ val hide_space: bool -> string * string list -> sg -> sg
+ val hide_space_i: bool -> string * string list -> sg -> sg
val add_name: string -> sg -> sg
val data_kinds: data -> string list
val merge_refs: sg_ref * sg_ref -> sg_ref
@@ -445,7 +445,7 @@
(*add / hide names*)
fun change_space f spaces kind x = overwrite (spaces, (kind, f (space_of spaces kind, x)));
fun add_names x = change_space NameSpace.extend x;
-fun hide_names x = change_space NameSpace.hide x;
+fun hide_names b x = change_space (NameSpace.hide b) x;
(*make full names*)
fun full _ "" = error "Attempt to declare empty name \"\""
@@ -1006,11 +1006,11 @@
fun ext_add_space (syn, tsig, ctab, (path, spaces), data) (kind, names) =
(syn, tsig, ctab, (path, add_names spaces kind names), data);
-fun ext_hide_space (syn, tsig, ctab, (path, spaces), data) (kind, xnames) =
- (syn, tsig, ctab, (path, hide_names spaces kind (map (intrn spaces kind) xnames)), data);
+fun ext_hide_space (syn, tsig, ctab, (path, spaces), data) (b, (kind, xnames)) =
+ (syn, tsig, ctab, (path, hide_names b spaces kind (map (intrn spaces kind) xnames)), data);
-fun ext_hide_space_i (syn, tsig, ctab, (path, spaces), data) (kind, names) =
- (syn, tsig, ctab, (path, hide_names spaces kind names), data);
+fun ext_hide_space_i (syn, tsig, ctab, (path, spaces), data) (b, (kind, names)) =
+ (syn, tsig, ctab, (path, hide_names b spaces kind names), data);
(* signature data *)
@@ -1061,8 +1061,8 @@
val add_trrules_i = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
val add_path = extend_sign true ext_path "#";
val add_space = extend_sign true ext_add_space "#";
-val hide_space = extend_sign true ext_hide_space "#";
-val hide_space_i = extend_sign true ext_hide_space_i "#";
+val hide_space = curry (extend_sign true ext_hide_space "#");
+val hide_space_i = curry (extend_sign true ext_hide_space_i "#");
fun init_data arg sg = extend_sign true (ext_init_data sg) "#" arg sg;
fun put_data k f x sg = extend_sign true (ext_put_data sg) "#" (k, f, x) sg;
fun add_name name sg = extend_sign true K name () sg;
--- a/src/Pure/theory.ML Fri Dec 21 23:16:17 2001 +0100
+++ b/src/Pure/theory.ML Fri Dec 21 23:17:12 2001 +0100
@@ -79,11 +79,11 @@
val parent_path: theory -> theory
val root_path: theory -> theory
val absolute_path: theory -> theory
- val hide_space: string * xstring list -> theory -> theory
- val hide_space_i: string * string list -> theory -> theory
- val hide_classes: string list -> theory -> theory
- val hide_types: string list -> theory -> theory
- val hide_consts: string list -> theory -> theory
+ val hide_space: bool -> string * xstring list -> theory -> theory
+ val hide_space_i: bool -> string * string list -> theory -> theory
+ val hide_classes: bool -> string list -> theory -> theory
+ val hide_types: bool -> string list -> theory -> theory
+ val hide_consts: bool -> string list -> theory -> theory
val add_name: string -> theory -> theory
val copy: theory -> theory
val prep_ext: theory -> theory
@@ -220,11 +220,11 @@
val root_path = add_path "/";
val absolute_path = add_path "//";
val add_space = ext_sign Sign.add_space;
-val hide_space = ext_sign Sign.hide_space;
-val hide_space_i = ext_sign Sign.hide_space_i;
-val hide_classes = curry hide_space_i Sign.classK;
-val hide_types = curry hide_space_i Sign.typeK;
-val hide_consts = curry hide_space_i Sign.constK;
+val hide_space = ext_sign o Sign.hide_space;
+val hide_space_i = ext_sign o Sign.hide_space_i;
+fun hide_classes b = curry (hide_space_i b) Sign.classK;
+fun hide_types b = curry (hide_space_i b) Sign.typeK;
+fun hide_consts b = curry (hide_space_i b) Sign.constK;
val add_name = ext_sign Sign.add_name;
val copy = ext_sign (K Sign.copy) ();
val prep_ext = ext_sign (K Sign.prep_ext) ();