src/Pure/General/binding.ML

 
 signature BINDING =
 sig
   type binding
   val dest: binding -> (string * bool) list * bstring
-  val verbose: bool ref
   val str_of: binding -> string
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
   val name: bstring -> binding
   val name_of: binding -> string

   val empty: binding
   val is_empty: binding -> bool
   val qualify: bool -> string -> binding -> binding
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
-  val add_prefix: bool -> string -> binding -> binding
+  val prefix: bool -> string -> binding -> binding
 end;
 
 structure Binding: BINDING =
 struct
 

 fun map_binding f (Binding {prefix, qualifier, name, pos}) =
   make_binding (f (prefix, qualifier, name, pos));
 
 fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
 
-
-(* diagnostic output *)
-
-val verbose = ref false;
-
-val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?");
-
 fun str_of (Binding {prefix, qualifier, name, pos}) =
   let
-    val text =
-      if ! verbose then
-        (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
-          str_of_components qualifier ^ name
-      else name;
+    val text = space_implode "." (map #1 qualifier @ [name]);
     val props = Position.properties_of pos;
   in Markup.markup (Markup.properties props (Markup.binding name)) text end;
 
 
 

 
 
 (* user qualifier *)
 
 fun qualify _ "" = I
-  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
-      (prefix, (qual, mandatory) :: qualifier, name, pos));
+  | qualify strict qual = map_binding (fn (prefix, qualifier, name, pos) =>
+      (prefix, (qual, strict) :: qualifier, name, pos));
 
 
 (* system prefix *)
 
 fun prefix_of (Binding {prefix, ...}) = prefix;
 
 fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
   (f prefix, qualifier, name, pos));
 
-fun add_prefix _ "" = I
-  | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
+fun prefix _ "" = I
+  | prefix strict prfx = map_prefix (cons (prfx, strict));
 
 end;
 
 type binding = Binding.binding;