# HG changeset patch
# User wenzelm
# Date 1236088333 -3600
# Node ID f84c9f10292a9ba14529b3e9b8034f34807ecde0
# Parent  3951aab916fdc96283fc01606dea09cbe289c8d4
moved name space externalization flags back to name_space.ML;
display: always show prefix for now;
tuned signature;

diff -r 3951aab916fd -r f84c9f10292a src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Mar 03 14:16:05 2009 +0100
+++ b/src/Pure/General/binding.ML	Tue Mar 03 14:52:13 2009 +0100
@@ -1,20 +1,13 @@
 (*  Title:      Pure/General/binding.ML
     Author:     Florian Haftmann, TU Muenchen
+    Author:     Makarius
 
 Structured name bindings.
 *)
 
-signature BASIC_BINDING =
+signature BINDING =
 sig
   type binding
-  val long_names: bool ref
-  val short_names: bool ref
-  val unique_names: bool ref
-end;
-
-signature BINDING =
-sig
-  include BASIC_BINDING
   val name_pos: string * Position.T -> binding
   val name: string -> binding
   val empty: binding
@@ -34,13 +27,6 @@
 structure Binding : BINDING =
 struct
 
-(** global flags **)
-
-val long_names = ref false;
-val short_names = ref false;
-val unique_names = ref true;
-
-
 (** qualification **)
 
 val separator = ".";
@@ -88,11 +74,9 @@
   let
     fun mk_prefix (prfx, true) = prfx
       | mk_prefix (prfx, false) = enclose "(" ")" prfx
-  in if not (! long_names) orelse null prefix orelse name = "" then name
-    else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
-  end;
+  in space_implode "." (map mk_prefix prefix) ^ ":" ^ name end;
 
 end;
 
-structure Basic_Binding : BASIC_BINDING = Binding;
-open Basic_Binding;
+type binding = Binding.binding;
+