# HG changeset patch
# User wenzelm
# Date 1236113374 -3600
# Node ID 8f551a13ee99d23bc4aa59138c3a66249c2b4c47
# Parent  b3f3ad327d4d56d3521dc42fa1104f643507cc42
tuned str_of, now subject to verbose flag;

diff -r b3f3ad327d4d -r 8f551a13ee99 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Mar 03 21:49:05 2009 +0100
+++ b/src/Pure/General/binding.ML	Tue Mar 03 21:49:34 2009 +0100
@@ -11,6 +11,7 @@
 sig
   type binding
   val dest: binding -> (string * bool) list * (string * bool) list * bstring
+  val verbose: bool ref
   val str_of: binding -> string
   val make: bstring * Position.T -> binding
   val name: bstring -> binding
@@ -50,13 +51,17 @@
 
 (* 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 null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
-      str_of_components qualifier ^ ":" ^ name;
+      if ! verbose then
+        (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
+          str_of_components qualifier ^ name
+      else name;
     val props = Position.properties_of pos;
   in Markup.markup (Markup.properties props (Markup.binding name)) text end;