Added flag short_names
authorberghofe
Wed Feb 11 17:36:08 2004 +0100 (2004-02-11)
changeset 143829fb68cd74719
parent 14381 1189a8212a12
child 14383 09aab4710789
Added flag short_names
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Feb 11 01:26:15 2004 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Feb 11 17:36:08 2004 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4    val intern: T -> string -> string
     1.5    val extern: T -> string -> string
     1.6    val long_names: bool ref
     1.7 +  val short_names: bool ref
     1.8    val cond_extern: T -> string -> string
     1.9    val cond_extern_table: T -> 'a Symtab.table -> (string * 'a) list
    1.10    val dest: T -> (string * string list) list
    1.11 @@ -151,7 +152,12 @@
    1.12  (*prune names on output by default*)
    1.13  val long_names = ref false;
    1.14  
    1.15 -fun cond_extern space = if ! long_names then I else extern space;
    1.16 +(*output only base name*)
    1.17 +val short_names = ref false;
    1.18 +
    1.19 +fun cond_extern space =
    1.20 +  if ! long_names then I
    1.21 +  else if ! short_names then base else extern space;
    1.22  
    1.23  fun cond_extern_table space tab =
    1.24    Library.sort_wrt #1 (map (apfst (cond_extern space)) (Symtab.dest tab));