# HG changeset patch
# User wenzelm
# Date 901123189 -7200
# Node ID 2dbef0104bcf2724a23c7003bb1d4f7dc64862af
# Parent  c51961c75921586394de7ef163a1a38038c0aedb
moved long_names / cond_extern to name_space.ML;

diff -r c51961c75921 -r 2dbef0104bcf src/Pure/General/name_space.ML
--- 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;
diff -r c51961c75921 -r 2dbef0104bcf src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Jul 22 11:33:32 1998 +0200
+++ b/src/Pure/pure_thy.ML	Wed Jul 22 17:59:49 1998 +0200
@@ -81,9 +81,7 @@
             Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
         | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
 
-      fun extrn name =
-        if ! long_names then name else NameSpace.extern space name;
-      val thmss = sort_wrt fst (map (apfst extrn) (Symtab.dest thms_tab));
+      val thmss = sort_wrt fst (map (apfst (NameSpace.cond_extern space)) (Symtab.dest thms_tab));
     in
       Pretty.writeln (Display.pretty_name_space ("theorem name space", space));
       Pretty.writeln (Pretty.big_list "theorems:" (map prt_thms thmss))
diff -r c51961c75921 -r 2dbef0104bcf src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Jul 22 11:33:32 1998 +0200
+++ b/src/Pure/sign.ML	Wed Jul 22 17:59:49 1998 +0200
@@ -46,7 +46,6 @@
   val norm_sort: sg -> sort -> sort
   val nonempty_sort: sg -> sort list -> sort -> bool
   val of_sort: sg -> typ * sort -> bool
-  val long_names: bool ref
   val classK: string
   val typeK: string
   val constK: string
@@ -385,10 +384,6 @@
 
 (** name spaces **)
 
-(*prune names on output by default*)
-val long_names = ref false;
-
-
 (* kinds *)
 
 val classK = "class";
@@ -404,6 +399,7 @@
 (*input and output of qualified names*)
 fun intrn spaces kind = NameSpace.intern (space_of spaces kind);
 fun extrn spaces kind = NameSpace.extern (space_of spaces kind);
+fun cond_extrn spaces kind = NameSpace.cond_extern (space_of spaces kind);
 
 (*add names*)
 fun add_names spaces kind names =
@@ -464,7 +460,7 @@
 
   val intern = intrn o spaces_of;
   val extern = extrn o spaces_of;
-  fun cond_extern sg kind = if ! long_names then I else extern sg kind;
+  val cond_extern = cond_extrn o spaces_of;
 
   val intern_class = intrn_class o spaces_of;
   val intern_sort = intrn_sort o spaces_of;
@@ -488,15 +484,15 @@
 fun pretty_term (sg as Sg ({stamps, ...}, {syn, spaces, ...})) t =
   Syntax.pretty_term syn
     (exists (equal "CPure" o !) stamps)
-    (if ! long_names then t else extrn_term spaces t);
+    (if ! NameSpace.long_names then t else extrn_term spaces t);
 
 fun pretty_typ (Sg (_, {syn, spaces, ...})) T =
   Syntax.pretty_typ syn
-    (if ! long_names then T else extrn_typ spaces T);
+    (if ! NameSpace.long_names then T else extrn_typ spaces T);
 
 fun pretty_sort (Sg (_, {syn, spaces, ...})) S =
   Syntax.pretty_sort syn
-    (if ! long_names then S else extrn_sort spaces S);
+    (if ! NameSpace.long_names then S else extrn_sort spaces S);
 
 fun pretty_classrel sg (c1, c2) = Pretty.block
   [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]];
@@ -598,8 +594,8 @@
   let
     val prt =
       setmp Syntax.show_brackets true
-        (setmp long_names true (pretty_term sg));
-    val prT = setmp long_names true (pretty_typ sg);
+        (setmp NameSpace.long_names true (pretty_term sg));
+    val prT = setmp NameSpace.long_names true (pretty_typ sg);
 
     fun err_appl why bs t T u U =
       let
@@ -679,8 +675,8 @@
     val tsig = tsig_of sg;
     val prt =
       setmp Syntax.show_brackets true
-        (setmp long_names true (pretty_term sg));
-    val prT = setmp long_names true (pretty_typ sg);
+        (setmp NameSpace.long_names true (pretty_term sg));
+    val prT = setmp NameSpace.long_names true (pretty_typ sg);
 
     val termss = foldr multiply (map fst args, [[]]);
     val typs =
@@ -1032,6 +1028,3 @@
 
 
 end;
-
-
-val long_names = Sign.long_names;