--- a/src/Pure/General/binding.ML Sat Mar 07 11:31:41 2009 +0100
+++ b/src/Pure/General/binding.ML Sat Mar 07 11:32:31 2009 +0100
@@ -11,7 +11,6 @@
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
@@ -23,7 +22,7 @@
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 =
@@ -47,20 +46,9 @@
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;
@@ -85,8 +73,8 @@
(* 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 *)
@@ -96,8 +84,8 @@
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;