# HG changeset patch
# User wenzelm
# Date 1309015069 -7200
# Node ID f3a8476285c6394278f041a299843b5f56641e37
# Parent  6629e2dedb009ce554e927a03fcfcf6e97ce89e9
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;

diff -r 6629e2dedb00 -r f3a8476285c6 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Jun 25 15:08:58 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Jun 25 17:17:49 2011 +0200
@@ -1094,7 +1094,7 @@
   @{index_ML Binding.qualify: "bool -> string -> binding -> binding"} \\
   @{index_ML Binding.prefix: "bool -> string -> binding -> binding"} \\
   @{index_ML Binding.conceal: "binding -> binding"} \\
-  @{index_ML Binding.str_of: "binding -> string"} \\
+  @{index_ML Binding.print: "binding -> string"} \\
   \end{mldecls}
   \begin{mldecls}
   @{index_ML_type Name_Space.naming} \\
@@ -1144,7 +1144,7 @@
   particulars of concealed entities (cf.\ @{ML
   Name_Space.is_concealed}).
 
-  \item @{ML Binding.str_of}~@{text "binding"} produces a string
+  \item @{ML Binding.print}~@{text "binding"} produces a string
   representation for human-readable output, together with some formal
   markup that might get used in GUI front-ends, for example.
 
diff -r 6629e2dedb00 -r f3a8476285c6 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Jun 25 15:08:58 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Jun 25 17:17:49 2011 +0200
@@ -1604,7 +1604,7 @@
   \indexdef{}{ML}{Binding.qualify}\verb|Binding.qualify: bool -> string -> binding -> binding| \\
   \indexdef{}{ML}{Binding.prefix}\verb|Binding.prefix: bool -> string -> binding -> binding| \\
   \indexdef{}{ML}{Binding.conceal}\verb|Binding.conceal: binding -> binding| \\
-  \indexdef{}{ML}{Binding.str\_of}\verb|Binding.str_of: binding -> string| \\
+  \indexdef{}{ML}{Binding.print}\verb|Binding.print: binding -> string| \\
   \end{mldecls}
   \begin{mldecls}
   \indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\
@@ -1651,7 +1651,7 @@
   specification mechanism etc.  Other tools should not depend on the
   particulars of concealed entities (cf.\ \verb|Name_Space.is_concealed|).
 
-  \item \verb|Binding.str_of|~\isa{binding} produces a string
+  \item \verb|Binding.print|~\isa{binding} produces a string
   representation for human-readable output, together with some formal
   markup that might get used in GUI front-ends, for example.
 
diff -r 6629e2dedb00 -r f3a8476285c6 etc/isabelle.css
--- a/etc/isabelle.css	Sat Jun 25 15:08:58 2011 +0200
+++ b/etc/isabelle.css	Sat Jun 25 17:17:49 2011 +0200
@@ -19,6 +19,7 @@
 
 .hidden, hidden { font-size: 0.1pt; visibility: hidden; }
 
+.binding, binding             { color: #9966FF; }
 .tclass, tclass               { color: red; }
 .tfree, tfree                 { color: #A020F0; }
 .tvar, tvar                   { color: #A020F0; }
diff -r 6629e2dedb00 -r f3a8476285c6 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -87,8 +87,8 @@
      Pretty.chunks (maps (Element.pretty_ctxt ctxt) context),
 
      Pretty.str "Definitions:",
-     Pretty.chunks (map (fn (bdg, th) => Pretty.block
-       [Pretty.str (Binding.str_of bdg ^ ":"),
+     Pretty.chunks (map (fn (b, th) => Pretty.block
+       [Binding.pretty b, Pretty.str ":",
         Pretty.brk 1,
         Display.pretty_thm ctxt th])
           defs),
diff -r 6629e2dedb00 -r f3a8476285c6 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -181,7 +181,7 @@
     val rel_frees = map fst (Term.add_frees rel [])
     val rel_vars = Term.add_vars rel []
     val rel_tvars = Term.add_tvars rel []
-    val qty_str = Binding.str_of qty_name ^ ": "
+    val qty_str = Binding.print qty_name ^ ": "
 
     val illegal_rel_vars =
       if null rel_vars andalso null rel_tvars then []
diff -r 6629e2dedb00 -r f3a8476285c6 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/Pure/General/binding.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -28,7 +28,7 @@
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding
   val conceal: binding -> binding
-  val str_of: binding -> string
+  val pretty: binding -> Pretty.T
   val print: binding -> string
   val bad: binding -> string
   val check: binding -> unit
@@ -121,13 +121,13 @@
 
 (* print *)
 
-fun str_of (Binding {prefix, qualifier, name, pos, ...}) =
-  if name = "" then ""
+fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
+  if name = "" then Pretty.str ""
   else
-    Long_Name.implode (map #1 (prefix @ qualifier) @ [name])
-    |> Markup.markup (Position.markup pos (Markup.binding name));
+    Pretty.markup (Position.markup pos Markup.binding)
+      [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))];
 
-val print = quote o str_of;
+val print = Pretty.str_of o pretty;
 
 
 (* check *)
diff -r 6629e2dedb00 -r f3a8476285c6 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/Pure/General/markup.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -15,7 +15,7 @@
   val nameN: string
   val name: string -> T -> T
   val kindN: string
-  val bindingN: string val binding: string -> T
+  val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val defN: string
   val refN: string
@@ -165,7 +165,7 @@
 
 (* formal entities *)
 
-val (bindingN, binding) = markup_string "binding" nameN;
+val (bindingN, binding) = markup_elem "binding";
 
 val entityN = "entity";
 fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
diff -r 6629e2dedb00 -r f3a8476285c6 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/Pure/Isar/element.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -129,8 +129,9 @@
 
 fun pretty_name_atts ctxt (b, atts) sep =
   if Binding.is_empty b andalso null atts then []
-  else [Pretty.block (Pretty.breaks
-    (Pretty.str (Binding.str_of b) :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
+  else
+    [Pretty.block (Pretty.breaks
+      (Binding.pretty b :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
 
 
 (* pretty_stmt *)
diff -r 6629e2dedb00 -r f3a8476285c6 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -41,6 +41,7 @@
           if null ts then Markup.no_output
           else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
           else if name = Markup.sendbackN then (special "W", special "X")
+          else if name = Markup.bindingN then (special "F", special "A")
           else if name = Markup.hiliteN then (special "0", special "1")
           else if name = Markup.tclassN then (special "B", special "A")
           else if name = Markup.tfreeN then (special "C", special "A")
diff -r 6629e2dedb00 -r f3a8476285c6 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Jun 25 15:08:58 2011 +0200
+++ b/src/Pure/ROOT.ML	Sat Jun 25 17:17:49 2011 +0200
@@ -44,8 +44,6 @@
 use "General/balanced_tree.ML";
 use "General/graph.ML";
 use "General/linear_set.ML";
-use "General/long_name.ML";
-use "General/binding.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/buffer.ML";
@@ -54,6 +52,8 @@
 use "General/xml_data.ML";
 use "General/yxml.ML";
 use "General/pretty.ML";
+use "General/long_name.ML";
+use "General/binding.ML";
 
 use "General/sha1.ML";
 if String.isPrefix "polyml" ml_system