support for pretty blocks that are "open" and thus have no impact on formatting, only on markup;
effectively revert 2cb4a2970941 and unify pretty-printing in Scala and ML, following Scala before that change;
build error messages are properly formatted again (amending 320bcbf34849): "no_report" markup does not affect its enclosed line break anymore;
--- a/NEWS Sun Oct 06 13:02:33 2024 +0200
+++ b/NEWS Sun Oct 06 18:34:35 2024 +0200
@@ -22,6 +22,11 @@
so its declarations are applied immediately, but also named for later
re-use: "unbundle no b" etc.
+* Blocks for pretty-printing (of types, terms, props etc.) now support
+the option "open_block". Thus the block has no impact on formatting, but
+it may carry markup information, which is relevant both for input and
+output of inner syntax.
+
* Inner syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract
specification of the effect of 'translations' (or translation functions
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Oct 06 18:34:35 2024 +0200
@@ -399,6 +399,9 @@
\<^item> \<open>indent\<close> (natural number): the block indentation --- the same as for the
simple syntax without block properties.
+ \<^item> \<open>open_block\<close> (Boolean): this block has no impact on formatting, but it
+ may carry markup information.
+
\<^item> \<open>consistent\<close> (Boolean): this block has consistent breaks (if one break
is taken, all breaks are taken).
--- a/src/Pure/General/pretty.ML Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/General/pretty.ML Sun Oct 06 18:34:35 2024 +0200
@@ -31,11 +31,13 @@
val block0: T list -> T
val block1: T list -> T
val block: T list -> T
- type 'a block = {markup: 'a, consistent: bool, indent: int}
+ type 'a block = {markup: 'a, open_block: bool, consistent: bool, indent: int}
val make_block: Markup.output block -> T list -> T
val markup_block: Markup.T block -> T list -> T
val markup: Markup.T -> T list -> T
+ val markup_open: Markup.T -> T list -> T
val mark: Markup.T -> T -> T
+ val mark_open: Markup.T -> T -> T
val markup_blocks: Markup.T list block -> T list -> T
val str: string -> T
val dots: T
@@ -125,28 +127,39 @@
(* blocks with markup *)
-type 'a block = {markup: 'a, consistent: bool, indent: int}
+type 'a block = {markup: 'a, open_block: bool, consistent: bool, indent: int}
-fun make_block ({markup, consistent, indent}: Markup.output block) body =
- let val context = ML_Pretty.markup_context markup
+fun make_block ({markup, open_block, consistent, indent}: Markup.output block) body =
+ let
+ val context =
+ ML_Pretty.markup_context markup @
+ ML_Pretty.open_block_context open_block;
in from_ML (ML_Pretty.PrettyBlock (short_nat indent, consistent, context, map to_ML body)) end;
-fun markup_block ({markup, consistent, indent}: Markup.T block) body =
- make_block {markup = YXML.output_markup markup, consistent = consistent, indent = indent} body;
+fun markup_block ({markup, open_block, consistent, indent}: Markup.T block) body =
+ make_block
+ {markup = YXML.output_markup markup,
+ open_block = open_block,
+ consistent = consistent,
+ indent = indent} body;
-fun markup m = markup_block {markup = m, consistent = false, indent = 0};
+fun markup m = markup_block {markup = m, open_block = false, consistent = false, indent = 0};
+fun markup_open m = markup_block {markup = m, open_block = true, consistent = false, indent = 0};
fun mark m prt = if m = Markup.empty then prt else markup m [prt];
+fun mark_open m prt = if m = Markup.empty then prt else markup_open m [prt];
-fun markup_blocks ({markup, consistent, indent}: Markup.T list block) body =
- if forall Markup.is_empty markup andalso not consistent then blk (indent, body)
+fun markup_blocks ({markup, open_block, consistent, indent}: Markup.T list block) body =
+ if forall Markup.is_empty markup andalso not open_block andalso not consistent
+ then blk (indent, body)
else
let
val markups = filter_out Markup.is_empty markup;
val (ms, m) = if null markups then ([], Markup.empty) else split_last markups;
in
- fold_rev mark ms
- (markup_block {markup = m, consistent = consistent, indent = indent} body)
+ fold_rev mark_open ms
+ (markup_block
+ {markup = m, open_block = open_block, consistent = consistent, indent = indent} body)
end;
@@ -167,8 +180,8 @@
val strs = block o breaks o map str;
-fun mark_str (m, s) = mark m (str s);
-fun marks_str (ms, s) = fold_rev mark ms (str s);
+fun mark_str (m, s) = mark_open m (str s);
+fun marks_str (ms, s) = fold_rev mark_open ms (str s);
val mark_position = mark o Position.markup;
fun mark_str_position (pos, s) = mark_str (Position.markup pos, s);
@@ -258,14 +271,21 @@
(* output tree *)
datatype tree =
- Block of Markup.output * bool * int * tree list * int
- (*markup output, consistent, indentation, body, length*)
+ Block of
+ {markup: Markup.output,
+ open_block: bool,
+ consistent: bool,
+ indent: int,
+ body: tree list,
+ length: int}
| Break of bool * int * int (*mandatory flag, width if not taken, extra indentation if taken*)
- | Str of Output.output * int; (*string output, length*)
+ | Str of Output.output * int (*string output, length*)
+ | Out of Output.output; (*immediate output*)
-fun tree_length (Block (_, _, _, _, len)) = len
+fun tree_length (Block {length = len, ...}) = len
| tree_length (Break (_, wd, _)) = wd
- | tree_length (Str (_, len)) = len;
+ | tree_length (Str (_, len)) = len
+ | tree_length (Out _) = 0;
local
@@ -291,11 +311,17 @@
let
fun out (ML_Pretty.PrettyBlock (ind, consistent, context, body)) =
let
- val markup = #markup ops (ML_Pretty.context_markup context);
val indent = long_nat ind;
val body' = map out body;
- val len = if make_length then block_length indent body' else ~1;
- in Block (markup, consistent, indent, body', len) end
+ in
+ Block
+ {markup = #markup ops (ML_Pretty.context_markup context),
+ open_block = ML_Pretty.context_open_block context,
+ consistent = consistent,
+ indent = indent,
+ body = body',
+ length = if make_length then block_length indent body' else ~1}
+ end
| out (ML_Pretty.PrettyBreak (wd, ind)) = Break (false, long_nat wd, long_nat ind)
| out ML_Pretty.PrettyLineBreak = fbreak
| out (ML_Pretty.PrettyString s) = Str (#output ops s ||> force_nat)
@@ -374,7 +400,9 @@
fun format ([], _, _) text = text
| format (prt :: prts, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
(case prt of
- Block ((bg, en), consistent, indent, bes, blen) =>
+ Block {markup = (bg, en), open_block = true, body = bes, ...} =>
+ format (Out bg :: bes @ Out en :: prts, block, after) text
+ | Block {markup = (bg, en), consistent, indent, body = bes, length = blen, ...} =>
let
val pos' = pos + indent;
val pos'' = pos' mod emergencypos;
@@ -398,7 +426,8 @@
pos + wd <= Int.max (margin - break_dist (prts, after), blockin + breakgain)
then text |> blanks wd (*just insert wd blanks*)
else text |> linebreak |> indentation block |> blanks ind)
- | Str str => format (prts, block, after) (string str text));
+ | Str str => format (prts, block, after) (string str text)
+ | Out s => format (prts, block, after) (control s text));
in
#tx (format ([output_tree ops true input], (Buffer.empty, 0), 0) empty)
end;
@@ -419,15 +448,17 @@
let val (bg, en) = #markup ops (YXML.output_markup m)
in Bytes.add bg #> body #> Bytes.add en end;
- fun out (Block ((bg, en), _, _, [], _)) = Bytes.add bg #> Bytes.add en
- | out (Block ((bg, en), consistent, indent, prts, _)) =
- Bytes.add bg #>
- markup_bytes (Markup.block {consistent = consistent, indent = indent}) (fold out prts) #>
- Bytes.add en
+ fun out (Block {markup = (bg, en), body = [], ...}) = Bytes.add bg #> Bytes.add en
+ | out (Block {markup = (bg, en), open_block, consistent, indent, body = prts, ...}) =
+ let
+ val block_markup =
+ Markup.block {open_block = open_block, consistent = consistent, indent = indent};
+ in Bytes.add bg #> markup_bytes block_markup (fold out prts) #> Bytes.add en end
| out (Break (false, wd, ind)) =
markup_bytes (Markup.break {width = wd, indent = ind}) (output_spaces_bytes ops wd)
| out (Break (true, _, _)) = Bytes.add (output_newline ops)
- | out (Str (s, _)) = Bytes.add s;
+ | out (Str (s, _)) = Bytes.add s
+ | out (Out s) = Bytes.add s;
in Bytes.build o out o output_tree ops false end;
val symbolic_string_of = Bytes.content o symbolic_output;
@@ -437,9 +468,11 @@
fun unformatted ops =
let
- fun out (Block ((bg, en), _, _, prts, _)) = Bytes.add bg #> fold out prts #> Bytes.add en
+ fun out (Block ({markup = (bg, en), body = prts, ...})) =
+ Bytes.add bg #> fold out prts #> Bytes.add en
| out (Break (_, wd, _)) = output_spaces_bytes ops wd
- | out (Str (s, _)) = Bytes.add s;
+ | out (Str (s, _)) = Bytes.add s
+ | out (Out s) = Bytes.add s;
in Bytes.build o out o output_tree ops false end;
fun unformatted_string_of prt =
--- a/src/Pure/General/pretty.scala Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/General/pretty.scala Sun Oct 06 18:34:35 2024 +0200
@@ -20,8 +20,14 @@
val bullet: XML.Body = XML.elem(Markup.BULLET, space) :: space
- def block(body: XML.Body, consistent: Boolean = false, indent: Int = 2): XML.Tree =
- XML.Elem(Markup.Block(consistent = consistent, indent = indent), body)
+ def block(body: XML.Body,
+ open_block: Boolean = false,
+ consistent: Boolean = false,
+ indent: Int = 2
+ ): XML.Tree = {
+ val markup = Markup.Block(open_block = open_block, consistent = consistent, indent = indent)
+ XML.Elem(markup, body)
+ }
def brk(width: Int, indent: Int = 0): XML.Tree =
XML.Elem(Markup.Break(width = width, indent = indent), spaces(width))
@@ -65,6 +71,7 @@
private case class Block(
markup: Markup,
markup_body: Option[XML.Body],
+ open_block: Boolean,
consistent: Boolean,
indent: Int,
body: List[Tree],
@@ -80,6 +87,7 @@
private def make_block(body: List[Tree],
markup: Markup = Markup.Empty,
markup_body: Option[XML.Body] = None,
+ open_block: Boolean = false,
consistent: Boolean = false,
indent: Int = 0
): Tree = {
@@ -95,7 +103,7 @@
case Nil => len1
}
}
- Block(markup, markup_body, consistent, indent1, body, body_length(body, 0.0))
+ Block(markup, markup_body, open_block, consistent, indent1, body, body_length(body, 0.0))
}
@@ -161,15 +169,17 @@
List(make_block(make_tree(body2), markup = markup, markup_body = Some(body1)))
case XML.Elem(markup, body) =>
markup match {
- case Markup.Block(consistent, indent) =>
- List(make_block(make_tree(body), consistent = consistent, indent = indent))
+ case Markup.Block(open_block, consistent, indent) =>
+ List(
+ make_block(make_tree(body),
+ open_block = open_block, consistent = consistent, indent = indent))
case Markup.Break(width, indent) =>
List(Break(false, force_nat(width), force_nat(indent)))
case Markup(Markup.ITEM, _) =>
List(make_block(make_tree(bullet ::: body),
markup = Markup.Expression.item, indent = 2))
case _ =>
- List(make_block(make_tree(body), markup = markup))
+ List(make_block(make_tree(body), markup = markup, open_block = true))
}
case XML.Text(text) =>
Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
@@ -179,7 +189,13 @@
trees match {
case Nil => text
- case Block(markup, markup_body, consistent, indent, body, blen) :: ts =>
+ case (block: Block) :: ts if block.open_block =>
+ val btext = format(block.body, blockin, break_dist(ts, after), text.copy(tx = Nil))
+ val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
+ val btext1 = btext.copy(tx = XML.Elem(block.markup, btext.content) :: text.tx)
+ format(ts1, blockin, after, btext1)
+
+ case Block(markup, markup_body, _, consistent, indent, body, blen) :: ts =>
val pos1 = (text.pos + indent).ceil.toInt
val pos2 = pos1 % emergencypos
val blockin1 = if (pos1 < emergencypos) pos1 else pos2
--- a/src/Pure/ML/ml_pretty.ML Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML Sun Oct 06 18:34:35 2024 +0200
@@ -9,6 +9,8 @@
datatype context = datatype PolyML.context
val context_markup: PolyML.context list -> string * string
val markup_context: string * string -> PolyML.context list
+ val context_open_block: PolyML.context list -> bool
+ val open_block_context: bool -> PolyML.context list
datatype pretty = datatype PolyML.pretty
val block: pretty list -> pretty
val str: string -> pretty
@@ -29,7 +31,9 @@
structure ML_Pretty: ML_PRETTY =
struct
-(* context and markup *)
+(** context **)
+
+(* properties *)
datatype context = datatype PolyML.context;
@@ -38,6 +42,9 @@
SOME (ContextProperty (_, b)) => b
| _ => "");
+
+(* markup *)
+
val markup_bg = "markup_bg";
val markup_en = "markup_en";
@@ -52,6 +59,19 @@
(if en = "" then [] else [ContextProperty (markup_en, en)]);
+(* open_block flag *)
+
+val open_block = ContextProperty ("open_block", "true");
+
+val context_open_block = List.exists (fn c => c = open_block);
+
+fun open_block_context false = []
+ | open_block_context true = [open_block];
+
+
+
+(** pretty printing **)
+
(* datatype pretty with derived operations *)
datatype pretty = datatype PolyML.pretty;
--- a/src/Pure/PIDE/markup.ML Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/PIDE/markup.ML Sun Oct 06 18:34:35 2024 +0200
@@ -79,12 +79,13 @@
val docN: string val doc: string -> T
val toolN: string val tool: string -> T
val markupN: string
+ val open_blockN: string
val consistentN: string
val unbreakableN: string
val block_properties: string list
val indentN: string
val widthN: string
- val blockN: string val block: {consistent: bool, indent: int} -> T
+ val blockN: string val block: {open_block: bool, consistent: bool, indent: int} -> T
val breakN: string val break: {width: int, indent: int} -> T
val fbreakN: string val fbreak: T
val itemN: string val item: T
@@ -472,17 +473,19 @@
(* pretty printing *)
val markupN = "markup";
+val open_blockN = "open_block";
val consistentN = "consistent";
val unbreakableN = "unbreakable";
val indentN = "indent";
-val block_properties = [notationN, markupN, consistentN, unbreakableN, indentN];
+val block_properties = [notationN, markupN, open_blockN, consistentN, unbreakableN, indentN];
val widthN = "width";
val blockN = "block";
-fun block {consistent, indent} =
+fun block {open_block, consistent, indent} =
(blockN,
+ (if open_block then [(open_blockN, Value.print_bool open_block)] else []) @
(if consistent then [(consistentN, Value.print_bool consistent)] else []) @
(if indent <> 0 then [(indentN, Value.print_int indent)] else []));
--- a/src/Pure/PIDE/markup.scala Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/PIDE/markup.scala Sun Oct 06 18:34:35 2024 +0200
@@ -259,21 +259,24 @@
/* pretty printing */
+ val Open_Block = new Properties.Boolean("open_block")
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(consistent: Boolean = false, indent: Int = 0): Markup =
+ def apply(open_block: Boolean = false, consistent: Boolean = false, indent: Int = 0): Markup =
Markup(name,
+ (if (open_block) Open_Block(open_block) else Nil) :::
(if (consistent) Consistent(consistent) else Nil) :::
(if (indent != 0) Indent(indent) else Nil))
- def unapply(markup: Markup): Option[(Boolean, Int)] =
+ def unapply(markup: Markup): Option[(Boolean, Boolean, Int)] =
if (markup.name == name) {
+ val open_block = Open_Block.get(markup.properties)
val consistent = Consistent.get(markup.properties)
val indent = Indent.get(markup.properties)
- Some((consistent, indent))
+ Some((open_block, consistent, indent))
}
else None
}
--- a/src/Pure/Syntax/printer.ML Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/Syntax/printer.ML Sun Oct 06 18:34:35 2024 +0200
@@ -243,13 +243,14 @@
val (Ts, args') = synT m (symbs, args);
val T = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s);
in (T :: Ts, args') end
- | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
+ | synT m (Block (block, bsymbs) :: symbs, args) =
let
+ val {markup, open_block, consistent, unbreakable, indent} = block;
val (bTs, args') = synT m (bsymbs, args);
val (Ts, args'') = synT m (symbs, args');
- val T =
- Pretty.markup_blocks {markup = markup, consistent = consistent, indent = indent} bTs
- |> unbreakable ? Pretty.unbreakable;
+ val prt_block =
+ {markup = markup, open_block = open_block, consistent = consistent, indent = indent};
+ val T = Pretty.markup_blocks prt_block bTs |> unbreakable ? Pretty.unbreakable;
in (T :: Ts, args'') end
| synT m (Break i :: symbs, args) =
let
--- a/src/Pure/Syntax/syntax_ext.ML Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Sun Oct 06 18:34:35 2024 +0200
@@ -7,7 +7,8 @@
signature SYNTAX_EXT =
sig
datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
- type block = {markup: Markup.T list, consistent: bool, unbreakable: bool, indent: int}
+ type block =
+ {markup: Markup.T list, open_block: bool, consistent: bool, unbreakable: bool, indent: int}
val block_indent: int -> block
datatype xsymb =
Delim of string |
@@ -62,10 +63,11 @@
Space s: some white space for printing
Bg, Brk, En: blocks and breaks for pretty printing*)
-type block = {markup: Markup.T list, consistent: bool, unbreakable: bool, indent: int};
+type block =
+ {markup: Markup.T list, open_block: bool, consistent: bool, unbreakable: bool, indent: int};
fun block_indent indent : block =
- {markup = [], consistent = false, unbreakable = false, indent = indent};
+ {markup = [], open_block = false, consistent = false, unbreakable = false, indent = indent};
datatype xsymb =
Delim of string |
@@ -259,6 +261,7 @@
val block: block =
{markup = more_markups @ markups,
+ open_block = get_bool Markup.open_blockN props,
consistent = get_bool Markup.consistentN props,
unbreakable = get_bool Markup.unbreakableN props,
indent = get_nat Markup.indentN props};
--- a/src/Pure/Syntax/syntax_phases.ML Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Sun Oct 06 18:34:35 2024 +0200
@@ -803,7 +803,7 @@
val ((bg1, bg2), en) = if is_typing then typing_elem else sorting_elem;
val B = Pretty.symbolic_output (pretty_typ_ast Markup.empty A);
val bg = implode (bg1 :: Bytes.contents B @ [bg2]);
- val block = {markup = (bg, en), consistent = false, indent = 0};
+ val block = {markup = (bg, en), open_block = false, consistent = false, indent = 0};
in Unsynchronized.change cache (Ast.Table.update (A, block)); block end)
end;
in