--- 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{" "}")));
--- 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
--- 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
--- 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;
--- 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
--- 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));
--- 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;
--- 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 *)
--- 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 *)
--- 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!*)
--- 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{" "}");
--- 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
--- 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));