# HG changeset patch
# User wenzelm
# Date 1008973032 -3600
# Node ID 0361fd72f1a7a7d02c6d3d5ecefbabe889bd62b5
# Parent  3f3d2ffb5df5cfb2e31ef49525219cf72f84a291
hide: flag for full/base name;

diff -r 3f3d2ffb5df5 -r 0361fd72f1a7 src/Pure/General/name_space.ML
--- 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 *)
diff -r 3f3d2ffb5df5 -r 0361fd72f1a7 src/Pure/sign.ML
--- 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;
diff -r 3f3d2ffb5df5 -r 0361fd72f1a7 src/Pure/theory.ML
--- 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) ();