merged

--- a/etc/options	Sun Jun 30 06:30:08 2024 +0000
+++ b/etc/options	Sun Jun 30 13:20:54 2024 +0200
@@ -393,12 +393,12 @@
   -- "maximum number of messages to keep SSH server connection alive (ignore value < 0)"
 
 
-section "Phabricator"
+section "Phabricator / Phorge"
 
-option phabricator_version_arcanist : string = "e46025f7a9146f9918bab9d6fbdf6ed1816db5b5"
+option phabricator_version_arcanist : string = "7f28d7266f81985096219a11b949561d70f052e4"
   -- "repository version for arcanist"
 
-option phabricator_version_phabricator : string = "2ba2cbaf9bbf8f88e910d3da0a3cd643e4879e8a"
+option phabricator_version_phabricator : string = "f2a01dca39280d78cc799cd602dc1fc7bc26f165"
   -- "repository version for phabricator"
 
 

--- a/src/Pure/PIDE/protocol_message.scala	Sun Jun 30 06:30:08 2024 +0000
+++ b/src/Pure/PIDE/protocol_message.scala	Sun Jun 30 13:20:54 2024 +0200
@@ -64,7 +64,7 @@
         List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
       case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
         List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
-      case XML.Wrapped_Elem(_, _, ts) => reports(props, ts)
+      case XML.Wrapped_Elem_Body(ts) => reports(props, ts)
       case XML.Elem(_, ts) => reports(props, ts)
       case XML.Text(_) => Nil
     }

--- a/src/Pure/PIDE/xml.scala	Sun Jun 30 06:30:08 2024 +0000
+++ b/src/Pure/PIDE/xml.scala	Sun Jun 30 13:20:54 2024 +0200
@@ -47,16 +47,24 @@
     def end_elem(name: String): Unit
 
     def traverse(trees: List[Tree]): Unit = {
+      @tailrec def trav_atomic(list: List[Trav]): List[Trav] =
+        list match {
+          case Text(s) :: rest => text(s); trav_atomic(rest)
+          case Elem(markup, Nil) :: rest =>
+            if (!markup.is_empty) elem(markup, end = true)
+            trav_atomic(rest)
+          case End(name) :: rest => end_elem(name); trav_atomic(rest)
+          case _ => list
+        }
+
       @tailrec def trav(list: List[Trav]): Unit =
-        (list : @unchecked) match {
+        (trav_atomic(list) : @unchecked) match {
           case Nil =>
-          case Text(s) :: rest => text(s); trav(rest)
-          case Elem(markup, body) :: rest =>
-            if (markup.is_empty) trav(body ::: rest)
-            else if (body.isEmpty) { elem(markup, end = true); trav(rest) }
-            else { elem(markup); trav(body ::: End(markup.name) :: rest) }
-          case End(name) :: rest => end_elem(name); trav(rest)
+          case Elem(markup, body) :: rest if body.nonEmpty =>
+            if (markup.is_empty) trav(trav_atomic(body) ::: rest)
+            else { elem(markup); trav(trav_atomic(body) ::: End(markup.name) :: rest) }
         }
+
       trav(trees)
     }
   }
@@ -110,6 +118,17 @@
       }
   }
 
+  object Wrapped_Elem_Body {
+    def unapply(tree: Tree): Option[Body] =
+      tree match {
+        case
+          XML.Elem(Markup(XML_ELEM, (XML_NAME, _) :: _),
+            XML.Elem(Markup(XML_BODY, Nil), _) :: body) =>
+          Some(body)
+        case _ => None
+      }
+  }
+
   object Root_Elem {
     def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body)
     def unapply(tree: Tree): Option[Body] =
@@ -126,7 +145,7 @@
     @tailrec def trav(x: A, list: List[Tree]): A =
       list match {
         case Nil => x
-        case XML.Wrapped_Elem(_, _, body) :: rest => trav(x, body ::: rest)
+        case XML.Wrapped_Elem_Body(body) :: rest => trav(x, body ::: rest)
         case XML.Elem(_, body) :: rest => trav(x, body ::: rest)
         case XML.Text(s) :: rest => trav(op(x, s), rest)
       }
@@ -136,6 +155,14 @@
   def text_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + s.length)
   def symbol_length(body: Body): Int = traverse_text(body, 0, (n, s) => n + Symbol.length(s))
 
+  def content_is_empty(body: Body): Boolean =
+    traverse_text(body, true, (b, s) => b && s.isEmpty)
+
+  def content_lines(body: Body): Int = {
+    val n = traverse_text(body, 0, (n, s) => n + Library.count_newlines(s))
+    if (n == 0 && content_is_empty(body)) 0 else n + 1
+  }
+
   def content(body: Body): String =
     Library.string_builder(hint = text_length(body)) { text =>
       traverse_text(body, (), (_, s) => text.append(s))
@@ -316,7 +343,7 @@
     val properties: T[Properties.T] =
       (props => List(XML.Elem(Markup(":", props), Nil)))
 
-    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
+    val string: T[String] = XML.string
 
     val long: T[Long] = (x => string(long_atom(x)))
 

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Jun 30 06:30:08 2024 +0000
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Jun 30 13:20:54 2024 +0200
@@ -250,9 +250,7 @@
           ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
 
       val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
-      val lines =
-        XML.traverse_text(formatted, if (XML.text_length(formatted) == 0) 0 else 1,
-          (n: Int, s: String) => n + Library.count_newlines(s))
+      val lines = XML.content_lines(formatted)
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =