--- a/src/Doc/Isar_Ref/Proof_Script.thy Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Sat Dec 19 23:19:10 2015 +0100
@@ -102,8 +102,8 @@
apply} sequences.
The current goal state, which is essentially a hidden part of the Isar/VM
- configurtation, is turned into a proof context and remaining conclusion.
- This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
+ configuration, is turned into a proof context and remaining conclusion.
+ This corresponds to @{command fix}~/ @{command assume}~/ @{command show} in
structured proofs, but the text of the parameters, premises and conclusion
is not given explicitly.
--- a/src/Pure/General/pretty.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/General/pretty.ML Sat Dec 19 23:19:10 2015 +0100
@@ -12,28 +12,27 @@
breaking information. A "break" inserts a newline if the text until
the next break is too long to fit on the current line. After the newline,
text is indented to the level of the enclosing block. Normally, if a block
-is broken then all enclosing blocks will also be broken. Only "inconsistent
-breaks" are provided.
+is broken then all enclosing blocks will also be broken.
-The stored length of a block is used in breakdist (to treat each inner block as
+The stored length of a block is used in break_dist (to treat each inner block as
a unit for breaking).
*)
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
+ val make_block: Output.output * Output.output -> bool -> int -> T list -> T
val str: string -> T
val brk: int -> T
+ val brk_indent: int -> int -> T
val fbrk: T
val breaks: T list -> T list
val fbreaks: T list -> T list
val blk: int * T list -> T
val block: T list -> T
val strs: string list -> T
- val raw_markup: Output.output * Output.output -> int * T list -> T
val markup: Markup.T -> T list -> T
val mark: Markup.T -> T -> T
val mark_str: Markup.T * string -> 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;
@@ -123,41 +108,40 @@
(** printing items: compound phrases, strings, and breaks **)
abstype T =
- Block of (Output.output * Output.output) * T list * int * int
- (*markup output, body, indentation, length*)
- | String of Output.output * int (*text, length*)
- | Break of bool * int (*mandatory flag, width if not taken*)
+ Block of (Output.output * Output.output) * bool * int * T list * int
+ (*markup output, consistent, indentation, body, length*)
+ | Break of bool * int * int (*mandatory flag, width if not taken, extra indentation if taken*)
+ | Str of Output.output * int (*text, length*)
with
-fun length (Block (_, _, _, len)) = len
- | length (String (_, len)) = len
- | length (Break (_, wd)) = wd;
+fun length (Block (_, _, _, _, len)) = len
+ | length (Break (_, wd, _)) = wd
+ | length (Str (_, len)) = len;
+
+fun body_length [] len = len
+ | body_length (e :: es) len = body_length es (length e + len);
+
+fun make_block m consistent indent es = Block (m, consistent, indent, es, body_length es 0);
+fun markup_block m indent es = make_block (Markup.output m) false indent es;
(** derived operations to create formatting expressions **)
-val str = String o Output.output_width;
+val str = Str o Output.output_width;
-fun brk wd = Break (false, wd);
-val fbrk = Break (true, 1);
+fun brk wd = Break (false, wd, 0);
+fun brk_indent wd ind = Break (false, wd, ind);
+val fbrk = Break (true, 1, 0);
fun breaks prts = Library.separate (brk 1) prts;
fun fbreaks prts = Library.separate fbrk prts;
-fun raw_markup m (indent, es) =
- let
- fun sum [] k = k
- | sum (e :: es) k = sum es (length e + k);
- in Block (m, es, indent, sum es 0) end;
-
-fun markup_block m arg = raw_markup (Markup.output m) arg;
-
-val blk = markup_block Markup.empty;
+fun blk (ind, es) = markup_block Markup.empty ind es;
fun block prts = blk (2, prts);
val strs = block o breaks o map str;
-fun markup m prts = markup_block m (0, prts);
+fun markup m = markup_block m 0;
fun mark m prt = if m = Markup.empty then prt else markup m [prt];
fun mark_str (m, s) = mark m (str s);
fun marks_str (ms, s) = fold_rev mark ms (str s);
@@ -195,11 +179,12 @@
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, indent, wd)
- | unbreakable (e as String _) = e;
+fun unbreakable (Block (m, consistent, indent, es, len)) =
+ Block (m, consistent, indent, map unbreakable es, len)
+ | unbreakable (Break (_, wd, _)) = Str (output_spaces wd, wd)
+ | unbreakable (e as Str _) = e;
@@ -247,15 +232,17 @@
(*Add the lengths of the expressions until the next Break; if no Break then
include "after", to account for text following this block.*)
-fun breakdist (Break _ :: _, _) = 0
- | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
- | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
- | breakdist ([], after) = after;
+fun break_dist (Break _ :: _, _) = 0
+ | break_dist (e :: es, after) = length e + break_dist (es, after)
+ | break_dist ([], after) = after;
+
+val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
+val force_all = map force_break;
(*Search for the next break (at this or higher levels) and force it to occur.*)
-fun forcenext [] = []
- | forcenext (Break _ :: es) = fbrk :: es
- | forcenext (e :: es) = e :: forcenext es;
+fun force_next [] = []
+ | force_next ((e as Break _) :: es) = force_break e :: es
+ | force_next (e :: es) = e :: force_next es;
in
@@ -270,29 +257,31 @@
fun format ([], _, _) text = text
| format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
(case e of
- Block ((bg, en), bes, indent, _) =>
+ Block ((bg, en), consistent, indent, bes, blen) =>
let
val pos' = pos + indent;
val pos'' = pos' mod emergencypos;
val block' =
if pos' < emergencypos then (ind |> add_indent indent, pos')
else (add_indent pos'' Buffer.empty, pos'');
+ val d = break_dist (es, after)
+ val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes;
val btext: text = text
|> control bg
- |> format (bes, block', breakdist (es, after))
+ |> format (bes', block', d)
|> control en;
(*if this block was broken then force the next break*)
- val es' = if nl < #nl btext then forcenext es else es;
+ val es' = if nl < #nl btext then force_next es else es;
in format (es', block, after) btext end
- | Break (force, wd) =>
+ | Break (force, wd, ind) =>
(*no break if text to next break fits on this line
or if breaking would add only breakgain to space*)
format (es, block, after)
(if not force andalso
- pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
- then text |> blanks wd (*just insert wd blanks*)
- else text |> newline |> indentation block)
- | String str => format (es, block, after) (string str text));
+ pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain)
+ then text |> blanks wd (*just insert wd blanks*)
+ else text |> newline |> indentation block |> blanks ind)
+ | Str str => format (es, block, after) (string str text));
in
#tx (format ([input], (Buffer.empty, 0), 0) empty)
end;
@@ -305,23 +294,23 @@
(*symbolic markup -- no formatting*)
fun symbolic prt =
let
- fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
- | out (Block ((bg, en), prts, indent, _)) =
+ fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
+ | out (Block ((bg, en), consistent, indent, prts, _)) =
Buffer.add bg #>
- Buffer.markup (Markup.block indent) (fold out prts) #>
+ Buffer.markup (Markup.block consistent indent) (fold out prts) #>
Buffer.add en
- | out (String (s, _)) = Buffer.add s
- | out (Break (false, wd)) =
- Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
- | out (Break (true, _)) = Buffer.add (Output.output "\n");
+ | out (Break (false, wd, ind)) =
+ Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
+ | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
+ | out (Str (s, _)) = Buffer.add s;
in out prt Buffer.empty end;
(*unformatted output*)
fun unformatted prt =
let
- fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
- | fmt (String (s, _)) = Buffer.add s
- | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
+ fun fmt (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
+ | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd)
+ | fmt (Str (s, _)) = Buffer.add s;
in fmt prt Buffer.empty end;
@@ -376,13 +365,15 @@
(** ML toplevel pretty printing **)
-fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
- | to_ML (String s) = ML_Pretty.String s
- | to_ML (Break b) = ML_Pretty.Break b;
+fun to_ML (Block (m, consistent, indent, prts, _)) =
+ ML_Pretty.Block (m, consistent, indent, map to_ML prts)
+ | to_ML (Break b) = ML_Pretty.Break b
+ | to_ML (Str s) = ML_Pretty.String s;
-fun from_ML (ML_Pretty.Block (m, prts, ind)) = raw_markup m (ind, map from_ML prts)
- | from_ML (ML_Pretty.String s) = String s
- | from_ML (ML_Pretty.Break b) = Break b;
+fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
+ make_block m consistent indent (map from_ML prts)
+ | from_ML (ML_Pretty.Break b) = Break b
+ | from_ML (ML_Pretty.String s) = Str s;
end;
--- a/src/Pure/General/pretty.scala Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/General/pretty.scala Sat Dec 19 23:19:10 2015 +0100
@@ -9,18 +9,23 @@
object Pretty
{
- /* spaces */
+ /* XML constructors */
- 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)))
+ val space: XML.Body = spaces(1)
- def spaces(k: Int): String =
- {
- require(k >= 0)
- if (k < static_spaces.length) static_spaces.substring(0, k)
- else space * k
- }
+ def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
+ XML.Elem(Markup.Block(consistent, indent), body)
+ def block(indent: Int, body: XML.Body): XML.Tree = block(false, indent, body)
+ def block(body: XML.Body): XML.Tree = block(2, body)
+
+ def brk(width: Int, indent: Int = 0): XML.Tree =
+ XML.Elem(Markup.Break(width, indent), spaces(width))
+
+ val fbrk: XML.Tree = XML.Text("\n")
+
+ val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
+ def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
/* text metric -- standardized to width of space */
@@ -40,51 +45,41 @@
/* markup trees with physical blocks and breaks */
- def block(body: XML.Body): XML.Tree = Block(2, body)
-
- object Block
- {
- def apply(i: Int, body: XML.Body): XML.Tree =
- XML.Elem(Markup.Block(i), body)
+ sealed abstract class Tree { def length: Double }
+ case class Block(
+ markup: Option[(Markup, Option[XML.Body])],
+ consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
+ case class Str(string: String, length: Double) extends Tree
+ case class Break(force: Boolean, width: Int, indent: Int) extends Tree
+ { def length: Double = width.toDouble }
- def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
- tree match {
- case XML.Elem(Markup.Block(i), body) => Some((i, body))
- case _ => None
- }
- }
+ val FBreak = Break(true, 1, 0)
- object Break
- {
- def apply(w: Int): XML.Tree =
- XML.Elem(Markup.Break(w), List(XML.Text(spaces(w))))
+ def make_block(
+ markup: Option[(Markup, Option[XML.Body])],
+ consistent: Boolean,
+ indent: Int,
+ body: List[Tree]): Tree =
+ Block(markup, consistent, indent, body, (0.0 /: body) { case (n, t) => n + t.length })
- def unapply(tree: XML.Tree): Option[Int] =
- tree match {
- case XML.Elem(Markup.Break(w), _) => Some(w)
- case _ => None
- }
- }
-
- val FBreak = XML.Text("\n")
-
- def item(body: XML.Body): XML.Tree =
- Block(2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
-
- val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
- def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
-
-
- /* standard form */
-
- def standard_form(body: XML.Body): XML.Body =
- body flatMap {
+ def make_tree(metric: Metric, xml: XML.Body): List[Tree] =
+ xml flatMap {
case XML.Wrapped_Elem(markup, body1, body2) =>
- List(XML.Wrapped_Elem(markup, body1, standard_form(body2)))
+ List(make_block(Some(markup, Some(body1)), false, 0, make_tree(metric, body2)))
case XML.Elem(markup, body) =>
- if (markup.name == Markup.ITEM) List(item(standard_form(body)))
- else List(XML.Elem(markup, standard_form(body)))
- case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
+ markup match {
+ case Markup.Block(consistent, indent) =>
+ List(make_block(None, consistent, indent, make_tree(metric, body)))
+ case Markup.Break(width, indent) =>
+ List(Break(false, width, indent))
+ case Markup(Markup.ITEM, _) =>
+ List(make_block(None, false, 2,
+ make_tree(metric, XML.elem(Markup.BULLET, space) :: space ::: body)))
+ case _ =>
+ List(make_block(Some((markup, None)), false, 0, make_tree(metric, body)))
+ }
+ case XML.Text(text) =>
+ Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
}
@@ -97,70 +92,68 @@
{
sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
{
- def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
- def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
- def blanks(wd: Int): Text = string(spaces(wd))
+ def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
+ def string(s: String, len: Double): Text =
+ copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
+ def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
def content: XML.Body = tx.reverse
}
val breakgain = margin / 20
val emergencypos = (margin / 2).round.toInt
- def content_length(tree: XML.Tree): Double =
- XML.traverse_text(List(tree))(0.0)(_ + metric(_))
-
- def breakdist(trees: XML.Body, after: Double): Double =
+ def break_dist(trees: List[Tree], after: Double): Double =
trees match {
- case Break(_) :: _ => 0.0
- case FBreak :: _ => 0.0
- case t :: ts => content_length(t) + breakdist(ts, after)
+ case (_: Break) :: _ => 0.0
+ case t :: ts => t.length + break_dist(ts, after)
case Nil => after
}
- def forcenext(trees: XML.Body): XML.Body =
+ def force_break(tree: Tree): Tree =
+ tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
+ def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
+
+ def force_next(trees: List[Tree]): List[Tree] =
trees match {
case Nil => Nil
- case FBreak :: _ => trees
- case Break(_) :: ts => FBreak :: ts
- case t :: ts => t :: forcenext(ts)
+ case (t: Break) :: ts => force_break(t) :: ts
+ case t :: ts => t :: force_next(ts)
}
- def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
+ def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
trees match {
case Nil => text
- case Block(indent, body) :: ts =>
+ case Block(markup, consistent, indent, body, blen) :: ts =>
val pos1 = (text.pos + indent).ceil.toInt
val pos2 = pos1 % emergencypos
- val blockin1 =
- if (pos1 < emergencypos) pos1
- else pos2
- val btext = format(body, blockin1, breakdist(ts, after), text)
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
+ val blockin1 = if (pos1 < emergencypos) pos1 else pos2
+ val d = break_dist(ts, after)
+ val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
+ val btext =
+ markup match {
+ case None => format(body1, blockin1, d, text)
+ case Some((m, markup_body)) =>
+ val btext0 = format(body1, blockin1, d, text.copy(tx = Nil))
+ val elem =
+ markup_body match {
+ case None => XML.Elem(m, btext0.content)
+ case Some(b) => XML.Wrapped_Elem(m, b, btext0.content)
+ }
+ btext0.copy(tx = elem :: text.tx)
+ }
+ val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
format(ts1, blockin, after, btext)
- case Break(wd) :: ts =>
- if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
+ case Break(force, wd, ind) :: ts =>
+ if (!force &&
+ text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
format(ts, blockin, after, text.blanks(wd))
- else format(ts, blockin, after, text.newline.blanks(blockin))
- case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
+ else format(ts, blockin, after, text.newline.blanks(blockin + ind))
- case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
- val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
- val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
- format(ts1, blockin, after, btext1)
-
- case XML.Elem(markup, body) :: ts =>
- val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
- val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
- val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
- format(ts1, blockin, after, btext1)
-
- case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
+ case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
}
-
- format(standard_form(input), 0, 0.0, Text()).content
+ format(make_tree(metric, input), 0, 0.0, Text()).content
}
def string_of(input: XML.Body, margin: Double = margin_default,
@@ -174,15 +167,17 @@
{
def fmt(tree: XML.Tree): XML.Body =
tree match {
- case Block(_, body) => body.flatMap(fmt)
- case Break(wd) => List(XML.Text(spaces(wd)))
- case FBreak => List(XML.Text(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)))
- case XML.Text(_) => List(tree)
+ case XML.Elem(markup, body) =>
+ markup match {
+ case Markup.Block(_, _) => body.flatMap(fmt)
+ case Markup.Break(wd, _) => spaces(wd)
+ case _ => List(XML.Elem(markup, body.flatMap(fmt)))
+ }
+ case XML.Text(s) => List(XML.Text(s.replace('\n', ' ')))
}
- standard_form(input).flatMap(fmt)
+ input.flatMap(fmt)
}
def str_of(input: XML.Body): String = XML.content(unformatted(input))
--- a/src/Pure/General/symbol.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/General/symbol.ML Sat Dec 19 23:19:10 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 20:02:51 2015 +0100
+++ b/src/Pure/General/symbol.scala Sat Dec 19 23:19:10 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/ML-Systems/ml_pretty.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/ML-Systems/ml_pretty.ML Sat Dec 19 23:19:10 2015 +0100
@@ -8,13 +8,13 @@
struct
datatype pretty =
- Block of (string * string) * pretty list * int |
+ Block of (string * string) * bool * int * pretty list |
String of string * int |
- Break of bool * int;
+ Break of bool * int * int;
-fun block prts = Block (("", ""), prts, 2);
+fun block prts = Block (("", ""), false, 2, prts);
fun str s = String (s, size s);
-fun brk wd = Break (false, wd);
+fun brk width = Break (false, width, 0);
fun pair pretty1 pretty2 ((x, y), depth: int) =
block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
@@ -28,4 +28,3 @@
in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
end;
-
--- a/src/Pure/ML-Systems/polyml.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Sat Dec 19 23:19:10 2015 +0100
@@ -132,11 +132,11 @@
val pretty_ml =
let
- fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd)
+ fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
| convert _ (PolyML.PrettyBlock (_, _,
[PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
- ML_Pretty.Break (true, 1)
- | convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
+ ML_Pretty.Break (true, 1, 0)
+ | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
let
fun property name default =
(case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
@@ -145,20 +145,20 @@
val bg = property "begin" "";
val en = property "end" "";
val len' = property "length" len;
- in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
+ in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
| convert len (PolyML.PrettyString s) =
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
in convert "" end;
-fun ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
- | ml_pretty (ML_Pretty.Break (true, _)) =
+fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
+ | ml_pretty (ML_Pretty.Break (true, _, _)) =
PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
[PolyML.PrettyString " "])
- | ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
+ | ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
let val context =
(if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
(if en = "" then [] else [PolyML.ContextProperty ("end", en)])
- in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
+ in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
| ml_pretty (ML_Pretty.String (s, len)) =
if len = size s then PolyML.PrettyString s
else PolyML.PrettyBlock
--- a/src/Pure/ML-Systems/smlnj.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Sat Dec 19 23:19:10 2015 +0100
@@ -115,12 +115,16 @@
let
fun str "" = ()
| str s = PrettyPrint.string pps s;
- fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
- (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
- List.app pprint prts; PrettyPrint.closeBox pps; str en)
+ fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
+ (str bg;
+ (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
+ (PrettyPrint.Rel (dest_int ind));
+ List.app pprint prts; PrettyPrint.closeBox pps;
+ str en)
| pprint (ML_Pretty.String (s, _)) = str s
- | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
- | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
+ | pprint (ML_Pretty.Break (false, width, offset)) =
+ PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
+ | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
in pprint end;
fun toplevel_pp context path pp =
--- a/src/Pure/PIDE/markup.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Dec 19 23:19:10 2015 +0100
@@ -64,9 +64,9 @@
val urlN: string val url: string -> T
val docN: string val doc: string -> T
val indentN: string
- val blockN: string val block: int -> T
val widthN: string
- val breakN: string val break: int -> T
+ val blockN: string val block: bool -> int -> T
+ val breakN: string val break: int -> int -> T
val fbreakN: string val fbreak: T
val itemN: string val item: T
val wordsN: string val words: T
@@ -377,11 +377,21 @@
(* pretty printing *)
+val consistentN = "consistent";
val indentN = "indent";
-val (blockN, block) = markup_int "block" indentN;
+val widthN = "width";
-val widthN = "width";
-val (breakN, break) = markup_int "break" widthN;
+val blockN = "block";
+fun block c i =
+ (blockN,
+ (if c then [(consistentN, print_bool c)] else []) @
+ (if i <> 0 then [(indentN, print_int i)] else []));
+
+val breakN = "break";
+fun break w i =
+ (breakN,
+ (if w <> 0 then [(widthN, print_int w)] else []) @
+ (if i <> 0 then [(indentN, print_int i)] else []));
val (fbreakN, fbreak) = markup_elem "fbreak";
--- a/src/Pure/PIDE/markup.scala Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Dec 19 23:19:10 2015 +0100
@@ -180,8 +180,41 @@
/* pretty printing */
- val Block = new Markup_Int("block", "indent")
- val Break = new Markup_Int("break", "width")
+ val Consistent = new Properties.Boolean("consistent")
+ val Indent = new Properties.Int("indent")
+ val Width = new Properties.Int("width")
+
+ object Block
+ {
+ val name = "block"
+ def apply(c: Boolean, i: Int): Markup =
+ Markup(name,
+ (if (c) Consistent(c) else Nil) :::
+ (if (i != 0) Indent(i) else Nil))
+ def unapply(markup: Markup): Option[(Boolean, Int)] =
+ if (markup.name == name) {
+ val c = Consistent.unapply(markup.properties).getOrElse(false)
+ val i = Indent.unapply(markup.properties).getOrElse(0)
+ Some((c, i))
+ }
+ else None
+ }
+
+ object Break
+ {
+ val name = "break"
+ def apply(w: Int, i: Int): Markup =
+ Markup(name,
+ (if (w != 0) Width(w) else Nil) :::
+ (if (i != 0) Indent(i) else Nil))
+ def unapply(markup: Markup): Option[(Int, Int)] =
+ if (markup.name == name) {
+ val w = Width.unapply(markup.properties).getOrElse(0)
+ val i = Indent.unapply(markup.properties).getOrElse(0)
+ Some((w, i))
+ }
+ else None
+ }
val ITEM = "item"
val BULLET = "bullet"
--- a/src/Pure/Proof/extraction.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Dec 19 23:19:10 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/Syntax/syntax_phases.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Dec 19 23:19:10 2015 +0100
@@ -750,7 +750,7 @@
let
val ((bg1, bg2), en) = typing_elem;
val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
- in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
+ in SOME (Pretty.make_block (bg, en) false 0 [pretty_ast Markup.empty t]) end
else NONE
and ofsort_trans ty s =
@@ -758,7 +758,7 @@
let
val ((bg1, bg2), en) = sorting_elem;
val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
- in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end
+ in SOME (Pretty.make_block (bg, en) false 0 [pretty_typ_ast Markup.empty ty]) end
else NONE
and pretty_typ_ast m ast = ast
--- a/src/Pure/Thy/thy_output.ML Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML Sat Dec 19 23:19:10 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/isabelle_sidekick.scala Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Dec 19 23:19:10 2015 +0100
@@ -179,7 +179,7 @@
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
val info_text =
- Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
+ Pretty.formatted(Library.separate(Pretty.fbrk, info.info), margin = 40.0)
.mkString
new DefaultMutableTreeNode(
--- a/src/Tools/jEdit/src/jedit_lib.scala Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sat Dec 19 23:19:10 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
}
--- a/src/Tools/jEdit/src/rendering.scala Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Dec 19 23:19:10 2015 +0100
@@ -506,7 +506,7 @@
/* tooltips */
private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
- Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
+ Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
private def timing_threshold: Double = options.real("jedit_timing_threshold")
@@ -585,7 +585,7 @@
case tips =>
val r = Text.Range(results.head.range.start, results.last.range.stop)
val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
- Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
+ Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
}
}
--- a/src/Tools/jEdit/src/state_dockable.scala Sat Dec 19 20:02:51 2015 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Sat Dec 19 23:19:10 2015 +0100
@@ -108,8 +108,6 @@
locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)
add(controls.peer, BorderLayout.NORTH)
- override def focusOnDefaultComponent { update_button.requestFocus }
-
/* main */