--- a/src/Pure/GUI/font_metric.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/GUI/font_metric.scala Fri Nov 08 22:52:29 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
+ }
}
--- a/src/Pure/GUI/gui.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/GUI/gui.scala Fri Nov 08 22:52:29 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
--- a/src/Pure/General/pretty.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/General/pretty.scala Fri Nov 08 22:52:29 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 */
--- a/src/Pure/General/symbol.ML Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/General/symbol.ML Fri Nov 08 22:52:29 2024 +0100
@@ -498,22 +498,22 @@
(** symbol output **)
-(* length *)
+(* metric *)
-fun sym_len s =
+fun metric1 s =
if String.isPrefix "\092<longlonglong" s then 4
else if String.isPrefix "\092<longlong" s then 3
else if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
- else if is_printable s then 1
+ else if is_blank s orelse is_printable s then 1
else 0;
-fun sym_length ss = fold (fn s => 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;
--- a/src/Pure/General/symbol.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/General/symbol.scala Fri Nov 08 22:52:29 2024 +0100
@@ -676,7 +676,7 @@
if (sym.startsWith("\\<longlonglong")) 4
else if (sym.startsWith("\\<longlong")) 3
else if (sym.startsWith("\\<long") || sym.startsWith("\\<Long")) 2
- else if (is_printable(sym)) 1
+ else if (is_blank(sym) || is_printable(sym)) 1
else 0
}).sum
}
--- a/src/Pure/PIDE/command.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/PIDE/command.scala Fri Nov 08 22:52:29 2024 +0100
@@ -386,10 +386,8 @@
new Command(id, node_name, blobs_info, span1, source1, results, markups)
}
- def text(source: String): Command = unparsed(source)
-
- def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
- unparsed(XML.content(body), id = id, results = results,
+ def rich_text(body: XML.Body = Nil, results: Results = Results.empty): Command =
+ unparsed(XML.content(body), id = Document_ID.make(), results = results,
markups = Markups.init(Markup_Tree.from_XML(body)))
--- a/src/Pure/PIDE/query_operation.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/PIDE/query_operation.scala Fri Nov 08 22:52:29 2024 +0100
@@ -36,7 +36,7 @@
editor_context: Editor_Context,
operation_name: String,
consume_status: Query_Operation.Status => 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"
--- a/src/Pure/PIDE/rendering.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala Fri Nov 08 22:52:29 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
--- a/src/Pure/System/program_progress.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/System/program_progress.scala Fri Nov 08 22:52:29 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 {
--- a/src/Pure/Thy/thy_syntax.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Fri Nov 08 22:52:29 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) =>
--- a/src/Pure/Tools/debugger.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Pure/Tools/debugger.scala Fri Nov 08 22:52:29 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)
}
--- a/src/Tools/Graphview/graph_panel.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Fri Nov 08 22:52:29 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() }
--- a/src/Tools/Graphview/graphview.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/Graphview/graphview.scala Fri Nov 08 22:52:29 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 */
--- a/src/Tools/VSCode/src/pretty_text_panel.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala Fri Nov 08 22:52:29 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))))
}
}
}
--- a/src/Tools/VSCode/src/state_panel.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala Fri Nov 08 22:52:29 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()
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Nov 08 22:52:29 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
--- a/src/Tools/jEdit/src/debugger_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Nov 08 22:52:29 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 */
--- a/src/Tools/jEdit/src/document_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Fri Nov 08 22:52:29 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 {
--- a/src/Tools/jEdit/src/documentation_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Fri Nov 08 22:52:29 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)
}
}
})
--- a/src/Tools/jEdit/src/font_info.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/font_info.scala Fri Nov 08 22:52:29 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) {
--- a/src/Tools/jEdit/src/graphview_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Fri Nov 08 22:52:29 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
}
--- a/src/Tools/jEdit/src/info_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Fri Nov 08 22:52:29 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)
--- a/src/Tools/jEdit/src/isabelle.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Nov 08 22:52:29 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)
}
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 08 22:52:29 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
}
--- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Nov 08 22:52:29 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 */
--- a/src/Tools/jEdit/src/output_area.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala Fri Nov 08 22:52:29 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 */
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Nov 08 22:52:29 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)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 08 22:52:29 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 =>
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Fri Nov 08 22:52:29 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
--- a/src/Tools/jEdit/src/query_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Fri Nov 08 22:52:29 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 =
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 08 22:52:29 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)
}
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Fri Nov 08 22:52:29 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) =
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Fri Nov 08 22:52:29 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)
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Nov 08 22:52:29 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)
--- a/src/Tools/jEdit/src/state_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Fri Nov 08 22:52:29 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)
--- a/src/Tools/jEdit/src/symbols_dockable.scala Fri Nov 08 18:13:55 2024 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Nov 08 22:52:29 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 */