# HG changeset patch
# User berghofe
# Date 1076517368 -3600
# Node ID 9fb68cd747193524879e8064986b6f424e884930
# Parent  1189a8212a121e572f4f11702b0a603d06853c8c
Added flag short_names

diff -r 1189a8212a12 -r 9fb68cd74719 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Feb 11 01:26:15 2004 +0100
+++ b/src/Pure/General/name_space.ML	Wed Feb 11 17:36:08 2004 +0100
@@ -30,6 +30,7 @@
   val intern: T -> string -> string
   val extern: T -> string -> string
   val long_names: bool ref
+  val short_names: bool ref
   val cond_extern: T -> string -> string
   val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
   val dest: T -> (string * string list) list
@@ -151,7 +152,12 @@
 (*prune names on output by default*)
 val long_names = ref false;
 
-fun cond_extern space = if ! long_names then I else extern space;
+(*output only base name*)
+val short_names = ref false;
+
+fun cond_extern space =
+  if ! long_names then I
+  else if ! short_names then base else extern space;
 
 fun cond_extern_table space tab =
   Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));