tuned signature;
authorwenzelm
Sat Dec 19 15:14:59 2015 +0100 (2015-12-19)
changeset 618656dcc9e4f1aa6
parent 61864 3a5992c3410c
child 61866 6fa60a4f7e48
tuned signature;
src/Pure/General/pretty.ML
src/Pure/General/pretty.scala
src/Pure/General/symbol.ML
src/Pure/General/symbol.scala
src/Pure/Proof/extraction.ML
src/Pure/Thy/thy_output.ML
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Pure/General/pretty.ML	Sat Dec 19 14:47:52 2015 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Sat Dec 19 15:14:59 2015 +0100
     1.3 @@ -20,7 +20,6 @@
     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 @@ -81,23 +80,9 @@
    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 => 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
    1.23 -      replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
    1.24 -        Vector.sub (small_spaces, k mod 64);
    1.25 -end;
    1.26 -
    1.27 -
    1.28 -
    1.29  (** print mode operations **)
    1.30  
    1.31 -fun default_indent (_: string) = spaces;
    1.32 +fun default_indent (_: string) = Symbol.spaces;
    1.33  
    1.34  local
    1.35    val default = {indent = default_indent};
    1.36 @@ -115,7 +100,7 @@
    1.37  
    1.38  fun mode_indent x y = #indent (get_mode ()) x y;
    1.39  
    1.40 -val output_spaces = Output.output o spaces;
    1.41 +val output_spaces = Output.output o Symbol.spaces;
    1.42  val add_indent = Buffer.add o output_spaces;
    1.43  
    1.44  
    1.45 @@ -194,7 +179,7 @@
    1.46  fun big_list name prts = block (fbreaks (str name :: prts));
    1.47  
    1.48  fun indent 0 prt = prt
    1.49 -  | indent n prt = blk (0, [str (spaces n), prt]);
    1.50 +  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
    1.51  
    1.52  fun unbreakable (Break (_, wd, _)) = String (output_spaces wd, wd)
    1.53    | unbreakable (Block (m, es, _, indent, wd)) = Block (m, map unbreakable es, false, indent, wd)
     2.1 --- a/src/Pure/General/pretty.scala	Sat Dec 19 14:47:52 2015 +0100
     2.2 +++ b/src/Pure/General/pretty.scala	Sat Dec 19 15:14:59 2015 +0100
     2.3 @@ -11,20 +11,11 @@
     2.4  {
     2.5    /* spaces */
     2.6  
     2.7 -  val space = " "
     2.8 -
     2.9 -  private val static_spaces = space * 4000
    2.10 +  def spaces(n: Int): XML.Body =
    2.11 +    if (n == 0) Nil
    2.12 +    else List(XML.Text(Symbol.spaces(n)))
    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 -  def spaces_body(k: Int): XML.Body =
    2.22 -    if (k == 0) Nil
    2.23 -    else List(XML.Text(spaces(k)))
    2.24 +  val space: XML.Body = spaces(1)
    2.25  
    2.26  
    2.27    /* text metric -- standardized to width of space */
    2.28 @@ -61,7 +52,7 @@
    2.29    object Break
    2.30    {
    2.31      def apply(w: Int, i: Int = 0): XML.Tree =
    2.32 -      XML.Elem(Markup.Break(w, i), spaces_body(w))
    2.33 +      XML.Elem(Markup.Break(w, i), spaces(w))
    2.34  
    2.35      def unapply(tree: XML.Tree): Option[(Int, Int)] =
    2.36        tree match {
    2.37 @@ -73,9 +64,9 @@
    2.38    val FBreak = XML.Text("\n")
    2.39  
    2.40    def item(body: XML.Body): XML.Tree =
    2.41 -    Block(false, 2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
    2.42 +    Block(false, 2, XML.elem(Markup.BULLET, space) :: space ::: body)
    2.43  
    2.44 -  val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
    2.45 +  val Separator = List(XML.elem(Markup.SEPARATOR, space), FBreak)
    2.46    def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
    2.47  
    2.48  
    2.49 @@ -105,7 +96,7 @@
    2.50        def string(s: String): Text =
    2.51          if (s == "") this
    2.52          else copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
    2.53 -      def blanks(wd: Int): Text = string(spaces(wd))
    2.54 +      def blanks(wd: Int): Text = string(Symbol.spaces(wd))
    2.55        def content: XML.Body = tx.reverse
    2.56      }
    2.57  
    2.58 @@ -125,7 +116,7 @@
    2.59  
    2.60      def force_all(trees: XML.Body): XML.Body =
    2.61        trees flatMap {
    2.62 -        case Break(_, ind) => FBreak :: spaces_body(ind)
    2.63 +        case Break(_, ind) => FBreak :: spaces(ind)
    2.64          case tree => List(tree)
    2.65        }
    2.66  
    2.67 @@ -133,7 +124,7 @@
    2.68        trees match {
    2.69          case Nil => Nil
    2.70          case FBreak :: _ => trees
    2.71 -        case Break(_, ind) :: ts => FBreak :: spaces_body(ind) ::: ts
    2.72 +        case Break(_, ind) :: ts => FBreak :: spaces(ind) ::: ts
    2.73          case t :: ts => t :: force_next(ts)
    2.74        }
    2.75  
    2.76 @@ -190,8 +181,8 @@
    2.77      def fmt(tree: XML.Tree): XML.Body =
    2.78        tree match {
    2.79          case Block(_, _, body) => body.flatMap(fmt)
    2.80 -        case Break(wd, _) => spaces_body(wd)
    2.81 -        case FBreak => List(XML.Text(space))
    2.82 +        case Break(wd, _) => spaces(wd)
    2.83 +        case FBreak => space
    2.84          case XML.Wrapped_Elem(markup, body1, body2) =>
    2.85            List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
    2.86          case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
     3.1 --- a/src/Pure/General/symbol.ML	Sat Dec 19 14:47:52 2015 +0100
     3.2 +++ b/src/Pure/General/symbol.ML	Sat Dec 19 15:14:59 2015 +0100
     3.3 @@ -7,6 +7,7 @@
     3.4  signature SYMBOL =
     3.5  sig
     3.6    type symbol = string
     3.7 +  val spaces: int -> string
     3.8    val STX: symbol
     3.9    val DEL: symbol
    3.10    val space: symbol
    3.11 @@ -94,6 +95,16 @@
    3.12  
    3.13  val space = chr 32;
    3.14  
    3.15 +local
    3.16 +  val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
    3.17 +in
    3.18 +  fun spaces n =
    3.19 +    if n < 64 then Vector.sub (small_spaces, n)
    3.20 +    else
    3.21 +      replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^
    3.22 +        Vector.sub (small_spaces, n mod 64);
    3.23 +end;
    3.24 +
    3.25  val comment = "\\<comment>";
    3.26  
    3.27  fun is_char s = size s = 1;
     4.1 --- a/src/Pure/General/symbol.scala	Sat Dec 19 14:47:52 2015 +0100
     4.2 +++ b/src/Pure/General/symbol.scala	Sat Dec 19 15:14:59 2015 +0100
     4.3 @@ -21,6 +21,20 @@
     4.4    type Range = Text.Range
     4.5  
     4.6  
     4.7 +  /* spaces */
     4.8 +
     4.9 +  val space = " "
    4.10 +
    4.11 +  private val static_spaces = space * 4000
    4.12 +
    4.13 +  def spaces(n: Int): String =
    4.14 +  {
    4.15 +    require(n >= 0)
    4.16 +    if (n < static_spaces.length) static_spaces.substring(0, n)
    4.17 +    else space * n
    4.18 +  }
    4.19 +
    4.20 +
    4.21    /* ASCII characters */
    4.22  
    4.23    def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
    4.24 @@ -425,7 +439,7 @@
    4.25        "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
    4.26        "\\<Psi>", "\\<Omega>")
    4.27  
    4.28 -    val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n")
    4.29 +    val blanks = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
    4.30  
    4.31      val sym_chars =
    4.32        Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
     5.1 --- a/src/Pure/Proof/extraction.ML	Sat Dec 19 14:47:52 2015 +0100
     5.2 +++ b/src/Pure/Proof/extraction.ML	Sat Dec 19 15:14:59 2015 +0100
     5.3 @@ -121,7 +121,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 = writeln (Pretty.spaces d ^ s);
     5.8 +fun msg d s = writeln (Symbol.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/Pure/Thy/thy_output.ML	Sat Dec 19 14:47:52 2015 +0100
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Dec 19 15:14:59 2015 +0100
     6.3 @@ -602,7 +602,7 @@
     6.4  
     6.5  fun verbatim_text ctxt =
     6.6    if Config.get ctxt display then
     6.7 -    split_lines #> map (prefix (Pretty.spaces (Config.get ctxt indent))) #> cat_lines #>
     6.8 +    split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #>
     6.9      Latex.output_ascii #> Latex.environment "isabellett"
    6.10    else
    6.11      split_lines #>
     7.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 19 14:47:52 2015 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 19 15:14:59 2015 +0100
     7.3 @@ -299,7 +299,7 @@
     7.4        def string_width(s: String): Double =
     7.5          painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
     7.6  
     7.7 -      val unit = string_width(Pretty.space) max 1.0
     7.8 +      val unit = string_width(Symbol.space) max 1.0
     7.9        val average = string_width("mix") / (3 * unit)
    7.10        def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
    7.11      }