renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
authorwenzelm
Sun Dec 20 13:06:26 2015 +0100 (2015-12-20)
changeset 61877276ad4354069
parent 61876 669f47397249
child 61878 fa4dbb82732f
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
src/Doc/antiquote_setup.ML
src/HOL/Probability/measurable.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/SMT/smtlib.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/try0.ML
src/Pure/General/binding.ML
src/Pure/General/path.ML
src/Pure/General/pretty.ML
src/Pure/General/url.ML
src/Pure/Thy/thy_output.ML
src/Pure/context.ML
src/Pure/defs.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Sun Dec 20 13:03:41 2015 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Dec 20 13:06:26 2015 +0100
     1.3 @@ -130,13 +130,15 @@
     1.4                Output.output
     1.5                  (Thy_Output.string_of_margin ctxt
     1.6                    (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
     1.7 -              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
     1.8 +              "\\rulename{" ^
     1.9 +              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.10              #> space_implode "\\par\\smallskip%\n"
    1.11              #> Latex.environment "isabelle"
    1.12            else
    1.13              map (fn (p, name) =>
    1.14 -              Output.output (Pretty.str_of p) ^
    1.15 -              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.16 +              Output.output (Pretty.unformatted_string_of p) ^
    1.17 +              "\\rulename{" ^
    1.18 +              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    1.19              #> space_implode "\\par\\smallskip%\n"
    1.20              #> enclose "\\isa{" "}")));
    1.21  
     2.1 --- a/src/HOL/Probability/measurable.ML	Sun Dec 20 13:03:41 2015 +0100
     2.2 +++ b/src/HOL/Probability/measurable.ML	Sun Dec 20 13:06:26 2015 +0100
     2.3 @@ -204,7 +204,7 @@
     2.4  fun measurable_tac ctxt facts =
     2.5    let
     2.6      fun debug_fact msg thm () =
     2.7 -      msg ^ " " ^ Pretty.str_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
     2.8 +      msg ^ " " ^ Pretty.unformatted_string_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
     2.9  
    2.10      fun IF' c t i = COND (c i) (t i) no_tac
    2.11  
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Dec 20 13:03:41 2015 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Dec 20 13:06:26 2015 +0100
     3.3 @@ -280,9 +280,8 @@
     3.4  val maybe_quote = ATP_Util.maybe_quote
     3.5  
     3.6  fun pretty_maybe_quote keywords pretty =
     3.7 -  let val s = Pretty.str_of pretty in
     3.8 -    if maybe_quote keywords s = s then pretty else Pretty.quote pretty
     3.9 -  end
    3.10 +  let val s = Pretty.unformatted_string_of pretty
    3.11 +  in if maybe_quote keywords s = s then pretty else Pretty.quote pretty end
    3.12  
    3.13  val hashw = ATP_Util.hashw
    3.14  val hashw_string = ATP_Util.hashw_string
     4.1 --- a/src/HOL/Tools/SMT/smtlib.ML	Sun Dec 20 13:03:41 2015 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smtlib.ML	Sun Dec 20 13:06:26 2015 +0100
     4.3 @@ -186,6 +186,6 @@
     4.4    | pretty_tree (S trees) =
     4.5        Pretty.enclose "(" ")" (Pretty.separate "" (map pretty_tree trees))
     4.6  
     4.7 -val str_of = Pretty.str_of o pretty_tree
     4.8 +val str_of = Pretty.unformatted_string_of o pretty_tree
     4.9  
    4.10  end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Dec 20 13:03:41 2015 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Dec 20 13:06:26 2015 +0100
     5.3 @@ -163,7 +163,8 @@
     5.4  fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) =
     5.5    let
     5.6      val ths = Attrib.eval_thms ctxt [xthm]
     5.7 -    val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
     5.8 +    val bracket =
     5.9 +      implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src ctxt) args)
    5.10  
    5.11      fun nth_name j =
    5.12        (case xref of
     6.1 --- a/src/HOL/Tools/try0.ML	Sun Dec 20 13:03:41 2015 +0100
     6.2 +++ b/src/HOL/Tools/try0.ML	Sun Dec 20 13:06:26 2015 +0100
     6.3 @@ -163,7 +163,7 @@
     6.4  
     6.5  fun string_of_xthm (xref, args) =
     6.6    Facts.string_of_ref xref ^
     6.7 -  implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
     6.8 +  implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args);
     6.9  
    6.10  val parse_fact_refs =
    6.11    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
     7.1 --- a/src/Pure/General/binding.ML	Sun Dec 20 13:03:41 2015 +0100
     7.2 +++ b/src/Pure/General/binding.ML	Sun Dec 20 13:06:26 2015 +0100
     7.3 @@ -156,7 +156,7 @@
     7.4        [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
     7.5      |> Pretty.quote;
     7.6  
     7.7 -val print = Pretty.str_of o pretty;
     7.8 +val print = Pretty.unformatted_string_of o pretty;
     7.9  
    7.10  val pp = pretty o set_pos Position.none;
    7.11  
     8.1 --- a/src/Pure/General/path.ML	Sun Dec 20 13:03:41 2015 +0100
     8.2 +++ b/src/Pure/General/path.ML	Sun Dec 20 13:06:26 2015 +0100
     8.3 @@ -171,7 +171,7 @@
     8.4    let val s = implode_path path
     8.5    in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
     8.6  
     8.7 -val print = Pretty.str_of o pretty;
     8.8 +val print = Pretty.unformatted_string_of o pretty;
     8.9  
    8.10  
    8.11  (* base element *)
     9.1 --- a/src/Pure/General/pretty.ML	Sun Dec 20 13:03:41 2015 +0100
     9.2 +++ b/src/Pure/General/pretty.ML	Sun Dec 20 13:06:26 2015 +0100
     9.3 @@ -66,7 +66,7 @@
     9.4    val writeln: T -> unit
     9.5    val symbolic_output: T -> Output.output
     9.6    val symbolic_string_of: T -> string
     9.7 -  val str_of: T -> string
     9.8 +  val unformatted_string_of: T -> string
     9.9    val markup_chunks: Markup.T -> T list -> T
    9.10    val chunks: T list -> T
    9.11    val chunks2: T list -> T
    9.12 @@ -332,7 +332,7 @@
    9.13  val symbolic_output = Buffer.content o symbolic;
    9.14  val symbolic_string_of = Output.escape o symbolic_output;
    9.15  
    9.16 -val str_of = Output.escape o Buffer.content o unformatted;
    9.17 +val unformatted_string_of = Output.escape o Buffer.content o unformatted;
    9.18  
    9.19  
    9.20  (* chunks *)
    10.1 --- a/src/Pure/General/url.ML	Sun Dec 20 13:03:41 2015 +0100
    10.2 +++ b/src/Pure/General/url.ML	Sun Dec 20 13:06:26 2015 +0100
    10.3 @@ -81,7 +81,7 @@
    10.4  
    10.5  val pretty = Pretty.mark_str o `Markup.url o implode_url;
    10.6  
    10.7 -val print = Pretty.str_of o pretty;
    10.8 +val print = Pretty.unformatted_string_of o pretty;
    10.9  
   10.10  
   10.11  (*final declarations of this structure!*)
    11.1 --- a/src/Pure/Thy/thy_output.ML	Sun Dec 20 13:03:41 2015 +0100
    11.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Dec 20 13:06:26 2015 +0100
    11.3 @@ -592,8 +592,9 @@
    11.4          #> space_implode "\\isasep\\isanewline%\n"
    11.5          #> Latex.environment "isabelle"
    11.6        else
    11.7 -        map ((if Config.get ctxt break then string_of_margin ctxt else Pretty.str_of) #>
    11.8 -          Output.output)
    11.9 +        map
   11.10 +          ((if Config.get ctxt break then string_of_margin ctxt else Pretty.unformatted_string_of)
   11.11 +            #> Output.output)
   11.12          #> space_implode "\\isasep\\isanewline%\n"
   11.13          #> enclose "\\isa{" "}");
   11.14  
    12.1 --- a/src/Pure/context.ML	Sun Dec 20 13:03:41 2015 +0100
    12.2 +++ b/src/Pure/context.ML	Sun Dec 20 13:06:26 2015 +0100
    12.3 @@ -179,7 +179,7 @@
    12.4      val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
    12.5    in Pretty.str_list "{" "}" abbrev end;
    12.6  
    12.7 -val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
    12.8 +val str_of_thy = Pretty.unformatted_string_of o pretty_abbrev_thy;
    12.9  
   12.10  fun get_theory thy name =
   12.11    if theory_name thy <> name then
    13.1 --- a/src/Pure/defs.ML	Sun Dec 20 13:03:41 2015 +0100
    13.2 +++ b/src/Pure/defs.ML	Sun Dec 20 13:06:26 2015 +0100
    13.3 @@ -147,7 +147,8 @@
    13.4  fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
    13.5    Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
    13.6      i = j orelse disjoint_args (Ts, Us) orelse
    13.7 -      error ("Clash of specifications for " ^ Pretty.str_of (pretty_item context c) ^ ":\n" ^
    13.8 +      error ("Clash of specifications for " ^
    13.9 +        Pretty.unformatted_string_of (pretty_item context c) ^ ":\n" ^
   13.10          "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
   13.11          "  " ^ quote b ^ Position.here pos_b));
   13.12