# HG changeset patch
# User wenzelm
# Date 955973299 -7200
# Node ID 0e48ee5b52db358d4d80e309f6fbed3a4e33e101
# Parent  ef7efded8fdcedf3e31bd744d6419a9e5808fe1b
name space hide operations;

diff -r ef7efded8fdc -r 0e48ee5b52db src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Apr 17 14:07:00 2000 +0200
+++ b/src/Pure/sign.ML	Mon Apr 17 14:08:19 2000 +0200
@@ -125,6 +125,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 add_name: string -> sg -> sg
   val data_kinds: data -> string list
   val merge_refs: sg_ref * sg_ref -> sg_ref
@@ -407,7 +409,7 @@
 val constK = "const";
 
 
-(* add and retrieve names *)
+(* declare and retrieve names *)
 
 fun space_of spaces kind =
   if_none (assoc (spaces, kind)) NameSpace.empty;
@@ -418,16 +420,15 @@
 fun cond_extrn spaces kind = NameSpace.cond_extern (space_of spaces kind);
 fun cond_extrn_table spaces kind tab = NameSpace.cond_extern_table (space_of spaces kind) tab;
 
-(*add names*)
-fun add_names spaces kind names =
-  let val space' = NameSpace.extend (space_of spaces kind, names) in
-    overwrite (spaces, (kind, space'))
-  end;
+(*add / hide names*)
+fun change_space f spaces kind x = overwrite (spaces, (kind, f (space_of spaces kind, x)));
+val add_names = change_space NameSpace.extend;
+val hide_names = change_space NameSpace.hide;
 
 (*make full names*)
 fun full path name =
   if name = "" then error "Attempt to declare empty name \"\""
-  else if NameSpace.qualified name then
+  else if NameSpace.is_qualified name then
     error ("Attempt to declare qualified name " ^ quote name)
   else NameSpace.pack (path @ [name]);
 
@@ -616,10 +617,8 @@
 (*compute and check type of the term*)
 fun type_check sg tm =
   let
-    val prt =
-      setmp Syntax.show_brackets true
-        (setmp NameSpace.long_names true (pretty_term sg));
-    val prT = setmp NameSpace.long_names true (pretty_typ sg);
+    val prt = setmp Syntax.show_brackets true (pretty_term sg);
+    val prT = pretty_typ sg;
 
     fun err_appl why bs t T u U =
       let
@@ -690,10 +689,8 @@
 fun infer_types_simult sg def_type def_sort used freeze args =
   let
     val tsig = tsig_of sg;
-    val prt =
-      setmp Syntax.show_brackets true
-        (setmp NameSpace.long_names true (pretty_term sg));
-    val prT = setmp NameSpace.long_names true (pretty_typ sg);
+    val prt = setmp Syntax.show_brackets true (pretty_term sg);
+    val prT = pretty_typ sg;
 
     val termss = foldr multiply (map fst args, [[]]);
     val typs =
@@ -923,10 +920,16 @@
   end;      
 
 
-(* add to name space *)
+(* change name space *)
+
+fun ext_add_space (syn, tsig, ctab, (path, spaces), data) (kind, names) =
+  (syn, tsig, ctab, (path, add_names spaces kind names), data);
 
-fun ext_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_i (syn, tsig, ctab, (path, spaces), data) (kind, names) =
+  (syn, tsig, ctab, (path, hide_names spaces kind names), data);
 
 
 (* signature data *)
@@ -976,7 +979,9 @@
 val add_trrules       = extend_sign true ext_trrules "#";
 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_space "#";
+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 "#";
 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 ef7efded8fdc -r 0e48ee5b52db src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Apr 17 14:07:00 2000 +0200
+++ b/src/Pure/theory.ML	Mon Apr 17 14:08:19 2000 +0200
@@ -77,7 +77,11 @@
   val add_path: string -> theory -> theory
   val parent_path: theory -> theory
   val root_path: theory -> theory
-  val add_space: string * string list -> 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 add_name: string -> theory -> theory
   val copy: theory -> theory
   val prep_ext: theory -> theory
@@ -147,7 +151,7 @@
 
 (** extend theory **)
 
-(*name space kinds*)
+(*name spaces*)
 val axiomK = "axiom";
 val oracleK = "oracle";
 
@@ -209,6 +213,11 @@
 val parent_path      = add_path "..";
 val root_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 add_name         = ext_sign Sign.add_name;
 val copy             = ext_sign (K Sign.copy) ();
 val prep_ext         = ext_sign (K Sign.prep_ext) ();