# HG changeset patch
# User wenzelm
# Date 1444764450 -7200
# Node ID 636bb75e76836f7a1a0503ecf73c2dc3b6dca229
# Parent  46d6586eb04c7dcfcc6388b8c2dd91a203debea3
tuned signature (cf. XML.trim_blanks);

diff -r 46d6586eb04c -r 636bb75e7683 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Oct 13 20:58:59 2015 +0200
+++ b/src/Pure/General/symbol.ML	Tue Oct 13 21:27:30 2015 +0200
@@ -59,7 +59,7 @@
   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
   val split_words: symbol list -> string list
   val explode_words: string -> string list
-  val strip_blanks: string -> string
+  val trim_blanks: string -> string
   val bump_init: string -> string
   val bump_string: string -> string
   val length: symbol list -> int
@@ -503,7 +503,7 @@
 
 (* blanks *)
 
-fun strip_blanks s =
+fun trim_blanks s =
   sym_explode s
   |> take_prefix is_blank |> #2
   |> take_suffix is_blank |> #1
diff -r 46d6586eb04c -r 636bb75e7683 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Oct 13 20:58:59 2015 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Oct 13 21:27:30 2015 +0200
@@ -149,7 +149,7 @@
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
 val output_text =
-  Symbol.strip_blanks #> Symbol.explode #> output_ctrl_symbols;
+  Symbol.trim_blanks #> Symbol.explode #> output_ctrl_symbols;
 
 fun output_markup cmd txt = "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text txt ^ "%\n}\n";
 
@@ -158,7 +158,7 @@
   output_text txt ^
   "%\n\\end{isamarkup" ^ cmd ^ "}%\n";
 
-fun output_verbatim txt = "%\n" ^ Symbol.strip_blanks txt ^ "\n";
+fun output_verbatim txt = "%\n" ^ Symbol.trim_blanks txt ^ "\n";
 
 val markup_true = "\\isamarkuptrue%\n";
 val markup_false = "\\isamarkupfalse%\n";
diff -r 46d6586eb04c -r 636bb75e7683 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Oct 13 20:58:59 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Oct 13 21:27:30 2015 +0200
@@ -487,11 +487,11 @@
 
 (* basic pretty printing *)
 
-fun tweak_line ctxt s =
-  if Config.get ctxt display then s else Symbol.strip_blanks s;
+fun perhaps_trim ctxt =
+  not (Config.get ctxt display) ? Symbol.trim_blanks;
 
 fun pretty_text ctxt =
-  Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
+  Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines;
 
 fun pretty_text_report ctxt source =
  (Context_Position.report ctxt (Input.pos_of source)