src/Pure/General/name_space.ML
changeset 5175 2dbef0104bcf
parent 5012 086b055c4d73
child 5682 9125611c1645
--- a/src/Pure/General/name_space.ML	Wed Jul 22 11:33:32 1998 +0200
+++ b/src/Pure/General/name_space.ML	Wed Jul 22 17:59:49 1998 +0200
@@ -24,6 +24,8 @@
   val merge: T * T -> T
   val intern: T -> string -> string
   val extern: T -> string -> string
+  val long_names: bool ref
+  val cond_extern: T -> string -> string
   val dest: T -> (string * string list) list
 end;
 
@@ -96,6 +98,11 @@
           else try nms;
   in try (map pack (suffixes1 (unpack name))) end;
 
+(*prune names on output by default*)
+val long_names = ref false;
+
+fun cond_extern space = if ! long_names then I else extern space;
+
 
 (* dest *)
 
@@ -105,3 +112,6 @@
 
 
 end;
+
+
+val long_names = NameSpace.long_names;