# HG changeset patch
# User wenzelm
# Date 1728232475 -7200
# Node ID 7cacedbddba71d8c71e75e2788bfc0aff40e9aa8
# Parent  080beab272645363c446a408c8c7d7e069aad9ec
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;

diff -r 080beab27264 -r 7cacedbddba7 NEWS
--- 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
diff -r 080beab27264 -r 7cacedbddba7 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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).
 
diff -r 080beab27264 -r 7cacedbddba7 src/Pure/General/pretty.ML
--- 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 =
diff -r 080beab27264 -r 7cacedbddba7 src/Pure/General/pretty.scala
--- 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
diff -r 080beab27264 -r 7cacedbddba7 src/Pure/ML/ml_pretty.ML
--- 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;
diff -r 080beab27264 -r 7cacedbddba7 src/Pure/PIDE/markup.ML
--- 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 []));
 
diff -r 080beab27264 -r 7cacedbddba7 src/Pure/PIDE/markup.scala
--- 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
   }
diff -r 080beab27264 -r 7cacedbddba7 src/Pure/Syntax/printer.ML
--- 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
diff -r 080beab27264 -r 7cacedbddba7 src/Pure/Syntax/syntax_ext.ML
--- 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};
diff -r 080beab27264 -r 7cacedbddba7 src/Pure/Syntax/syntax_phases.ML
--- 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