# HG changeset patch # User wenzelm # Date 1731089912 -3600 # Node ID 37cff2ad31daeff7f0294f3e918cab599933c089 # Parent 5ad7c7f825d20fd7b94fc6fd7f1b29bb7b4e42b5# Parent 3796346f5bacb1b600c35c8c0969747a121a0e79 merged diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/GUI/font_metric.scala --- a/src/Pure/GUI/font_metric.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/GUI/font_metric.scala Fri Nov 08 19:18:32 2024 +0100 @@ -45,6 +45,18 @@ val space_width: Double = string_width(Symbol.space) override def unit: Double = space_width max 1.0 - override def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit + override def apply(s: String): Double = { + val s1 = + if (s.exists(c => Symbol.is_ascii_blank(c) && c != Symbol.space_char)) { + s.map(c => if (Symbol.is_ascii_blank(c)) Symbol.space_char else c) + } + else s + string_width(s1) / unit + } def average: Double = average_width / unit + + def pretty_margin(margin: Int, limit: Int = -1): Int = { + val m = (margin * average).toInt + (if (limit < 0) m else m min limit) max 20 + } } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/GUI/gui.scala Fri Nov 08 19:18:32 2024 +0100 @@ -222,17 +222,18 @@ /* zoom factor */ - private val Zoom_Factor = "([0-9]+)%?".r + private val Percent = "([0-9]+)%?".r class Zoom extends Selector[String]( List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%") .map(GUI.Selector.item) ) { - def factor: Int = parse(selection.item.toString) + def percent: Int = parse(selection.item.toString) + def scale: Double = 0.01 * percent private def parse(text: String): Int = text match { - case Zoom_Factor(s) => + case Percent(s) => val i = Integer.parseInt(s) if (10 <= i && i < 1000) i else 100 case _ => 100 diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/GUI/tree_view.scala diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/General/pretty.scala Fri Nov 08 19:18:32 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 5ad7c7f825d2 -r 37cff2ad31da src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/General/symbol.ML Fri Nov 08 19:18:32 2024 +0100 @@ -498,22 +498,22 @@ (** symbol output **) -(* length *) +(* metric *) -fun sym_len s = +fun metric1 s = if String.isPrefix "\092 fn n => sym_len s + n) ss 0; +fun metric ss = fold (fn s => fn n => metric1 s + n) ss 0; -fun output s = (s, sym_length (Symbol.explode s)); +fun output s = (s, metric (Symbol.explode s)); (*final declarations of this structure!*) val explode = Symbol.explode; -val length = sym_length; +val length = metric; end; diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/General/symbol.scala Fri Nov 08 19:18:32 2024 +0100 @@ -676,7 +676,7 @@ if (sym.startsWith("\\ Unit, - consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit + consume_output: (Document.Snapshot, Command.Results, List[XML.Elem]) => Unit ) { private val print_function = operation_name + "_query" diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/PIDE/rendering.scala Fri Nov 08 19:18:32 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,25 +665,25 @@ 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), _))) => val file = perhaps_append_file(snapshot.node_name, name) - val text = - if (name == file) "file " + quote(file) - else "path " + quote(name) + "\nfile " + quote(file) - Some(info.add_info(r0, XML.Text(text))) + val info1 = + if (name == file) info + else info.add_info_text(r0, "path " + quote(name)) + Some(info1.add_info_text(r0, "file " + quote(file))) 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 => @@ -690,13 +697,13 @@ important = false)) case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) => - val text = - if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" - else "breakpoint (disabled)" - Some(info.add_info(r0, XML.Text(text))) + val text = + if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" + else "breakpoint (disabled)" + 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 diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/System/program_progress.scala --- a/src/Pure/System/program_progress.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/System/program_progress.scala Fri Nov 08 19:18:32 2024 +0100 @@ -20,7 +20,7 @@ private var stop_time: Option[Time] = None def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) } - def output(): (Command.Results, XML.Body) = synchronized { + def output(): (Command.Results, XML.Elem) = synchronized { val output_text = output_buffer.toString val elapsed_time = stop_time.map(t => t - start_time) @@ -45,7 +45,7 @@ (results, message) } - (results, List(XML.elem(Markup.TRACING_MESSAGE, message))) + (results, XML.elem(Markup.TRACING_MESSAGE, message)) } } } @@ -58,12 +58,11 @@ private var _finished_programs: List[Program_Progress.Program] = Nil private var _running_program: Option[Program_Progress.Program] = None - def output(): (Command.Results, XML.Body) = synchronized { + def output(): (Command.Results, List[XML.Elem]) = synchronized { val programs = (_running_program.toList ::: _finished_programs).reverse val programs_output = programs.map(_.output()) val results = Command.Results.merge(programs_output.map(_._1)) - val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten - (results, body) + (results, programs_output.map(_._2)) } private def start_program(heading: String, title: String): Unit = synchronized { diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Fri Nov 08 19:18:32 2024 +0100 @@ -126,7 +126,7 @@ eds match { case e :: es => def insert_text(cmd: Option[Command], text: String): Linear_Set[Command] = - if (text == "") commands else commands.insert_after(cmd, Command.text(text)) + if (text == "") commands else commands.insert_after(cmd, Command.unparsed(text)) Document.Node.Commands.starts(commands.iterator).find { case (cmd, cmd_start) => diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Pure/Tools/debugger.scala Fri Nov 08 19:18:32 2024 +0100 @@ -216,7 +216,7 @@ } } - def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) = { + def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Elem]) = { val st = state.value val output = focus match { @@ -225,8 +225,8 @@ (for { (thread_name, results) <- st.output if thread_name == c.thread_name - (_, tree) <- results.iterator - } yield tree).toList + (_, msg) <- results.iterator + } yield msg).toList } (st.threads, output) } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Fri Nov 08 19:18:32 2024 +0100 @@ -82,8 +82,11 @@ case Some(node) => graphview.model.full_graph.get_node(node) match { case Nil => null - case content => - graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, content) + case List(tip: XML.Elem) => + graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, tip) + case body => + val tip = Pretty.block(body, indent = 0) + graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, tip) } case None => null } @@ -298,7 +301,7 @@ tooltip = "Save current graph layout as PNG or PDF" } - private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(0.01 * factor) } + private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(scale) } private val fit_window = new Button { action = Action("Fit to window") { fit_to_window() } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/Graphview/graphview.scala --- a/src/Tools/Graphview/graphview.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/Graphview/graphview.scala Fri Nov 08 19:18:32 2024 +0100 @@ -85,7 +85,7 @@ /* tooltips */ - def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null + def make_tooltip(parent: JComponent, x: Int, y: Int, tip: XML.Elem): String = null /* main colors */ diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/VSCode/src/pretty_text_panel.scala --- a/src/Tools/VSCode/src/pretty_text_panel.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/VSCode/src/pretty_text_panel.scala Fri Nov 08 19:18:32 2024 +0100 @@ -21,14 +21,14 @@ class Pretty_Text_Panel private( resources: VSCode_Resources, channel: Channel, - output: (String, Option[LSP.Decoration]) => JSON.T + output_json: (String, Option[LSP.Decoration]) => JSON.T ) { - private var current_body: XML.Body = Nil + private var current_output: List[XML.Elem] = Nil private var current_formatted: XML.Body = Nil private var margin: Double = resources.message_margin private val delay_margin = Delay.last(resources.output_delay, channel.Error_Logger) { - refresh(current_body) + refresh(current_output) } def update_margin(new_margin: Double): Unit = { @@ -36,12 +36,13 @@ delay_margin.invoke() } - def refresh(body: XML.Body): Unit = { - val formatted = Pretty.formatted(Pretty.separate(body), margin = margin, metric = Symbol.Metric) + def refresh(output: List[XML.Elem]): Unit = { + val formatted = + Pretty.formatted(Pretty.separate(output), margin = margin, metric = Symbol.Metric) if (formatted == current_formatted) return - current_body = body + current_output = output current_formatted = formatted if (resources.html_output) { @@ -57,7 +58,7 @@ } val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full) val html = node_context.make_html(elements, formatted) - val message = output(HTML.source(html).toString, None) + val message = output_json(HTML.source(html).toString, None) channel.write(message) } else { def convert_symbols(body: XML.Body): XML.Body = { @@ -83,8 +84,7 @@ }) .groupMap(_._2)(e => LSP.Decoration_Options(e._1, List())).toList - val message = output(text, Some(LSP.Decoration(decorations))) - channel.write(message) + channel.write(output_json(text, Some(LSP.Decoration(decorations)))) } } } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/VSCode/src/state_panel.scala --- a/src/Tools/VSCode/src/state_panel.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/VSCode/src/state_panel.scala Fri Nov 08 19:18:32 2024 +0100 @@ -70,9 +70,9 @@ private val print_state = new Query_Operation(server.editor, (), "print_state", _ => (), - (_, _, body) => - if (output_active.value && body.nonEmpty) { - pretty_panel.value.refresh(body) + (_, _, output) => + if (output_active.value && output.nonEmpty) { + pretty_panel.value.refresh(output) }) def locate(): Unit = print_state.locate_query() diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Fri Nov 08 19:18:32 2024 +0100 @@ -230,7 +230,7 @@ def open_popup(result: Completion.Result): Unit = { val font = painter.getFont.deriveFont( - Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale"))) + Font_Info.main_size(scale = PIDE.options.real("jedit_popup_font_scale"))) val range = result.range diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -67,14 +67,7 @@ /* pretty text area */ private val output: Output_Area = - new Output_Area(view, root_name = "Threads") { - override def handle_tree_selection(e: TreeSelectionEvent): Unit = { - update_focus() - update_vals() - } - - override def handle_resize(): Unit = pretty_text_area.zoom(zoom) - + new Output_Area(view, root_name = "Threads", split = true) { override def handle_update(): Unit = { val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) val (new_threads, new_output) = debugger.status(tree_selection()) @@ -82,7 +75,7 @@ if (new_threads != current_threads) update_tree(new_threads) if (new_output != current_output) { - pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output)) + pretty_text_area.update(new_snapshot, Command.Results.empty, new_output) } current_snapshot = new_snapshot @@ -236,17 +229,13 @@ tooltip = "Official Standard ML instead of Isabelle/ML" } - private val zoom = - new Font_Info.Zoom { override def changed(): Unit = output.handle_resize() } - private val controls = Wrap_Panel( List( break_button, continue_button, step_button, step_over_button, step_out_button, context_label, Component.wrap(context_field), - expression_label, Component.wrap(expression_field), eval_button, sml_button, - output.pretty_text_area.search_label, - output.pretty_text_area.search_field, zoom)) + expression_label, Component.wrap(expression_field), eval_button, sml_button) ::: + output.pretty_text_area.search_zoom_components) add(controls.peer, BorderLayout.NORTH) @@ -266,6 +255,11 @@ JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint()) } + output.tree.addTreeSelectionListener({ (e: TreeSelectionEvent) => + update_focus() + update_vals() + }) + /* main */ diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -30,24 +30,21 @@ process: Future[Unit] = Future.value(()), progress: Progress = new Progress, output_results: Command.Results = Command.Results.empty, - output_main: XML.Body = Nil, - output_more: XML.Body = Nil + output_main: List[XML.Elem] = Nil, + output_more: List[XML.Elem] = Nil ) { def running: Boolean = !process.is_finished def run(process: Future[Unit], progress: Progress, reset_pending: Boolean): State = copy(process = process, progress = progress, pending = if (reset_pending) false else pending) - def output(results: Command.Results, body: XML.Body): State = - copy(output_results = results, output_main = body, output_more = Nil) + def output(results: Command.Results, main: List[XML.Elem]): State = + copy(output_results = results, output_main = main, output_more = Nil) - def finish(body: XML.Body): State = - copy(process = Future.value(()), output_more = body) + def finish(more: List[XML.Elem]): State = + copy(process = Future.value(()), output_more = more) - def output_body: XML.Body = - output_main ::: - (if (output_main.nonEmpty && output_more.nonEmpty) Pretty.Separator else Nil) ::: - output_more + def output_all: List[XML.Elem] = output_main ::: output_more def reset(): State = { process.cancel() @@ -74,7 +71,7 @@ private def show_state(): Unit = GUI_Thread.later { val st = current_state.value - pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_body) + pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all) if (st.running) process_indicator.update("Running document build process ...", 15) else if (st.pending) process_indicator.update("Waiting for pending document content ...", 5) @@ -91,8 +88,7 @@ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation - private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } - private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) } + private def handle_resize(): Unit = pretty_text_area.zoom() private val delay_resize: Delay = Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } @@ -139,8 +135,8 @@ current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st)) private def output_process(progress: Log_Progress): Unit = { - val (results, body) = progress.output() - current_state.change(_.output(results, body)) + val (results, main) = progress.output() + current_state.change(_.output(results, main)) } private def pending_process(): Unit = @@ -153,7 +149,7 @@ } } - private def finish_process(output: XML.Body): Unit = + private def finish_process(output: List[XML.Elem]): Unit = current_state.change { st => if (st.pending) { delay_auto_build.revoke() @@ -231,7 +227,7 @@ progress.stop_program() output_process(progress) progress.stop() - finish_process(Pretty.separate(msgs)) + finish_process(msgs) show_page(output_page) } @@ -352,7 +348,7 @@ override def clicked(): Unit = cancel_process() } - private val output_controls = Wrap_Panel(List(cancel_button, zoom)) + private val output_controls = Wrap_Panel(List(cancel_button, pretty_text_area.zoom_component)) private val output_page = new TabbedPane.Page("Output", new BorderPanel { diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -23,15 +23,14 @@ for (section <- doc_contents.sections) { tree.root.add(Tree_View.Node(section.title)) - for (entry <- section.entries) { - tree.root.getLastChild.asInstanceOf[Tree_View.Node].add(Tree_View.Node(entry)) - } + val last_node = tree.root.getLastChild.asInstanceOf[Tree_View.Node] + for (entry <- section.entries) last_node.add(Tree_View.Node(entry)) } override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow - private def action(node: Tree_View.Node): Unit = { - node match { + private def action(obj: AnyRef): Unit = { + obj match { case Tree_View.Node(entry: Doc.Entry) => if (entry.path.is_pdf) PIDE.editor.goto_doc(view, entry.path) else PIDE.editor.goto_file(true, view, File.platform_path(entry.path)) @@ -44,12 +43,7 @@ if (e.getKeyCode == KeyEvent.VK_ENTER) { e.consume() val path = tree.getSelectionPath - if (path != null) { - path.getLastPathComponent match { - case node: Tree_View.Node => action(node) - case _ => - } - } + if (path != null) action(path.getLastPathComponent) } } }) @@ -57,10 +51,9 @@ override def mouseClicked(e: MouseEvent): Unit = { val click = tree.getPathForLocation(e.getX, e.getY) if (click != null && e.getClickCount == 1) { - (click.getLastPathComponent, tree.getLastSelectedPathComponent) match { - case (node: Tree_View.Node, node1: Tree_View.Node) if node == node1 => action(node) - case _ => - } + val click_node = click.getLastPathComponent + val path_node = tree.getLastSelectedPathComponent + if (click_node == path_node) action(click_node) } } }) diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/font_info.scala --- a/src/Tools/jEdit/src/font_info.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/font_info.scala Fri Nov 08 19:18:32 2024 +0100 @@ -31,8 +31,10 @@ def main_size(scale: Double = 1.0): Float = restrict_size(jEdit.getIntegerProperty("view.fontsize", 16).toFloat * scale.toFloat) - def main(scale: Double = 1.0): Font_Info = - Font_Info(main_family(), main_size(scale)) + def main(scale: Double = 1.0, zoom: Zoom = null): Font_Info = + Font_Info(main_family(), main_size(if (zoom == null) scale else scale * zoom.scale)) + + class Zoom extends GUI.Zoom { tooltip = "Zoom factor for output font size" } /* incremental size change */ @@ -76,11 +78,6 @@ change_size(_ => size) } } - - - /* zoom */ - - class Zoom extends GUI.Zoom { tooltip = "Zoom factor for output font size" } } sealed case class Font_Info(family: String, size: Float) { diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -84,13 +84,13 @@ val graphview = new isabelle.graphview.Graphview(graph) { def options: Options = PIDE.options.value - override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = { + override def make_tooltip(parent: JComponent, x: Int, y: Int, tip: XML.Elem): String = { Pretty_Tooltip.invoke(() => { val model = File_Model.init(PIDE.session) val rendering = JEdit_Rendering(snapshot, model, options) - val info = Text.Info(Text.Range.offside, body) - Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info) + val loc = new Point(x, y) + Pretty_Tooltip(view, parent, loc, rendering, Command.Results.empty, List(tip)) }) null } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/info_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -20,12 +20,12 @@ private var implicit_snapshot = Document.Snapshot.init private var implicit_results = Command.Results.empty - private var implicit_info: XML.Body = Nil + private var implicit_info: List[XML.Elem] = Nil private def set_implicit( snapshot: Document.Snapshot, results: Command.Results, - info: XML.Body + info: List[XML.Elem] ): Unit = { GUI_Thread.require {} @@ -41,7 +41,7 @@ view: View, snapshot: Document.Snapshot, results: Command.Results, - info: XML.Body + info: List[XML.Elem] ): Unit = { set_implicit(snapshot, results, info) view.getDockableWindowManager.floatDockableWindow("isabelle-info") @@ -72,10 +72,7 @@ pretty_text_area.update(snapshot, results, info) - private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } - - private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom) } + private def handle_resize(): Unit = pretty_text_area.zoom() /* resize */ @@ -88,8 +85,7 @@ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() }) - private val controls = - Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) + private val controls = Wrap_Panel(pretty_text_area.search_zoom_components) add(controls.peer, BorderLayout.NORTH) diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Fri Nov 08 19:18:32 2024 +0100 @@ -542,7 +542,7 @@ } { val loc = new Point(loc0.x, loc0.y + painter.getLineHeight * 3 / 4) val results = rendering.snapshot.command_results(tip.range) - Pretty_Tooltip(view, painter, loc, rendering, results, tip) + Pretty_Tooltip(view, painter, loc, rendering, results, tip.info) } } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 08 19:18:32 2024 +0100 @@ -46,7 +46,7 @@ val old_content = dummy_window.getContentPane dummy_window.setContentPane(outer) - dummy_window.pack + dummy_window.pack() dummy_window.revalidate() val geometry = @@ -252,17 +252,20 @@ try { val p = text_area.offsetToXY(range.start) val (q, r) = - if (get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n")) + if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) { (text_area.offsetToXY(stop - 1), char_width) - else if (stop >= end) + } + else if (stop >= end) { (text_area.offsetToXY(end), char_width * (stop - end)) + } else (text_area.offsetToXY(stop), 0) (p, q, r) } catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } - if (p != null && q != null && p.x < q.x + r && p.y == q.y) + if (p != null && q != null && p.x < q.x + r && p.y == q.y) { Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) + } else None } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Nov 08 19:18:32 2024 +0100 @@ -25,16 +25,10 @@ def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering = new JEdit_Rendering(snapshot, model, options) - def text( - snapshot: Document.Snapshot, - formatted_body: XML.Body, - results: Command.Results = Command.Results.empty - ): (String, JEdit_Rendering) = { - val command = Command.rich_text(Document_ID.make(), results, formatted_body) - val snippet = snapshot.snippet(command, Document.Blobs.empty) + def apply(snapshot: Document.Snapshot, rich_text: Command): JEdit_Rendering = { + val snippet = snapshot.snippet(rich_text, Document.Blobs.empty) val model = File_Model.init(PIDE.session) - val rendering = apply(snippet, model, PIDE.options.value) - (command.source, rendering) + apply(snippet, model, PIDE.options.value) } @@ -309,10 +303,9 @@ def tooltip_margin: Int = options.int("jedit_tooltip_margin") override def timing_threshold: Double = options.real("jedit_timing_threshold") - def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] = { - val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements - tooltips(elements, range).map(info => info.map(Pretty.fbreaks)) - } + def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[List[XML.Elem]]] = + tooltips(if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements, + range) lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon")) @@ -357,23 +350,16 @@ def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = message_underline_color(JEdit_Rendering.squiggly_elements, range) - def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] = { - val results = - snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ => - { - case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) - }) - val pri = results.foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 } + def line_background(range: Text.Range): Option[Rendering.Color.Value] = + Rendering.message_background_color.get( + snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ => { + case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) + }).foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 }) - Rendering.message_background_color.get(pri).map(message_color => { - val is_separator = - snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ => - { - case _ => Some(true) - }).exists(_.info) - (message_color, is_separator) - }) - } + def line_separator(range: Text.Range): Boolean = + snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ => { + case _ => Some(true) + }).exists(_.info) /* text color */ diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/output_area.scala --- a/src/Tools/jEdit/src/output_area.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/output_area.scala Fri Nov 08 19:18:32 2024 +0100 @@ -13,7 +13,6 @@ import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent, MouseEvent, MouseAdapter} import javax.swing.JComponent -import javax.swing.event.TreeSelectionEvent import scala.swing.{Component, ScrollPane, SplitPane, Orientation} import scala.swing.event.ButtonClicked @@ -21,7 +20,10 @@ import org.gjt.sp.jedit.View -class Output_Area(view: View, root_name: String = "Overview") { +class Output_Area(view: View, + root_name: String = "Overview", + split: Boolean = false +) { GUI_Thread.require {} @@ -30,33 +32,39 @@ val tree: Tree_View = new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true) - def handle_tree_selection(e: TreeSelectionEvent): Unit = () - tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e)) - /* text area */ val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view) - def handle_resize(): Unit = () + def handle_resize(): Unit = pretty_text_area.zoom() def handle_update(): Unit = () lazy val delay_resize: Delay = Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } - /* main pane */ + /* main GUI components */ + + lazy val tree_pane: Component = { + val scroll_pane: ScrollPane = new ScrollPane(Component.wrap(tree)) + scroll_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always + scroll_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always + scroll_pane.minimumSize = new Dimension(200, 100) + scroll_pane + } - val tree_pane: ScrollPane = new ScrollPane(Component.wrap(tree)) - tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always - tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always - tree_pane.minimumSize = new Dimension(200, 100) + lazy val text_pane: Component = Component.wrap(pretty_text_area) - val main_pane: SplitPane = new SplitPane(Orientation.Vertical) { - oneTouchExpandable = true - leftComponent = tree_pane - rightComponent = Component.wrap(pretty_text_area) - } + lazy val main_pane: Component = + if (split) { + new SplitPane(Orientation.Vertical) { + oneTouchExpandable = true + leftComponent = tree_pane + rightComponent = text_pane + } + } + else text_pane /* GUI component */ diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -19,7 +19,7 @@ /* component state -- owned by GUI thread */ private var do_update = true - private var current_output: List[XML.Tree] = Nil + private var current_output: List[XML.Elem] = Nil /* pretty text area */ @@ -30,8 +30,7 @@ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation - private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom) } + private def handle_resize(): Unit = pretty_text_area.zoom() private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = { GUI_Thread.require {} @@ -52,7 +51,7 @@ else current_output if (current_output != new_output) { - pretty_text_area.update(snapshot, results, Pretty.separate(new_output)) + pretty_text_area.update(snapshot, results, new_output) current_output = new_output } } @@ -78,12 +77,10 @@ override def clicked(): Unit = handle_update(true, None) } - private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } - private val controls = Wrap_Panel( - List(output_state_button, auto_hovering_button, auto_update_button, - update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)) + List(output_state_button, auto_hovering_button, auto_update_button, update_button) ::: + pretty_text_area.search_zoom_components) add(controls.peer, BorderLayout.NORTH) diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 08 19:18:32 2024 +0100 @@ -32,20 +32,20 @@ close_action: () => Unit = () => (), propagate_keys: Boolean = false ) extends JEditEmbeddedTextArea { - text_area => + pretty_text_area => GUI_Thread.require {} private var current_font_info: Font_Info = Font_Info.main() - private var current_body: XML.Body = Nil + private var current_output: List[XML.Elem] = Nil private var current_base_snapshot = Document.Snapshot.init private var current_base_results = Command.Results.empty private var current_rendering: JEdit_Rendering = - JEdit_Rendering.text(current_base_snapshot, Nil)._2 + JEdit_Rendering(current_base_snapshot, Command.rich_text()) private var future_refresh: Option[Future[Unit]] = None private val rich_text_area = - new Rich_Text_Area(view, text_area, () => current_rendering, close_action, + new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action, get_search_pattern _, () => (), caret_visible = false, enable_hovering = true) private var current_search_pattern: Option[Regex] = None @@ -88,17 +88,21 @@ if (getWidth > 0) { val metric = JEdit_Lib.font_metric(getPainter) - val margin = ((getPainter.getWidth.toDouble / metric.unit) max 20.0).floor + val margin = metric.pretty_margin((getPainter.getWidth.toDouble / metric.average_width).toInt) val snapshot = current_base_snapshot val results = current_base_results - val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric) + val formatted = + Pretty.formatted(Pretty.separate(current_output), margin = margin, metric = metric) future_refresh.foreach(_.cancel()) future_refresh = Some(Future.fork { val (text, rendering) = - try { JEdit_Rendering.text(snapshot, formatted_body, results = results) } + try { + val rich_text = Command.rich_text(body = formatted, results = results) + (rich_text.source, JEdit_Rendering(snapshot, rich_text)) + } catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } Exn.Interrupt.expose() @@ -115,48 +119,41 @@ } } - def resize(font_info: Font_Info): Unit = { - GUI_Thread.require {} - + def resize(font_info: Font_Info): Unit = GUI_Thread.require { current_font_info = font_info refresh() } - def zoom(zoom: GUI.Zoom): Unit = { - val factor = if (zoom == null) 100 else zoom.factor - resize(Font_Info.main(PIDE.options.real("jedit_font_scale") * factor / 100)) - } - def update( base_snapshot: Document.Snapshot, base_results: Command.Results, - body: XML.Body + output: List[XML.Elem] ): Unit = { GUI_Thread.require {} require(!base_snapshot.is_outdated, "document snapshot outdated") current_base_snapshot = base_snapshot current_base_results = base_results - current_body = body + current_output = output refresh() } def detach(): Unit = { GUI_Thread.require {} - Info_Dockable(view, current_base_snapshot, current_base_results, current_body) + Info_Dockable(view, current_base_snapshot, current_base_results, current_output) } def detach_operation: Option[() => Unit] = - if (current_body.isEmpty) None else Some(() => detach()) + if (current_output.isEmpty) None else Some(() => detach()) - /* common GUI components */ + /* search */ - val search_label: Component = new Label("Search:") { + private val search_label: Component = new Label("Search:") { tooltip = "Search and highlight output via regular expression" } - val search_field: Component = + private val search_field: Component = Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") { private val input_delay = Delay.last(PIDE.session.input_delay, gui = true) { search_action(this) } @@ -182,7 +179,7 @@ } if (current_search_pattern != pattern) { current_search_pattern = pattern - text_area.getPainter.repaint() + pretty_text_area.getPainter.repaint() } text_field.setForeground( if (ok) search_field_foreground @@ -190,14 +187,30 @@ } + /* zoom */ + + val zoom_component: Font_Info.Zoom = + new Font_Info.Zoom { override def changed(): Unit = zoom() } + + def zoom(zoom: Font_Info.Zoom = zoom_component): Unit = + resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale"), zoom = zoom)) + + + /* common GUI components */ + + def search_components: List[Component] = List(search_label, search_field) + + def search_zoom_components: List[Component] = List(search_label, search_field, zoom_component) + + /* key handling */ override def getInputMethodRequests: InputMethodRequests = null inputHandlerProvider = - new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) { + new DefaultInputHandlerProvider(new TextAreaInputHandler(pretty_text_area) { override def getAction(action: String): JEditBeanShellAction = - text_area.getActionContext.getAction(action) + pretty_text_area.getActionContext.getAction(action) override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean): Unit = {} override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false }) @@ -209,13 +222,13 @@ evt.getKeyCode match { case KeyEvent.VK_C | KeyEvent.VK_INSERT - if strict_control && text_area.getSelectionCount != 0 => - Registers.copy(text_area, '$') + if strict_control && pretty_text_area.getSelectionCount != 0 => + Registers.copy(pretty_text_area, '$') evt.consume() case KeyEvent.VK_A if strict_control => - text_area.selectAll + pretty_text_area.selectAll() evt.consume() case KeyEvent.VK_ESCAPE => diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Nov 08 19:18:32 2024 +0100 @@ -28,16 +28,18 @@ private var stack: List[Pretty_Tooltip] = Nil private def hierarchy( - tip: Pretty_Tooltip + pretty_tooltip: Pretty_Tooltip ): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] = { GUI_Thread.require {} - if (stack.contains(tip)) Some(stack.span(_ != tip)) + if (stack.contains(pretty_tooltip)) Some(stack.span(_ != pretty_tooltip)) else None } private def descendant(parent: JComponent): Option[Pretty_Tooltip] = - GUI_Thread.require { stack.find(tip => tip.original_parent == parent) } + GUI_Thread.require { + stack.find(pretty_tooltip => pretty_tooltip.original_parent == parent) + } def apply( view: View, @@ -45,27 +47,28 @@ location: Point, rendering: JEdit_Rendering, results: Command.Results, - info: Text.Info[XML.Body] + output: List[XML.Elem] ): Unit = { GUI_Thread.require {} stack match { - case top :: _ if top.results == results && top.info == info => + case top :: _ if top.results == results && top.output == output => case _ => GUI.layered_pane(parent) match { case None => case Some(layered) => val (old, rest) = GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match { - case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) + case Some(pretty_tooltip) => hierarchy(pretty_tooltip).getOrElse((stack, Nil)) case None => (stack, Nil) } old.foreach(_.hide_popup()) val loc = SwingUtilities.convertPoint(parent, location, layered) - val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info) - stack = tip :: rest - tip.show_popup() + val pretty_tooltip = + new Pretty_Tooltip(view, layered, parent, loc, rendering, results, output) + stack = pretty_tooltip :: rest + pretty_tooltip.show_popup() } } } @@ -117,7 +120,7 @@ Delay.last(PIDE.session.input_delay, gui = true) { dismiss_unfocused() } def dismiss_unfocused(): Unit = { - stack.span(tip => !tip.pretty_text_area.isFocusOwner) match { + stack.span(pretty_tooltip => !pretty_tooltip.pretty_text_area.isFocusOwner) match { case (Nil, _) => case (unfocused, rest) => deactivate() @@ -126,16 +129,16 @@ } } - def dismiss(tip: Pretty_Tooltip): Unit = { + def dismiss(pretty_tooltip: Pretty_Tooltip): Unit = { deactivate() - hierarchy(tip) match { + hierarchy(pretty_tooltip) match { case Some((old, _ :: rest)) => rest match { case top :: _ => top.request_focus() case Nil => JEdit_Lib.request_focus_view() } old.foreach(_.hide_popup()) - tip.hide_popup() + pretty_tooltip.hide_popup() stack = rest case _ => } @@ -164,9 +167,9 @@ location: Point, rendering: JEdit_Rendering, private val results: Command.Results, - private val info: Text.Info[XML.Body] + private val output: List[XML.Elem] ) extends JPanel(new BorderLayout) { - tip => + pretty_tooltip => GUI_Thread.require {} @@ -177,7 +180,7 @@ icon = rendering.tooltip_close_icon tooltip = "Close tooltip window" listenTo(mouse.clicks) - reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) } + reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(pretty_tooltip) } } private val detach = new Label { @@ -186,8 +189,8 @@ listenTo(mouse.clicks) reactions += { case _: MouseClicked => - Info_Dockable(view, rendering.snapshot, results, info.info) - Pretty_Tooltip.dismiss(tip) + Info_Dockable(view, rendering.snapshot, results, output) + Pretty_Tooltip.dismiss(pretty_tooltip) } } @@ -199,7 +202,7 @@ /* text area */ val pretty_text_area: Pretty_Text_Area = - new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) { + new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(pretty_tooltip), true) { override def get_background(): Option[Color] = Some(rendering.tooltip_color) } @@ -220,20 +223,20 @@ /* main content */ def tip_border(has_focus: Boolean): Unit = { - tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY)) - tip.repaint() + pretty_tooltip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY)) + pretty_tooltip.repaint() } tip_border(true) override def getFocusTraversalKeysEnabled = false - tip.setBackground(rendering.tooltip_color) - tip.add(controls.peer, BorderLayout.NORTH) - tip.add(pretty_text_area) + pretty_tooltip.setBackground(rendering.tooltip_color) + pretty_tooltip.add(controls.peer, BorderLayout.NORTH) + pretty_tooltip.add(pretty_text_area) /* popup */ - private val popup = { + private val popup: Popup = { val screen = GUI.screen_location(layered, location) val size = { val bounds = JEdit_Rendering.popup_bounds @@ -242,14 +245,13 @@ val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt val painter = pretty_text_area.getPainter - val geometry = JEdit_Lib.window_geometry(tip, painter) + val geometry = JEdit_Lib.window_geometry(pretty_tooltip, painter) val metric = JEdit_Lib.font_metric(painter) - val margin = - ((rendering.tooltip_margin * metric.average) min - ((w_max - geometry.deco_width) / metric.unit).toInt) max 20 + metric.pretty_margin(rendering.tooltip_margin, + limit = ((w_max - geometry.deco_width) / metric.average_width).toInt) - val formatted = Pretty.formatted(info.info, margin = margin, metric = metric) + val formatted = Pretty.formatted(Pretty.separate(output), margin = margin, metric = metric) val lines = XML.content_lines(formatted) val h = painter.getLineHeight * lines + geometry.deco_height @@ -257,18 +259,18 @@ if (h <= h_max) { split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) } } - else margin - val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width + else margin.toDouble + val w = (metric.unit * (margin1 + 1)).round.toInt + geometry.deco_width new Dimension(w min w_max, h min h_max) } - new Popup(layered, tip, screen.relative(layered, size), size) + new Popup(layered, pretty_tooltip, screen.relative(layered, size), size) } private def show_popup(): Unit = { popup.show pretty_text_area.requestFocus() - pretty_text_area.update(rendering.snapshot, results, info.info) + pretty_text_area.update(rendering.snapshot, results, output) } private def hide_popup(): Unit = popup.hide diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/query_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -77,9 +77,7 @@ val query_operation = new Query_Operation(PIDE.editor, view, "find_theorems", - consume_status(process_indicator, _), - (snapshot, results, body) => - pretty_text_area.update(snapshot, results, Pretty.separate(body))) + consume_status(process_indicator, _), pretty_text_area.update) private def apply_query(): Unit = { query.addCurrentToHistory() @@ -118,8 +116,8 @@ private val control_panel = Wrap_Panel( List(query_label, Component.wrap(query), limit, allow_dups, - process_indicator.component, apply_button, - pretty_text_area.search_label, pretty_text_area.search_field)) + process_indicator.component, apply_button) ::: + pretty_text_area.search_components) def select(): Unit = { control_panel.contents += zoom } @@ -140,9 +138,7 @@ val query_operation = new Query_Operation(PIDE.editor, view, "find_consts", - consume_status(process_indicator, _), - (snapshot, results, body) => - pretty_text_area.update(snapshot, results, Pretty.separate(body))) + consume_status(process_indicator, _), pretty_text_area.update) private val query_label = new Label("Find:") { tooltip = GUI.tooltip_lines("Name / type patterns for constants") @@ -166,9 +162,8 @@ private val control_panel = Wrap_Panel( - List( - query_label, Component.wrap(query), process_indicator.component, apply_button, - pretty_text_area.search_label, pretty_text_area.search_field)) + List(query_label, Component.wrap(query), process_indicator.component, apply_button) ::: + pretty_text_area.search_components) def select(): Unit = { control_panel.contents += zoom } @@ -218,9 +213,7 @@ val query_operation = new Query_Operation(PIDE.editor, view, "print_operation", - consume_status(process_indicator, _), - (snapshot, results, body) => - pretty_text_area.update(snapshot, results, Pretty.separate(body))) + consume_status(process_indicator, _), pretty_text_area.update) private def apply_query(): Unit = query_operation.apply_query(selected_items()) @@ -252,8 +245,8 @@ control_panel.contents += query_label update_items().foreach(item => control_panel.contents += item.gui) control_panel.contents ++= - List(process_indicator.component, apply_button, - pretty_text_area.search_label, pretty_text_area.search_field, zoom) + List(process_indicator.component, apply_button) ::: + pretty_text_area.search_components ::: List(zoom) } val page = @@ -301,7 +294,7 @@ private def handle_resize(): Unit = GUI_Thread.require { - if (operations != null) operations.foreach(_.pretty_text_area.zoom(zoom)) + if (operations != null) operations.foreach(_.pretty_text_area.zoom(zoom = zoom)) } private val delay_resize = diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 08 19:18:32 2024 +0100 @@ -299,7 +299,7 @@ val painter = text_area.getPainter val loc = new Point(x, y + painter.getLineHeight / 2) val results = snapshot.command_results(tip.range) - Pretty_Tooltip(view, painter, loc, rendering, results, tip) + Pretty_Tooltip(view, painter, loc, rendering, results, tip.info) } } } @@ -332,9 +332,10 @@ val line_range = Text.Range(start(i), end(i) min buffer.getLength) // line background color - for { (c, separator) <- rendering.line_background(line_range) } { + for (c <- rendering.line_background(line_range)) { + val separator = rendering.line_separator(line_range) + val sep = if (separator) (2 min (line_height / 2)) max (line_height / 8) else 0 gfx.setColor(rendering.color(c)) - val sep = if (separator) (2 min (line_height / 2)) max (line_height / 8) else 0 gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep) } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -30,8 +30,8 @@ private var do_update = true - private val text_area = new Pretty_Text_Area(view) - set_content(text_area) + private val pretty_text_area = new Pretty_Text_Area(view) + set_content(pretty_text_area) private def update_contents(): Unit = { val snapshot = current_snapshot @@ -41,8 +41,8 @@ context.questions.values.toList match { case q :: _ => val data = q.data - val content = Pretty.separate(XML.Text(data.text) :: data.content) - text_area.update(snapshot, Command.Results.empty, content) + val output = List(Pretty.block(XML.Text(data.text) :: data.content, indent = 0)) + pretty_text_area.update(snapshot, Command.Results.empty, output) q.answers.foreach { answer => answers.contents += new GUI.Button(answer.string) { override def clicked(): Unit = @@ -50,10 +50,10 @@ } } case Nil => - text_area.update(snapshot, Command.Results.empty, Nil) + pretty_text_area.update(snapshot, Command.Results.empty, Nil) } - do_paint() + handle_resize() } private def show_trace(): Unit = { @@ -61,13 +61,7 @@ new Simplifier_Trace_Window(view, current_snapshot, trace) } - private def do_paint(): Unit = { - GUI_Thread.later { - text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale"))) - } - } - - private def handle_resize(): Unit = do_paint() + private def handle_resize(): Unit = pretty_text_area.zoom() private def handle_update(follow: Boolean): Unit = { val (new_snapshot, new_command, new_results, new_id) = diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/simplifier_trace_window.scala --- a/src/Tools/jEdit/src/simplifier_trace_window.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Fri Nov 08 19:18:32 2024 +0100 @@ -41,9 +41,6 @@ val parent = None val interesting = true val markup = "" - - def format: XML.Body = - Pretty.separate(tree_children.flatMap(_.format)) } final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree]) @@ -59,7 +56,7 @@ private def body_contains(regex: Regex, body: XML.Body): Boolean = body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined) - def format: Option[XML.Tree] = { + def format: Option[XML.Elem] = { def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree = Pretty.block(Pretty.separate(XML.Text(data.text) :: data.content)) @@ -133,7 +130,6 @@ GUI_Thread.require {} private val pretty_text_area = new Pretty_Text_Area(view) - private val zoom = new Font_Info.Zoom { override def changed(): Unit = do_paint() } size = new Dimension(500, 500) contents = new BorderPanel { @@ -149,19 +145,16 @@ new Simplifier_Trace_Window.Root_Tree(0) } - do_update() + handle_update() open() - do_paint() + handle_resize() - def do_update(): Unit = { - val xml = tree.format - pretty_text_area.update(snapshot, Command.Results.empty, xml) + def handle_update(): Unit = { + val output = tree.tree_children.flatMap(_.format) + pretty_text_area.update(snapshot, Command.Results.empty, output) } - def do_paint(): Unit = - GUI_Thread.later { pretty_text_area.zoom(zoom) } - - def handle_resize(): Unit = do_paint() + def handle_resize(): Unit = pretty_text_area.zoom() /* resize */ @@ -177,8 +170,7 @@ /* controls */ - private val controls = - Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) + private val controls = Wrap_Panel(pretty_text_area.search_zoom_components) peer.add(controls.peer, BorderLayout.NORTH) } diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -46,9 +46,7 @@ } private val sledgehammer = - new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status, - (snapshot, results, body) => - pretty_text_area.update(snapshot, results, Pretty.separate(body))) + new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status, pretty_text_area.update) /* resize */ @@ -61,8 +59,7 @@ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() }) - private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom) } + private def handle_resize(): Unit = pretty_text_area.zoom() /* controls */ @@ -122,12 +119,11 @@ override def clicked(): Unit = sledgehammer.locate_query() } - private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } - private val controls = Wrap_Panel( List(provers_label, Component.wrap(provers), isar_proofs, try0, - process_indicator.component, apply_query, cancel_query, locate_query, zoom)) + process_indicator.component, apply_query, cancel_query, locate_query, + pretty_text_area.zoom_component)) add(controls.peer, BorderLayout.NORTH) diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -27,9 +27,7 @@ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation private val print_state = - new Query_Operation(PIDE.editor, view, "print_state", _ => (), - (snapshot, results, body) => - pretty_text_area.update(snapshot, results, Pretty.separate(body))) + new Query_Operation(PIDE.editor, view, "print_state", _ => (), pretty_text_area.update) /* resize */ @@ -42,8 +40,7 @@ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() }) - private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom) } + private def handle_resize(): Unit = pretty_text_area.zoom() /* update */ @@ -93,12 +90,10 @@ override def clicked(): Unit = print_state.locate_query() } - private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } - private val controls = Wrap_Panel( - List(auto_update_button, update_button, - locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)) + List(auto_update_button, update_button, locate_button) ::: + pretty_text_area.search_zoom_components) add(controls.peer, BorderLayout.NORTH) diff -r 5ad7c7f825d2 -r 37cff2ad31da src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Fri Nov 08 11:18:08 2024 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Nov 08 19:18:32 2024 +0100 @@ -18,7 +18,7 @@ class Symbols_Dockable(view: View, position: String) extends Dockable(view, position) { private def font_size: Int = - Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round + Font_Info.main_size(scale = PIDE.options.real("jedit_font_scale")).round /* abbrevs */