# HG changeset patch
# User wenzelm
# Date 1450613186 -3600
# Node ID 276ad43540693a4c278876c89cfd9eeee6a8cd3a
# Parent  669f473972499b9541c701609459d251a8970407
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;

diff -r 669f47397249 -r 276ad4354069 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Doc/antiquote_setup.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -130,13 +130,15 @@
               Output.output
                 (Thy_Output.string_of_margin ctxt
                   (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
-              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
+              "\\rulename{" ^
+              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
             #> space_implode "\\par\\smallskip%\n"
             #> Latex.environment "isabelle"
           else
             map (fn (p, name) =>
-              Output.output (Pretty.str_of p) ^
-              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
+              Output.output (Pretty.unformatted_string_of p) ^
+              "\\rulename{" ^
+              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
             #> space_implode "\\par\\smallskip%\n"
             #> enclose "\\isa{" "}")));
 
diff -r 669f47397249 -r 276ad4354069 src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/HOL/Probability/measurable.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -204,7 +204,7 @@
 fun measurable_tac ctxt facts =
   let
     fun debug_fact msg thm () =
-      msg ^ " " ^ Pretty.str_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
+      msg ^ " " ^ Pretty.unformatted_string_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
 
     fun IF' c t i = COND (c i) (t i) no_tac
 
diff -r 669f47397249 -r 276ad4354069 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -280,9 +280,8 @@
 val maybe_quote = ATP_Util.maybe_quote
 
 fun pretty_maybe_quote keywords pretty =
-  let val s = Pretty.str_of pretty in
-    if maybe_quote keywords s = s then pretty else Pretty.quote pretty
-  end
+  let val s = Pretty.unformatted_string_of pretty
+  in if maybe_quote keywords s = s then pretty else Pretty.quote pretty end
 
 val hashw = ATP_Util.hashw
 val hashw_string = ATP_Util.hashw_string
diff -r 669f47397249 -r 276ad4354069 src/HOL/Tools/SMT/smtlib.ML
--- a/src/HOL/Tools/SMT/smtlib.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/HOL/Tools/SMT/smtlib.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -186,6 +186,6 @@
   | pretty_tree (S trees) =
       Pretty.enclose "(" ")" (Pretty.separate "" (map pretty_tree trees))
 
-val str_of = Pretty.str_of o pretty_tree
+val str_of = Pretty.unformatted_string_of o pretty_tree
 
 end;
diff -r 669f47397249 -r 276ad4354069 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -163,7 +163,8 @@
 fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) =
   let
     val ths = Attrib.eval_thms ctxt [xthm]
-    val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
+    val bracket =
+      implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src ctxt) args)
 
     fun nth_name j =
       (case xref of
diff -r 669f47397249 -r 276ad4354069 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/HOL/Tools/try0.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -163,7 +163,7 @@
 
 fun string_of_xthm (xref, args) =
   Facts.string_of_ref xref ^
-  implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
+  implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args);
 
 val parse_fact_refs =
   Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
diff -r 669f47397249 -r 276ad4354069 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Pure/General/binding.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -156,7 +156,7 @@
       [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
     |> Pretty.quote;
 
-val print = Pretty.str_of o pretty;
+val print = Pretty.unformatted_string_of o pretty;
 
 val pp = pretty o set_pos Position.none;
 
diff -r 669f47397249 -r 276ad4354069 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Pure/General/path.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -171,7 +171,7 @@
   let val s = implode_path path
   in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
 
-val print = Pretty.str_of o pretty;
+val print = Pretty.unformatted_string_of o pretty;
 
 
 (* base element *)
diff -r 669f47397249 -r 276ad4354069 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Pure/General/pretty.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -66,7 +66,7 @@
   val writeln: T -> unit
   val symbolic_output: T -> Output.output
   val symbolic_string_of: T -> string
-  val str_of: T -> string
+  val unformatted_string_of: T -> string
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
   val chunks2: T list -> T
@@ -332,7 +332,7 @@
 val symbolic_output = Buffer.content o symbolic;
 val symbolic_string_of = Output.escape o symbolic_output;
 
-val str_of = Output.escape o Buffer.content o unformatted;
+val unformatted_string_of = Output.escape o Buffer.content o unformatted;
 
 
 (* chunks *)
diff -r 669f47397249 -r 276ad4354069 src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Pure/General/url.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -81,7 +81,7 @@
 
 val pretty = Pretty.mark_str o `Markup.url o implode_url;
 
-val print = Pretty.str_of o pretty;
+val print = Pretty.unformatted_string_of o pretty;
 
 
 (*final declarations of this structure!*)
diff -r 669f47397249 -r 276ad4354069 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -592,8 +592,9 @@
         #> space_implode "\\isasep\\isanewline%\n"
         #> Latex.environment "isabelle"
       else
-        map ((if Config.get ctxt break then string_of_margin ctxt else Pretty.str_of) #>
-          Output.output)
+        map
+          ((if Config.get ctxt break then string_of_margin ctxt else Pretty.unformatted_string_of)
+            #> Output.output)
         #> space_implode "\\isasep\\isanewline%\n"
         #> enclose "\\isa{" "}");
 
diff -r 669f47397249 -r 276ad4354069 src/Pure/context.ML
--- a/src/Pure/context.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Pure/context.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -179,7 +179,7 @@
     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   in Pretty.str_list "{" "}" abbrev end;
 
-val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
+val str_of_thy = Pretty.unformatted_string_of o pretty_abbrev_thy;
 
 fun get_theory thy name =
   if theory_name thy <> name then
diff -r 669f47397249 -r 276ad4354069 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Pure/defs.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -147,7 +147,8 @@
 fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
   Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
     i = j orelse disjoint_args (Ts, Us) orelse
-      error ("Clash of specifications for " ^ Pretty.str_of (pretty_item context c) ^ ":\n" ^
+      error ("Clash of specifications for " ^
+        Pretty.unformatted_string_of (pretty_item context c) ^ ":\n" ^
         "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
         "  " ^ quote b ^ Position.here pos_b));