tuned signature;

--- a/src/Pure/General/pretty.ML	Sat Dec 19 14:47:52 2015 +0100
+++ b/src/Pure/General/pretty.ML	Sat Dec 19 15:14:59 2015 +0100
@@ -20,7 +20,6 @@
 
 signature PRETTY =
 sig
-  val spaces: int -> string
   val default_indent: string -> int -> Output.output
   val add_mode: string -> (string -> int -> Output.output) -> unit
   type T
@@ -81,23 +80,9 @@
 structure Pretty: PRETTY =
 struct
 
-(** spaces **)
-
-local
-  val small_spaces = Vector.tabulate (65, fn i => replicate_string i Symbol.space);
-in
-  fun spaces k =
-    if k < 64 then Vector.sub (small_spaces, k)
-    else
-      replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
-        Vector.sub (small_spaces, k mod 64);
-end;
-
-
-
 (** print mode operations **)
 
-fun default_indent (_: string) = spaces;
+fun default_indent (_: string) = Symbol.spaces;
 
 local
   val default = {indent = default_indent};
@@ -115,7 +100,7 @@
 
 fun mode_indent x y = #indent (get_mode ()) x y;
 
-val output_spaces = Output.output o spaces;
+val output_spaces = Output.output o Symbol.spaces;
 val add_indent = Buffer.add o output_spaces;
 
 
@@ -194,7 +179,7 @@
 fun big_list name prts = block (fbreaks (str name :: prts));
 
 fun indent 0 prt = prt
-  | indent n prt = blk (0, [str (spaces n), prt]);
+  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
 
 fun unbreakable (Break (_, wd, _)) = String (output_spaces wd, wd)
   | unbreakable (Block (m, es, _, indent, wd)) = Block (m, map unbreakable es, false, indent, wd)

--- a/src/Pure/General/pretty.scala	Sat Dec 19 14:47:52 2015 +0100
+++ b/src/Pure/General/pretty.scala	Sat Dec 19 15:14:59 2015 +0100
@@ -11,20 +11,11 @@
 {
   /* spaces */
 
-  val space = " "
-
-  private val static_spaces = space * 4000
+  def spaces(n: Int): XML.Body =
+    if (n == 0) Nil
+    else List(XML.Text(Symbol.spaces(n)))
 
-  def spaces(k: Int): String =
-  {
-    require(k >= 0)
-    if (k < static_spaces.length) static_spaces.substring(0, k)
-    else space * k
-  }
-
-  def spaces_body(k: Int): XML.Body =
-    if (k == 0) Nil
-    else List(XML.Text(spaces(k)))
+  val space: XML.Body = spaces(1)
 
 
   /* text metric -- standardized to width of space */
@@ -61,7 +52,7 @@
   object Break
   {
     def apply(w: Int, i: Int = 0): XML.Tree =
-      XML.Elem(Markup.Break(w, i), spaces_body(w))
+      XML.Elem(Markup.Break(w, i), spaces(w))
 
     def unapply(tree: XML.Tree): Option[(Int, Int)] =
       tree match {
@@ -73,9 +64,9 @@
   val FBreak = XML.Text("\n")
 
   def item(body: XML.Body): XML.Tree =
-    Block(false, 2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
+    Block(false, 2, XML.elem(Markup.BULLET, space) :: space ::: body)
 
-  val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
+  val Separator = List(XML.elem(Markup.SEPARATOR, space), FBreak)
   def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
 
 
@@ -105,7 +96,7 @@
       def string(s: String): Text =
         if (s == "") this
         else copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
-      def blanks(wd: Int): Text = string(spaces(wd))
+      def blanks(wd: Int): Text = string(Symbol.spaces(wd))
       def content: XML.Body = tx.reverse
     }
 
@@ -125,7 +116,7 @@
 
     def force_all(trees: XML.Body): XML.Body =
       trees flatMap {
-        case Break(_, ind) => FBreak :: spaces_body(ind)
+        case Break(_, ind) => FBreak :: spaces(ind)
         case tree => List(tree)
       }
 
@@ -133,7 +124,7 @@
       trees match {
         case Nil => Nil
         case FBreak :: _ => trees
-        case Break(_, ind) :: ts => FBreak :: spaces_body(ind) ::: ts
+        case Break(_, ind) :: ts => FBreak :: spaces(ind) ::: ts
         case t :: ts => t :: force_next(ts)
       }
 
@@ -190,8 +181,8 @@
     def fmt(tree: XML.Tree): XML.Body =
       tree match {
         case Block(_, _, body) => body.flatMap(fmt)
-        case Break(wd, _) => spaces_body(wd)
-        case FBreak => List(XML.Text(space))
+        case Break(wd, _) => spaces(wd)
+        case FBreak => space
         case XML.Wrapped_Elem(markup, body1, body2) =>
           List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))

--- a/src/Pure/General/symbol.ML	Sat Dec 19 14:47:52 2015 +0100
+++ b/src/Pure/General/symbol.ML	Sat Dec 19 15:14:59 2015 +0100
@@ -7,6 +7,7 @@
 signature SYMBOL =
 sig
   type symbol = string
+  val spaces: int -> string
   val STX: symbol
   val DEL: symbol
   val space: symbol
@@ -94,6 +95,16 @@
 
 val space = chr 32;
 
+local
+  val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
+in
+  fun spaces n =
+    if n < 64 then Vector.sub (small_spaces, n)
+    else
+      replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^
+        Vector.sub (small_spaces, n mod 64);
+end;
+
 val comment = "\\<comment>";
 
 fun is_char s = size s = 1;

--- a/src/Pure/General/symbol.scala	Sat Dec 19 14:47:52 2015 +0100
+++ b/src/Pure/General/symbol.scala	Sat Dec 19 15:14:59 2015 +0100
@@ -21,6 +21,20 @@
   type Range = Text.Range
 
 
+  /* spaces */
+
+  val space = " "
+
+  private val static_spaces = space * 4000
+
+  def spaces(n: Int): String =
+  {
+    require(n >= 0)
+    if (n < static_spaces.length) static_spaces.substring(0, n)
+    else space * n
+  }
+
+
   /* ASCII characters */
 
   def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
@@ -425,7 +439,7 @@
       "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
       "\\<Psi>", "\\<Omega>")
 
-    val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n")
+    val blanks = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")

--- a/src/Pure/Proof/extraction.ML	Sat Dec 19 14:47:52 2015 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Dec 19 15:14:59 2015 +0100
@@ -121,7 +121,7 @@
 fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
 fun corr_name s vs = extr_name s vs ^ "_correctness";
 
-fun msg d s = writeln (Pretty.spaces d ^ s);
+fun msg d s = writeln (Symbol.spaces d ^ s);
 
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));

--- a/src/Pure/Thy/thy_output.ML	Sat Dec 19 14:47:52 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Dec 19 15:14:59 2015 +0100
@@ -602,7 +602,7 @@
 
 fun verbatim_text ctxt =
   if Config.get ctxt display then
-    split_lines #> map (prefix (Pretty.spaces (Config.get ctxt indent))) #> cat_lines #>
+    split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #>
     Latex.output_ascii #> Latex.environment "isabellett"
   else
     split_lines #>

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 19 14:47:52 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 19 15:14:59 2015 +0100
@@ -299,7 +299,7 @@
       def string_width(s: String): Double =
         painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
 
-      val unit = string_width(Pretty.space) max 1.0
+      val unit = string_width(Symbol.space) max 1.0
       val average = string_width("mix") / (3 * unit)
       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
     }