# HG changeset patch # User wenzelm # Date 1731007792 -3600 # Node ID d9f791f75b8b640b4b72965acde3e14fd5adc36a # Parent 95b53559af80885bc8baf2bfb85af328d6963d91 clarified signature: more robust type XML.Elem; diff -r 95b53559af80 -r d9f791f75b8b src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Thu Nov 07 20:08:50 2024 +0100 +++ b/src/Pure/General/pretty.scala Thu Nov 07 20:29:52 2024 +0100 @@ -23,9 +23,11 @@ def block(body: XML.Body, consistent: Boolean = false, indent: Int = 2 - ): XML.Tree = XML.Elem(Markup.Block(consistent = consistent, indent = indent), body) + ): XML.Elem = XML.Elem(Markup.Block(consistent = consistent, indent = indent), body) - def brk(width: Int, indent: Int = 0): XML.Tree = + def string(s: String): XML.Elem = block(XML.string(s), indent = 0) + + def brk(width: Int, indent: Int = 0): XML.Elem = XML.Elem(Markup.Break(width = width, indent = indent), spaces(width)) val fbrk: XML.Tree = XML.newline @@ -43,7 +45,7 @@ en: String = ")", sep: XML.Body = comma, indent: Int = 2 - ): XML.Tree = Pretty.block(XML.enclose(bg, en, separate(ts, sep = sep)), indent = indent) + ): XML.Elem = Pretty.block(XML.enclose(bg, en, separate(ts, sep = sep)), indent = indent) /* text metric -- standardized to width of space */ diff -r 95b53559af80 -r d9f791f75b8b src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Thu Nov 07 20:08:50 2024 +0100 +++ b/src/Pure/PIDE/rendering.scala Thu Nov 07 20:29:52 2024 +0100 @@ -604,40 +604,47 @@ private sealed case class Tooltip_Info( range: Text.Range, timing: Timing = Timing.zero, - messages: List[(Long, XML.Tree)] = Nil, - rev_infos: List[(Boolean, Int, XML.Tree)] = Nil + messages: List[(Long, XML.Elem)] = Nil, + rev_infos: List[(Boolean, Int, XML.Elem)] = Nil ) { def add_timing(t: Timing): Tooltip_Info = copy(timing = timing + t) - def add_message(r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info = { + def add_message(r0: Text.Range, serial: Long, msg: XML.Elem): Tooltip_Info = { val r = snapshot.convert(r0) - if (range == r) copy(messages = (serial -> tree) :: messages) - else copy(range = r, messages = List(serial -> tree)) + if (range == r) copy(messages = (serial -> msg) :: messages) + else copy(range = r, messages = List(serial -> msg)) } - def add_info(r0: Text.Range, tree: XML.Tree, important: Boolean = true, ord: Int = 0): Tooltip_Info = { + def add_info(r0: Text.Range, info: XML.Elem, + important: Boolean = true, + ord: Int = 0 + ): Tooltip_Info = { val r = snapshot.convert(r0) - val entry = (important, ord, tree) + val entry = (important, ord, info) if (range == r) copy(rev_infos = entry :: rev_infos) else copy (range = r, rev_infos = List(entry)) } + def add_info_text(r0: Text.Range, text: String, ord: Int = 0): Tooltip_Info = + add_info(r0, Pretty.string(text), ord = ord) - def timing_info(tree: XML.Tree): Option[XML.Tree] = - tree match { - case XML.Elem(Markup(Markup.TIMING, _), _) => - if (timing.elapsed.seconds >= timing_threshold) Some(XML.Text(timing.message)) else None - case _ => Some(tree) + def timing_info(elem: XML.Elem): Option[XML.Elem] = + if (elem.markup.name == Markup.TIMING) { + if (timing.elapsed.seconds >= timing_threshold) { + Some(Pretty.string(timing.message)) + } + else None } - def infos(important: Boolean = true): List[XML.Tree] = + else Some(elem) + def infos(important: Boolean = true): List[XML.Elem] = for { - (is_important, _, tree) <- rev_infos.reverse.sortBy(_._2) if is_important == important - tree1 <- timing_info(tree) - } yield tree1 + (is_important, _, elem) <- rev_infos.reverse.sortBy(_._2) if is_important == important + elem1 <- timing_info(elem) + } yield elem1 } def perhaps_append_file(node_name: Document.Node.Name, name: String): String = if (Path.is_valid(name)) session.resources.append_path(node_name.master_dir, Path.explode(name)) else name - def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = { + def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Elem]]] = { val results = snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states => { @@ -648,8 +655,8 @@ case (info, Text.Info(r0, XML.Elem(Markup(name, props), _))) if Rendering.tooltip_message_elements(name) => - for ((i, tree) <- Command.State.get_result_proper(command_states, props)) - yield info.add_message(r0, i, tree) + for ((i, msg) <- Command.State.get_result_proper(command_states, props)) + yield info.add_message(r0, i, msg) case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _))) if kind != "" && kind != Markup.ML_DEF => @@ -658,7 +665,7 @@ if (name == "") kind1 else if (kind1 == "") quote(name) else kind1 + " " + quote(name) - val info1 = info.add_info(r0, XML.Text(txt1), ord = 2) + val info1 = info.add_info_text(r0, txt1, ord = 2) Some(if (kind == Markup.COMMAND) info1.add_info(r0, XML.elem(Markup.TIMING)) else info1) case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) => @@ -666,17 +673,17 @@ val text = if (name == file) "file " + quote(file) else "path " + quote(name) + "\nfile " + quote(file) - Some(info.add_info(r0, XML.Text(text))) + Some(info.add_info_text(r0, text)) case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) => val text = "doc " + quote(name) - Some(info.add_info(r0, XML.Text(text))) + Some(info.add_info_text(r0, text)) case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) => - Some(info.add_info(r0, XML.Text("URL " + quote(name)))) + Some(info.add_info_text(r0, "URL " + quote(name))) case (info, Text.Info(r0, XML.Elem(Markup.Command_Span(span), _))) => - Some(info.add_info(r0, XML.Text("command span " + quote(span.name)))) + Some(info.add_info_text(r0, "command span " + quote(span.name))) case (info, Text.Info(r0, XML.Elem(Markup(name, _), body))) if name == Markup.SORTING || name == Markup.TYPING => @@ -693,10 +700,10 @@ val text = if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" else "breakpoint (disabled)" - Some(info.add_info(r0, XML.Text(text))) + Some(info.add_info_text(r0, text)) case (info, Text.Info(r0, XML.Elem(Markup.Language(lang), _))) => - Some(info.add_info(r0, XML.Text("language: " + lang.description))) + Some(info.add_info_text(r0, "language: " + lang.description)) case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) => val a = kind.nonEmpty @@ -705,30 +712,30 @@ val description = if (!a && !b) "notation" else "notation: " + k + if_proper(a && b, " ") + if_proper(b, quote(name)) - Some(info.add_info(r0, XML.Text(description), ord = 1)) + Some(info.add_info_text(r0, description, ord = 1)) case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) => val description = if (kind.isEmpty) "expression" else "expression: " + Word.implode(Word.explode('_', kind)) - Some(info.add_info(r0, XML.Text(description), ord = 1)) + Some(info.add_info_text(r0, description, ord = 1)) case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) => - Some(info.add_info(r0, XML.Text("Markdown: paragraph"))) + Some(info.add_info_text(r0, "Markdown: paragraph")) case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) => - Some(info.add_info(r0, XML.Text("Markdown: item"))) + Some(info.add_info_text(r0, "Markdown: item")) case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) => - Some(info.add_info(r0, XML.Text("Markdown: " + kind))) + Some(info.add_info_text(r0, "Markdown: " + kind)) case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) => - Rendering.tooltip_descriptions.get(name).map(desc => info.add_info(r0, XML.Text(desc))) + Rendering.tooltip_descriptions.get(name).map(desc => info.add_info_text(r0, desc)) }).map(_.info) if (results.isEmpty) None else { val r = Text.Range(results.head.range.start, results.last.range.stop) val all_tips = - results.flatMap(_.messages).foldLeft(SortedMap.empty[Long, XML.Tree])(_ + _) + results.flatMap(_.messages).foldLeft(SortedMap.empty[Long, XML.Elem])(_ + _) .iterator.map(_._2).toList ::: results.flatMap(res => res.infos()) ::: results.flatMap(res => res.infos(important = false)).lastOption.toList