1.1 --- a/src/Pure/General/pretty.ML	Tue Aug 07 10:28:04 2012 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Aug 07 12:10:26 2012 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4  
     1.5  signature PRETTY =
     1.6  sig
     1.7 +  val spaces: int -> string
     1.8    val default_indent: string -> int -> Output.output
     1.9    val add_mode: string -> (string -> int -> Output.output) -> unit
    1.10    type T
    1.11 @@ -69,9 +70,22 @@
    1.12  structure Pretty: PRETTY =
    1.13  struct
    1.14  
    1.15 +(** spaces **)
    1.16 +
    1.17 +local
    1.18 +  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i Symbol.space);
    1.19 +in
    1.20 +  fun spaces k =
    1.21 +    if k < 64 then Vector.sub (small_spaces, k)
    1.22 +    else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
    1.23 +      Vector.sub (small_spaces, k mod 64);
    1.24 +end;
    1.25 +
    1.26 +
    1.27 +
    1.28  (** print mode operations **)
    1.29  
    1.30 -fun default_indent (_: string) = Symbol.spaces;
    1.31 +fun default_indent (_: string) = spaces;
    1.32  
    1.33  local
    1.34    val default = {indent = default_indent};
    1.35 @@ -89,7 +103,7 @@
    1.36  
    1.37  fun mode_indent x y = #indent (get_mode ()) x y;
    1.38  
    1.39 -val output_spaces = Output.output o Symbol.spaces;
    1.40 +val output_spaces = Output.output o spaces;
    1.41  val add_indent = Buffer.add o output_spaces;
    1.42  
    1.43  
    1.44 @@ -167,7 +181,7 @@
    1.45  fun big_list name prts = block (fbreaks (str name :: prts));
    1.46  
    1.47  fun indent 0 prt = prt
    1.48 -  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
    1.49 +  | indent n prt = blk (0, [str (spaces n), prt]);
    1.50  
    1.51  fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
    1.52    | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)

     2.1 --- a/src/Pure/General/pretty.scala	Tue Aug 07 10:28:04 2012 +0200
     2.2 +++ b/src/Pure/General/pretty.scala	Tue Aug 07 12:10:26 2012 +0200
     2.3 @@ -12,6 +12,21 @@
     2.4  
     2.5  object Pretty
     2.6  {
     2.7 +  /* spaces */
     2.8 +
     2.9 +  val spc = ' '
    2.10 +  val space = " "
    2.11 +
    2.12 +  private val static_spaces = space * 4000
    2.13 +
    2.14 +  def spaces(k: Int): String =
    2.15 +  {
    2.16 +    require(k >= 0)
    2.17 +    if (k < static_spaces.length) static_spaces.substring(0, k)
    2.18 +    else space * k
    2.19 +  }
    2.20 +
    2.21 +
    2.22    /* markup trees with physical blocks and breaks */
    2.23  
    2.24    def block(body: XML.Body): XML.Tree = Block(2, body)
    2.25 @@ -33,7 +48,7 @@
    2.26    {
    2.27      def apply(w: Int): XML.Tree =
    2.28        XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
    2.29 -        List(XML.Text(Symbol.spaces(w))))
    2.30 +        List(XML.Text(spaces(w))))
    2.31  
    2.32      def unapply(tree: XML.Tree): Option[Int] =
    2.33        tree match {
    2.34 @@ -59,7 +74,7 @@
    2.35    {
    2.36      def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
    2.37      def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
    2.38 -    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
    2.39 +    def blanks(wd: Int): Text = string(spaces(wd), wd.toDouble)
    2.40      def content: XML.Body = tx.reverse
    2.41    }
    2.42  
    2.43 @@ -69,7 +84,7 @@
    2.44    def font_metric(metrics: FontMetrics): String => Double =
    2.45      if (metrics == null) ((s: String) => s.length.toDouble)
    2.46      else {
    2.47 -      val unit = metrics.charWidth(Symbol.spc).toDouble
    2.48 +      val unit = metrics.charWidth(spc).toDouble
    2.49        ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
    2.50      }
    2.51  
    2.52 @@ -143,8 +158,8 @@
    2.53      def fmt(tree: XML.Tree): XML.Body =
    2.54        tree match {
    2.55          case Block(_, body) => body.flatMap(fmt)
    2.56 -        case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
    2.57 -        case FBreak => List(XML.Text(Symbol.space))
    2.58 +        case Break(wd) => List(XML.Text(spaces(wd)))
    2.59 +        case FBreak => List(XML.Text(space))
    2.60          case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
    2.61          case XML.Text(_) => List(tree)
    2.62        }

     3.1 --- a/src/Pure/General/symbol.ML	Tue Aug 07 10:28:04 2012 +0200
     3.2 +++ b/src/Pure/General/symbol.ML	Tue Aug 07 12:10:26 2012 +0200
     3.3 @@ -10,7 +10,6 @@
     3.4    val STX: symbol
     3.5    val DEL: symbol
     3.6    val space: symbol
     3.7 -  val spaces: int -> string
     3.8    val is_char: symbol -> bool
     3.9    val is_utf8: symbol -> bool
    3.10    val is_symbolic: symbol -> bool
    3.11 @@ -92,15 +91,6 @@
    3.12  
    3.13  val space = chr 32;
    3.14  
    3.15 -local
    3.16 -  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i space);
    3.17 -in
    3.18 -  fun spaces k =
    3.19 -    if k < 64 then Vector.sub (small_spaces, k)
    3.20 -    else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
    3.21 -      Vector.sub (small_spaces, k mod 64);
    3.22 -end;
    3.23 -
    3.24  fun is_char s = size s = 1;
    3.25  
    3.26  fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;

     4.1 --- a/src/Pure/General/symbol.scala	Tue Aug 07 10:28:04 2012 +0200
     4.2 +++ b/src/Pure/General/symbol.scala	Tue Aug 07 12:10:26 2012 +0200
     4.3 @@ -15,21 +15,6 @@
     4.4    type Symbol = String
     4.5  
     4.6  
     4.7 -  /* spaces */
     4.8 -
     4.9 -  val spc = ' '
    4.10 -  val space = " "
    4.11 -
    4.12 -  private val static_spaces = space * 4000
    4.13 -
    4.14 -  def spaces(k: Int): String =
    4.15 -  {
    4.16 -    require(k >= 0)
    4.17 -    if (k < static_spaces.length) static_spaces.substring(0, k)
    4.18 -    else space * k
    4.19 -  }
    4.20 -
    4.21 -
    4.22    /* ASCII characters */
    4.23  
    4.24    def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
    4.25 @@ -345,7 +330,7 @@
    4.26        "\\<^isub>", "\\<^isup>")
    4.27  
    4.28      val blanks =
    4.29 -      recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
    4.30 +      recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
    4.31  
    4.32      val sym_chars =
    4.33        Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")

     5.1 --- a/src/Pure/Proof/extraction.ML	Tue Aug 07 10:28:04 2012 +0200
     5.2 +++ b/src/Pure/Proof/extraction.ML	Tue Aug 07 12:10:26 2012 +0200
     5.3 @@ -120,7 +120,7 @@
     5.4  fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
     5.5  fun corr_name s vs = extr_name s vs ^ "_correctness";
     5.6  
     5.7 -fun msg d s = Output.urgent_message (Symbol.spaces d ^ s);
     5.8 +fun msg d s = Output.urgent_message (Pretty.spaces d ^ s);
     5.9  
    5.10  fun vars_of t = map Var (rev (Term.add_vars t []));
    5.11  fun frees_of t = map Free (rev (Term.add_frees t []));

     6.1 --- a/src/Tools/jEdit/src/html_panel.scala	Tue Aug 07 10:28:04 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Tue Aug 07 12:10:26 2012 +0200
     6.3 @@ -134,7 +134,7 @@
     6.4        val (font_metrics, margin) =
     6.5          Swing_Thread.now {
     6.6            val metrics = getFontMetrics(font)
     6.7 -          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
     6.8 +          (metrics, (getWidth() / (metrics.charWidth(Pretty.spc) max 1) - 4) max 20)
     6.9          }
    6.10        if (current_font_metrics == null ||
    6.11            current_font_family != font_family ||