# HG changeset patch
# User wenzelm
# Date 1344334226 -7200
# Node ID 85a3de10567de1d6d24b484665afe4859e257f04
# Parent  d408ff0abf2381527534bf0d1217054e7940f0f6
tuned signature -- make Pretty less dependent on Symbol;

diff -r d408ff0abf23 -r 85a3de10567d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Aug 07 10:28:04 2012 +0200
+++ b/src/Pure/General/pretty.ML	Tue Aug 07 12:10:26 2012 +0200
@@ -21,6 +21,7 @@
 
 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
@@ -69,9 +70,22 @@
 structure Pretty: PRETTY =
 struct
 
+(** spaces **)
+
+local
+  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i Symbol.space);
+in
+  fun spaces k =
+    if k < 64 then Vector.sub (small_spaces, k)
+    else Library.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) = Symbol.spaces;
+fun default_indent (_: string) = spaces;
 
 local
   val default = {indent = default_indent};
@@ -89,7 +103,7 @@
 
 fun mode_indent x y = #indent (get_mode ()) x y;
 
-val output_spaces = Output.output o Symbol.spaces;
+val output_spaces = Output.output o spaces;
 val add_indent = Buffer.add o output_spaces;
 
 
@@ -167,7 +181,7 @@
 fun big_list name prts = block (fbreaks (str name :: prts));
 
 fun indent 0 prt = prt
-  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
+  | indent n prt = blk (0, [str (spaces n), prt]);
 
 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
   | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
diff -r d408ff0abf23 -r 85a3de10567d src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Tue Aug 07 10:28:04 2012 +0200
+++ b/src/Pure/General/pretty.scala	Tue Aug 07 12:10:26 2012 +0200
@@ -12,6 +12,21 @@
 
 object Pretty
 {
+  /* spaces */
+
+  val spc = ' '
+  val space = " "
+
+  private val static_spaces = space * 4000
+
+  def spaces(k: Int): String =
+  {
+    require(k >= 0)
+    if (k < static_spaces.length) static_spaces.substring(0, k)
+    else space * k
+  }
+
+
   /* markup trees with physical blocks and breaks */
 
   def block(body: XML.Body): XML.Tree = Block(2, body)
@@ -33,7 +48,7 @@
   {
     def apply(w: Int): XML.Tree =
       XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
-        List(XML.Text(Symbol.spaces(w))))
+        List(XML.Text(spaces(w))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
@@ -59,7 +74,7 @@
   {
     def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
-    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
+    def blanks(wd: Int): Text = string(spaces(wd), wd.toDouble)
     def content: XML.Body = tx.reverse
   }
 
@@ -69,7 +84,7 @@
   def font_metric(metrics: FontMetrics): String => Double =
     if (metrics == null) ((s: String) => s.length.toDouble)
     else {
-      val unit = metrics.charWidth(Symbol.spc).toDouble
+      val unit = metrics.charWidth(spc).toDouble
       ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
     }
 
@@ -143,8 +158,8 @@
     def fmt(tree: XML.Tree): XML.Body =
       tree match {
         case Block(_, body) => body.flatMap(fmt)
-        case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
-        case FBreak => List(XML.Text(Symbol.space))
+        case Break(wd) => List(XML.Text(spaces(wd)))
+        case FBreak => List(XML.Text(space))
         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
diff -r d408ff0abf23 -r 85a3de10567d src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Aug 07 10:28:04 2012 +0200
+++ b/src/Pure/General/symbol.ML	Tue Aug 07 12:10:26 2012 +0200
@@ -10,7 +10,6 @@
   val STX: symbol
   val DEL: symbol
   val space: symbol
-  val spaces: int -> string
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
   val is_symbolic: symbol -> bool
@@ -92,15 +91,6 @@
 
 val space = chr 32;
 
-local
-  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i space);
-in
-  fun spaces k =
-    if k < 64 then Vector.sub (small_spaces, k)
-    else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
-      Vector.sub (small_spaces, k mod 64);
-end;
-
 fun is_char s = size s = 1;
 
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
diff -r d408ff0abf23 -r 85a3de10567d src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Aug 07 10:28:04 2012 +0200
+++ b/src/Pure/General/symbol.scala	Tue Aug 07 12:10:26 2012 +0200
@@ -15,21 +15,6 @@
   type Symbol = String
 
 
-  /* spaces */
-
-  val spc = ' '
-  val space = " "
-
-  private val static_spaces = space * 4000
-
-  def spaces(k: Int): String =
-  {
-    require(k >= 0)
-    if (k < static_spaces.length) static_spaces.substring(0, k)
-    else space * k
-  }
-
-
   /* ASCII characters */
 
   def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
@@ -345,7 +330,7 @@
       "\\<^isub>", "\\<^isup>")
 
     val blanks =
-      recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
+      recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
diff -r d408ff0abf23 -r 85a3de10567d src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Aug 07 10:28:04 2012 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Aug 07 12:10:26 2012 +0200
@@ -120,7 +120,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 = Output.urgent_message (Symbol.spaces d ^ s);
+fun msg d s = Output.urgent_message (Pretty.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 []));
diff -r d408ff0abf23 -r 85a3de10567d src/Tools/jEdit/src/html_panel.scala
--- a/src/Tools/jEdit/src/html_panel.scala	Tue Aug 07 10:28:04 2012 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala	Tue Aug 07 12:10:26 2012 +0200
@@ -134,7 +134,7 @@
       val (font_metrics, margin) =
         Swing_Thread.now {
           val metrics = getFontMetrics(font)
-          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
+          (metrics, (getWidth() / (metrics.charWidth(Pretty.spc) max 1) - 4) max 20)
         }
       if (current_font_metrics == null ||
           current_font_family != font_family ||