# HG changeset patch # User wenzelm # Date 1719746454 -7200 # Node ID 8cd4c7da199ae3572b48c7782f08f7dd4788f06a # Parent 7a2d9e3fcdd50588e82a077a871c1bcec722625c# Parent 00fcbb277dae17b6190c352f6c029fa826fea903 merged diff -r 7a2d9e3fcdd5 -r 8cd4c7da199a etc/options --- 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" diff -r 7a2d9e3fcdd5 -r 8cd4c7da199a src/Pure/PIDE/protocol_message.scala --- 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 } diff -r 7a2d9e3fcdd5 -r 8cd4c7da199a src/Pure/PIDE/xml.scala --- 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))) diff -r 7a2d9e3fcdd5 -r 8cd4c7da199a src/Tools/jEdit/src/pretty_tooltip.scala --- 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 =