--- a/src/Pure/GUI/gui.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Pure/GUI/gui.scala Sun Aug 14 11:11:11 2022 +0100
@@ -13,8 +13,8 @@
import java.awt.geom.AffineTransform
import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
-import scala.swing.{ComboBox, ScrollPane, TextArea}
-import scala.swing.event.SelectionChanged
+import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea}
+import scala.swing.event.{ButtonClicked, SelectionChanged}
object GUI {
@@ -111,14 +111,37 @@
}
- /* zoom box */
+ /* basic GUI components */
+
+ class Button(label: String) extends scala.swing.Button(label) {
+ def clicked(): Unit = {}
+
+ reactions += { case ButtonClicked(_) => clicked() }
+ }
+
+ class Check(label: String, init: Boolean = false) extends CheckBox(label) {
+ def clicked(state: Boolean): Unit = {}
+ def clicked(): Unit = {}
+
+ selected = init
+ reactions += { case ButtonClicked(_) => clicked(selected); clicked() }
+ }
+
+ class Selector[A](val entries: List[A]) extends ComboBox[A](entries) {
+ def changed(): Unit = {}
+
+ listenTo(selection)
+ reactions += { case SelectionChanged(_) => changed() }
+ }
+
+
+ /* zoom factor */
private val Zoom_Factor = "([0-9]+)%?".r
- abstract class Zoom_Box extends ComboBox[String](
+ class Zoom extends Selector[String](
List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
) {
- def changed(): Unit
def factor: Int = parse(selection.item)
private def parse(text: String): Int =
@@ -145,9 +168,6 @@
}
selection.index = 3
-
- listenTo(selection)
- reactions += { case SelectionChanged(_) => changed() }
}
--- a/src/Pure/PIDE/rendering.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Pure/PIDE/rendering.scala Sun Aug 14 11:11:11 2022 +0100
@@ -95,11 +95,11 @@
legacy_pri -> Color.legacy_message,
error_pri -> Color.error_message)
- def output_messages(results: Command.Results): List[XML.Elem] = {
+ def output_messages(results: Command.Results, output_state: Boolean): List[XML.Elem] = {
val (states, other) =
results.iterator.map(_._2).filterNot(Protocol.is_result).toList
.partition(Protocol.is_state)
- states ::: other
+ (if (output_state) states else Nil) ::: other
}
--- a/src/Pure/System/components.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Pure/System/components.scala Sun Aug 14 11:11:11 2022 +0100
@@ -318,7 +318,7 @@
var options = Options.init()
def show_options: String =
- cat_lines(relevant_options.map(name => options.options(name).print))
+ cat_lines(relevant_options.flatMap(options.get).map(_.print))
val getopts = Getopts("""
Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS...
--- a/src/Pure/System/options.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Pure/System/options.scala Sun Aug 14 11:11:11 2022 +0100
@@ -13,6 +13,25 @@
val empty: Options = new Options()
+ /* typed access */
+
+ abstract class Access[A](val options: Options) {
+ def apply(name: String): A
+ def update(name: String, x: A): Options
+ def change(name: String, f: A => A): Options = update(name, f(apply(name)))
+ }
+
+ class Access_Variable[A](
+ val options: Options_Variable,
+ val pure_access: Options => Access[A]
+ ) {
+ def apply(name: String): A = pure_access(options.value)(name)
+ def update(name: String, x: A): Unit =
+ options.change(options => pure_access(options).update(name, x))
+ def change(name: String, f: A => A): Unit = update(name, f(apply(name)))
+ }
+
+
/* representation */
sealed abstract class Type {
@@ -200,23 +219,27 @@
final class Options private(
- val options: Map[String, Options.Opt] = Map.empty,
+ options: Map[String, Options.Opt] = Map.empty,
val section: String = ""
) {
- override def toString: String = options.iterator.mkString("Options(", ",", ")")
+ def opt_iterator: Iterator[(String, Options.Opt)] = options.iterator
+
+ override def toString: String = opt_iterator.mkString("Options(", ",", ")")
private def print_opt(opt: Options.Opt): String =
if (opt.public) "public " + opt.print else opt.print
- def print: String = cat_lines(options.toList.sortBy(_._1).map(p => print_opt(p._2)))
+ def print: String = cat_lines(opt_iterator.toList.sortBy(_._1).map(p => print_opt(p._2)))
def description(name: String): String = check_name(name).description
/* check */
+ def get(name: String): Option[Options.Opt] = options.get(name)
+
def check_name(name: String): Options.Opt =
- options.get(name) match {
+ get(name) match {
case Some(opt) if !opt.unknown => opt
case _ => error("Unknown option " + quote(name))
}
@@ -230,7 +253,7 @@
/* basic operations */
- private def put[A](name: String, typ: Options.Type, value: String): Options = {
+ private def put(name: String, typ: Options.Type, value: String): Options = {
val opt = check_type(name, typ)
new Options(options + (name -> opt.copy(value = value)), section)
}
@@ -248,32 +271,29 @@
/* internal lookup and update */
- class Bool_Access {
- def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply)
- def update(name: String, x: Boolean): Options =
- put(name, Options.Bool, Value.Boolean(x))
- }
- val bool = new Bool_Access
+ val bool: Options.Access[Boolean] =
+ new Options.Access[Boolean](this) {
+ def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply)
+ def update(name: String, x: Boolean): Options = put(name, Options.Bool, Value.Boolean(x))
+ }
+
+ val int: Options.Access[Int] =
+ new Options.Access[Int](this) {
+ def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply)
+ def update(name: String, x: Int): Options = put(name, Options.Int, Value.Int(x))
+ }
- class Int_Access {
- def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply)
- def update(name: String, x: Int): Options =
- put(name, Options.Int, Value.Int(x))
- }
- val int = new Int_Access
+ val real: Options.Access[Double] =
+ new Options.Access[Double](this) {
+ def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply)
+ def update(name: String, x: Double): Options = put(name, Options.Real, Value.Double(x))
+ }
- class Real_Access {
- def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply)
- def update(name: String, x: Double): Options =
- put(name, Options.Real, Value.Double(x))
- }
- val real = new Real_Access
-
- class String_Access {
- def apply(name: String): String = get(name, Options.String, s => Some(s))
- def update(name: String, x: String): Options = put(name, Options.String, x)
- }
- val string = new String_Access
+ val string: Options.Access[String] =
+ new Options.Access[String](this) {
+ def apply(name: String): String = get(name, Options.String, Some(_))
+ def update(name: String, x: String): Options = put(name, Options.String, x)
+ }
def proper_string(name: String): Option[String] =
Library.proper_string(string(name))
@@ -303,7 +323,7 @@
standard: Option[Option[String]],
description: String
): Options = {
- options.get(name) match {
+ get(name) match {
case Some(other) =>
error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
Position.here(other.pos))
@@ -392,7 +412,7 @@
val changed =
(for {
(name, opt2) <- options.iterator
- opt1 = defaults.options.get(name)
+ opt1 = defaults.get(name)
if opt1.isEmpty || opt1.get.value != opt2.value
} yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else "")).toList
@@ -407,36 +427,23 @@
class Options_Variable(init_options: Options) {
- private var options = init_options
-
- def value: Options = synchronized { options }
+ private var _options = init_options
- private def upd(f: Options => Options): Unit = synchronized { options = f(options) }
- def += (name: String, x: String): Unit = upd(opts => opts + (name, x))
+ def value: Options = synchronized { _options }
+ def change(f: Options => Options): Unit = synchronized { _options = f(_options) }
+ def += (name: String, x: String): Unit = change(options => options + (name, x))
- class Bool_Access {
- def apply(name: String): Boolean = value.bool(name)
- def update(name: String, x: Boolean): Unit = upd(opts => opts.bool.update(name, x))
- }
- val bool = new Bool_Access
+ val bool: Options.Access_Variable[Boolean] =
+ new Options.Access_Variable[Boolean](this, _.bool)
- class Int_Access {
- def apply(name: String): Int = value.int(name)
- def update(name: String, x: Int): Unit = upd(opts => opts.int.update(name, x))
- }
- val int = new Int_Access
+ val int: Options.Access_Variable[Int] =
+ new Options.Access_Variable[Int](this, _.int)
- class Real_Access {
- def apply(name: String): Double = value.real(name)
- def update(name: String, x: Double): Unit = upd(opts => opts.real.update(name, x))
- }
- val real = new Real_Access
+ val real: Options.Access_Variable[Double] =
+ new Options.Access_Variable[Double](this, _.real)
- class String_Access {
- def apply(name: String): String = value.string(name)
- def update(name: String, x: String): Unit = upd(opts => opts.string.update(name, x))
- }
- val string = new String_Access
+ val string: Options.Access_Variable[String] =
+ new Options.Access_Variable[String](this, _.string)
def proper_string(name: String): Option[String] =
Library.proper_string(string(name))
--- a/src/Tools/Graphview/graph_panel.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Sun Aug 14 11:11:11 2022 +0100
@@ -298,7 +298,7 @@
tooltip = "Save current graph layout as PNG or PDF"
}
- private val zoom = new GUI.Zoom_Box { def changed(): Unit = rescale(0.01 * factor) }
+ private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(0.01 * factor) }
private val fit_window = new Button {
action = Action("Fit to window") { fit_to_window() }
--- a/src/Tools/Graphview/tree_panel.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Sun Aug 14 11:11:11 2022 +0100
@@ -16,7 +16,7 @@
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
import scala.util.matching.Regex
-import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, CheckBox, Action}
+import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, Action}
class Tree_Panel(val graphview: Graphview, graph_panel: Graph_Panel)
--- a/src/Tools/VSCode/src/dynamic_output.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala Sun Aug 14 11:11:11 2022 +0100
@@ -27,9 +27,10 @@
case None => copy(output = Nil)
case Some(command) =>
copy(output =
- if (restriction.isEmpty || restriction.get.contains(command))
- Rendering.output_messages(snapshot.command_results(command))
- else output)
+ if (restriction.isEmpty || restriction.get.contains(command)) {
+ val output_state = resources.options.bool("editor_output_state")
+ Rendering.output_messages(snapshot.command_results(command), output_state)
+ } else output)
}
}
else this
--- a/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -17,8 +17,7 @@
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
import scala.collection.immutable.SortedMap
-import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation,
- CheckBox, BorderPanel}
+import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation, BorderPanel}
import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.{jEdit, View}
@@ -73,7 +72,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.factor) }
+ GUI_Thread.require { pretty_text_area.zoom(zoom) }
private def handle_update(): Unit = {
GUI_Thread.require {}
@@ -183,30 +182,29 @@
/* controls */
- private val break_button = new CheckBox("Break") {
+ private val break_button = new GUI.Check("Break", init = debugger.is_break()) {
tooltip = "Break running threads at next possible breakpoint"
- selected = debugger.is_break()
- reactions += { case ButtonClicked(_) => debugger.set_break(selected) }
+ override def clicked(state: Boolean): Unit = debugger.set_break(state)
}
- private val continue_button = new Button("Continue") {
+ private val continue_button = new GUI.Button("Continue") {
tooltip = "Continue program on current thread, until next breakpoint"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.continue) }
+ override def clicked(): Unit = thread_selection().map(debugger.continue)
}
- private val step_button = new Button("Step") {
+ private val step_button = new GUI.Button("Step") {
tooltip = "Single-step in depth-first order"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step) }
+ override def clicked(): Unit = thread_selection().map(debugger.step)
}
- private val step_over_button = new Button("Step over") {
+ private val step_over_button = new GUI.Button("Step over") {
tooltip = "Single-step within this function"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_over) }
+ override def clicked(): Unit = thread_selection().map(debugger.step_over)
}
- private val step_out_button = new Button("Step out") {
+ private val step_out_button = new GUI.Button("Step out") {
tooltip = "Single-step outside this function"
- reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_out) }
+ override def clicked(): Unit = thread_selection().map(debugger.step_out)
}
private val context_label = new Label("Context:") {
@@ -242,9 +240,10 @@
setFont(GUI.imitate_font(getFont, scale = 1.2))
}
- private val eval_button = new Button("<html><b>Eval</b></html>") {
+ private val eval_button =
+ new GUI.Button("<html><b>Eval</b></html>") {
tooltip = "Evaluate ML expression within optional context"
- reactions += { case ButtonClicked(_) => eval_expression() }
+ override def clicked(): Unit = eval_expression()
}
private def eval_expression(): Unit = {
@@ -257,12 +256,11 @@
}
}
- private val sml_button = new CheckBox("SML") {
+ private val sml_button = new GUI.Check("SML") {
tooltip = "Official Standard ML instead of Isabelle/ML"
- selected = false
}
- private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+ private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
--- a/src/Tools/jEdit/src/document_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -12,9 +12,6 @@
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
-import scala.swing.{ComboBox, Button}
-import scala.swing.event.{SelectionChanged, ButtonClicked}
-
import org.gjt.sp.jedit.{jEdit, View}
@@ -46,29 +43,27 @@
})
private def handle_resize(): Unit =
- GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
+ GUI_Thread.require { pretty_text_area.zoom(zoom) }
/* controls */
- private val document_session: ComboBox[String] = {
- new ComboBox(JEdit_Sessions.sessions_structure().build_topological_order.sorted) {
+ private val document_session =
+ new GUI.Selector(JEdit_Sessions.sessions_structure().build_topological_order.sorted) {
val title = "Session"
- listenTo(selection)
- reactions += { case SelectionChanged(_) => } // FIXME
}
- }
- private val build_button = new Button("<html><b>Build</b></html>") {
+ private val build_button =
+ new GUI.Button("<html><b>Build</b></html>") {
tooltip = "Build document"
- reactions += { case ButtonClicked(_) =>
+ override def clicked(): Unit = {
pretty_text_area.update(
Document.Snapshot.init, Command.Results.empty,
List(XML.Text(Date.now().toString))) // FIXME
}
}
- private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+ private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(List(document_session, process_indicator.component, build_button,
--- a/src/Tools/jEdit/src/document_model.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Aug 14 11:11:11 2022 +0100
@@ -342,7 +342,7 @@
): (Boolean, Document.Node.Perspective_Text) = {
GUI_Thread.require {}
- if (Isabelle.continuous_checking && is_theory) {
+ if (JEdit_Options.continuous_checking() && is_theory) {
val snapshot = this.snapshot()
val reparse = snapshot.node.load_commands_changed(doc_blobs)
--- a/src/Tools/jEdit/src/font_info.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/font_info.scala Sun Aug 14 11:11:11 2022 +0100
@@ -78,9 +78,9 @@
}
- /* zoom box */
+ /* zoom */
- abstract class Zoom_Box extends GUI.Zoom_Box { tooltip = "Zoom factor for output font size" }
+ 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/info_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -72,10 +72,10 @@
pretty_text_area.update(snapshot, results, info)
- private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+ 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.factor) }
+ GUI_Thread.require { pretty_text_area.zoom(zoom) }
/* resize */
--- a/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sun Aug 14 11:11:11 2022 +0100
@@ -11,9 +11,6 @@
import java.awt.{Point, Frame, Rectangle}
-import scala.swing.CheckBox
-import scala.swing.event.ButtonClicked
-
import org.gjt.sp.jedit.{jEdit, View, Buffer, EditBus}
import org.gjt.sp.jedit.msg.ViewUpdate
import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -27,7 +24,7 @@
object Isabelle {
/* editor modes */
- val modes =
+ val modes: List[String] =
List(
"isabelle", // theory source
"isabelle-ml", // ML source
@@ -195,28 +192,9 @@
/* continuous checking */
- private val CONTINUOUS_CHECKING = "editor_continuous_checking"
-
- def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
- def continuous_checking_=(b: Boolean): Unit =
- GUI_Thread.require {
- if (continuous_checking != b) {
- PIDE.options.bool(CONTINUOUS_CHECKING) = b
- PIDE.session.update_options(PIDE.options.value)
- PIDE.plugin.deps_changed()
- }
- }
-
- def set_continuous_checking(): Unit = { continuous_checking = true }
- def reset_continuous_checking(): Unit = { continuous_checking = false }
- def toggle_continuous_checking(): Unit = { continuous_checking = !continuous_checking }
-
- class Continuous_Checking extends CheckBox("Continuous checking") {
- tooltip = "Continuous checking of proof document (visible and required parts)"
- reactions += { case ButtonClicked(_) => continuous_checking = selected }
- def load(): Unit = { selected = continuous_checking }
- load()
- }
+ def set_continuous_checking(): Unit = JEdit_Options.continuous_checking.set()
+ def reset_continuous_checking(): Unit = JEdit_Options.continuous_checking.reset()
+ def toggle_continuous_checking(): Unit = JEdit_Options.continuous_checking.toggle()
/* update state */
@@ -300,7 +278,7 @@
val line = text_area.getCaretLine
val caret = text_area.getCaretPosition
- def nl: Unit = text_area.userInput('\n')
+ def nl(): Unit = text_area.userInput('\n')
if (indent_enabled(buffer, "jedit_indent_newline")) {
buffer_syntax(buffer) match {
@@ -316,11 +294,11 @@
text_area.setSelectedText("\n")
if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
}
- else nl
- case None => nl
+ else nl()
+ case None => nl()
}
}
- else nl
+ else nl()
}
}
@@ -330,7 +308,7 @@
val text1 =
if (text_area.getSelectionCount == 0) {
def pad(range: Text.Range): String =
- if (JEdit_Lib.get_text(buffer, range) == Some("\n")) "" else "\n"
+ if (JEdit_Lib.get_text(buffer, range).contains("\n")) "" else "\n"
val caret = JEdit_Lib.caret_range(text_area)
val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
--- a/src/Tools/jEdit/src/isabelle_options.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Sun Aug 14 11:11:11 2022 +0100
@@ -43,19 +43,18 @@
protected val components =
options.make_components(predefined,
- (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
+ (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
}
class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") {
private val predefined =
(for {
- (name, opt) <- PIDE.options.value.options.toList
+ (name, opt) <- PIDE.options.value.opt_iterator
if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
- } yield PIDE.options.make_color_component(opt))
+ } yield PIDE.options.make_color_component(opt)).toList
assert(predefined.nonEmpty)
protected val components = PIDE.options.make_components(predefined, _ => false)
}
-
--- a/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala Sun Aug 14 11:11:11 2022 +0100
@@ -14,7 +14,6 @@
import javax.swing.text.JTextComponent
import scala.swing.{Component, CheckBox, TextArea}
-import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.gui.ColorWellButton
@@ -26,23 +25,61 @@
}
object JEdit_Options {
+ /* sections */
+
val RENDERING_SECTION = "Rendering of Document Content"
- class Check_Box(name: String, label: String, description: String) extends CheckBox(label) {
- tooltip = description
- reactions += { case ButtonClicked(_) => update(selected) }
+
+ /* typed access and GUI components */
+
+ class Access[A](access: Options.Access_Variable[A], val name: String) {
+ def apply(): A = access.apply(name)
+ def update(x: A): Unit = change(_ => x)
+ def change(f: A => A): Unit = {
+ val x0 = apply()
+ access.change(name, f)
+ val x1 = apply()
+ if (x0 != x1) changed()
+ }
+ def changed(): Unit = GUI_Thread.require { PIDE.session.update_options(access.options.value) }
+ }
+
+ class Bool_Access(name: String) extends Access(PIDE.options.bool, name) {
+ def set(): Unit = update(true)
+ def reset(): Unit = update(false)
+ def toggle(): Unit = change(b => !b)
+ }
- def stored: Boolean = PIDE.options.bool(name)
- def update(b: Boolean): Unit =
- GUI_Thread.require {
- if (selected != b) selected = b
- if (stored != b) {
- PIDE.options.bool(name) = b
- PIDE.session.update_options(PIDE.options.value)
- }
- }
- def load(): Unit = { selected = stored }
- load()
+ class Bool_GUI(access: Bool_Access, label: String)
+ extends GUI.Check(label, init = access()) {
+ def load(): Unit = { selected = access() }
+ override def clicked(state: Boolean): Unit = access.update(state)
+ }
+
+
+ /* specific options */
+
+ object continuous_checking extends Bool_Access("editor_continuous_checking") {
+ override def changed(): Unit = {
+ super.changed()
+ PIDE.plugin.deps_changed()
+ }
+
+ class GUI extends Bool_GUI(this, "Continuous checking") {
+ tooltip = "Continuous checking of proof document (visible and required parts)"
+ }
+ }
+
+ object output_state extends Bool_Access("editor_output_state") {
+ override def changed(): Unit = GUI_Thread.require {
+ super.changed()
+ PIDE.editor.flush_edits(hidden = true)
+ PIDE.editor.flush()
+ }
+
+ class GUI extends Bool_GUI(this, "Proof state") {
+ tooltip = "Output of proof state (normally shown on State panel)"
+ }
}
}
--- a/src/Tools/jEdit/src/jedit_sessions.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Sun Aug 14 11:11:11 2022 +0100
@@ -10,9 +10,6 @@
import isabelle._
-import scala.swing.ComboBox
-import scala.swing.event.SelectionChanged
-
object JEdit_Sessions {
/* session options */
@@ -88,9 +85,7 @@
(main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name))
}
- val entries = default_entry :: session_entries
-
- new ComboBox(entries) with Option_Component {
+ new GUI.Selector[Logic_Entry](default_entry :: session_entries) with Option_Component {
name = jedit_logic_option
tooltip = "Logic session name (change requires restart)"
val title = "Logic"
@@ -102,12 +97,9 @@
}
}
def save(): Unit = options.string(jedit_logic_option) = selection.item.name
+ override def changed(): Unit = if (autosave) save()
load()
- if (autosave) {
- listenTo(selection)
- reactions += { case SelectionChanged(_) => save() }
- }
}
}
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Sun Aug 14 11:11:11 2022 +0100
@@ -10,7 +10,6 @@
import isabelle._
import javax.swing.JMenuItem
-import scala.swing.ComboBox
import org.gjt.sp.jedit.menu.EnhancedMenuItem
import org.gjt.sp.jedit.jEdit
@@ -86,9 +85,9 @@
val option_name = "spell_checker_dictionary"
val opt = PIDE.options.value.check_name(option_name)
- val entries = Spell_Checker.dictionaries
- val component = new ComboBox(entries) with Option_Component {
+ new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with Option_Component {
name = option_name
+ tooltip = GUI.tooltip_lines(opt.print_default)
val title = opt.title()
def load(): Unit = {
val lang = PIDE.options.string(option_name)
@@ -98,10 +97,8 @@
}
}
def save(): Unit = PIDE.options.string(option_name) = selection.item.lang
+
+ load()
}
-
- component.load()
- component.tooltip = GUI.tooltip_lines(opt.print_default)
- component
}
}
--- a/src/Tools/jEdit/src/main_plugin.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Sun Aug 14 11:11:11 2022 +0100
@@ -109,7 +109,7 @@
private def delay_load_activated(): Boolean =
delay_load_active.guarded_access(a => Some((!a, true)))
private def delay_load_action(): Unit = {
- if (Isabelle.continuous_checking && delay_load_activated() &&
+ if (JEdit_Options.continuous_checking() && delay_load_activated() &&
PerspectiveManager.isPerspectiveEnabled) {
if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
else {
@@ -189,7 +189,7 @@
case Session.Ready if !shutting_down.value =>
init_models()
- if (!Isabelle.continuous_checking) {
+ if (!JEdit_Options.continuous_checking()) {
GUI_Thread.later {
val answer =
GUI.confirm_dialog(jEdit.getActiveView,
@@ -198,7 +198,7 @@
"Continuous checking is presently disabled:",
"editor buffers will remain inactive!",
"Enable continuous checking now?")
- if (answer == 0) Isabelle.continuous_checking = true
+ if (answer == 0) JEdit_Options.continuous_checking.set()
}
}
--- a/src/Tools/jEdit/src/monitor_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -12,8 +12,8 @@
import java.awt.BorderLayout
import scala.collection.immutable.Queue
-import scala.swing.{TextField, ComboBox, Button}
-import scala.swing.event.{SelectionChanged, ButtonClicked, ValueChanged}
+import scala.swing.TextField
+import scala.swing.event.ValueChanged
import org.jfree.chart.ChartPanel
import org.jfree.data.xy.XYSeriesCollection
@@ -64,14 +64,9 @@
/* controls */
- private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1)) {
+ private val select_data = new GUI.Selector[String](ML_Statistics.all_fields.map(_._1)) {
tooltip = "Select visualized data collection"
- listenTo(selection)
- reactions += {
- case SelectionChanged(_) =>
- data_name = selection.item
- update_chart()
- }
+ override def changed(): Unit = { data_name = selection.item; update_chart() }
}
private val limit_data = new TextField("200", 5) {
@@ -83,29 +78,19 @@
reactions += { case ValueChanged(_) => input_delay.invoke() }
}
- private val reset_data = new Button("Reset") {
+ private val reset_data = new GUI.Button("Reset") {
tooltip = "Reset accumulated data"
- reactions += {
- case ButtonClicked(_) =>
- clear_statistics()
- update_chart()
- }
+ override def clicked(): Unit = { clear_statistics(); update_chart() }
}
- private val full_gc = new Button("GC") {
+ private val full_gc = new GUI.Button("GC") {
tooltip = "Full garbage collection of ML heap"
- reactions += {
- case ButtonClicked(_) =>
- PIDE.session.protocol_command("ML_Heap.full_gc")
- }
+ override def clicked(): Unit = PIDE.session.protocol_command("ML_Heap.full_gc")
}
- private val share_common_data = new Button("Sharing") {
+ private val share_common_data = new GUI.Button("Sharing") {
tooltip = "Share common data of ML heap"
- reactions += {
- case ButtonClicked(_) =>
- PIDE.session.protocol_command("ML_Heap.share_common_data")
- }
+ override def clicked(): Unit = PIDE.session.protocol_command("ML_Heap.share_common_data")
}
private val controls =
--- a/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -9,9 +9,6 @@
import isabelle._
-import scala.swing.{Button, CheckBox}
-import scala.swing.event.ButtonClicked
-
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
@@ -34,7 +31,7 @@
private def handle_resize(): Unit =
- GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
+ GUI_Thread.require { pretty_text_area.zoom(zoom) }
private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
GUI_Thread.require {}
@@ -51,7 +48,7 @@
val new_output =
if (restriction.isEmpty || restriction.get.contains(command))
- Rendering.output_messages(results)
+ Rendering.output_messages(results, JEdit_Options.output_state())
else current_output
if (current_output != new_output) {
@@ -64,35 +61,22 @@
/* controls */
- private def output_state: Boolean = PIDE.options.bool("editor_output_state")
- private def output_state_=(b: Boolean): Unit = {
- if (output_state != b) {
- PIDE.options.bool("editor_output_state") = b
- PIDE.session.update_options(PIDE.options.value)
- PIDE.editor.flush_edits(hidden = true)
- PIDE.editor.flush()
+ private val output_state_button = new JEdit_Options.output_state.GUI
+
+ private val auto_update_button = new GUI.Check("Auto update", init = do_update) {
+ tooltip = "Indicate automatic update following cursor movement"
+ override def clicked(state: Boolean): Unit = {
+ do_update = state
+ handle_update(do_update, None)
}
}
- private val output_state_button = new CheckBox("Proof state") {
- tooltip = "Output of proof state (normally shown on State panel)"
- reactions += { case ButtonClicked(_) => output_state = selected }
- selected = output_state
+ private val update_button = new GUI.Button("Update") {
+ tooltip = "Update display according to the command at cursor position"
+ override def clicked(): Unit = handle_update(true, None)
}
- private val auto_update_button = new CheckBox("Auto update") {
- tooltip = "Indicate automatic update following cursor movement"
- reactions += {
- case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
- selected = do_update
- }
-
- private val update_button = new Button("Update") {
- tooltip = "Update display according to the command at cursor position"
- reactions += { case ButtonClicked(_) => handle_update(true, None) }
- }
-
- private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+ private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
@@ -109,7 +93,7 @@
case _: Session.Global_Options =>
GUI_Thread.later {
handle_resize()
- output_state_button.selected = output_state
+ output_state_button.load()
handle_update(do_update, None)
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sun Aug 14 11:11:11 2022 +0100
@@ -122,8 +122,10 @@
refresh()
}
- def zoom(factor: Int): Unit =
+ 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,
--- a/src/Tools/jEdit/src/query_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -12,9 +12,8 @@
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
import javax.swing.{JComponent, JTextField}
-import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
- ComboBox, TabbedPane, BorderPanel}
-import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
+import scala.swing.{Component, TextField, Label, ListView, TabbedPane, BorderPanel}
+import scala.swing.event.{SelectionChanged, Key, KeyPressed}
import org.gjt.sp.jedit.View
@@ -32,7 +31,7 @@
class Query_Dockable(view: View, position: String) extends Dockable(view, position) {
/* common GUI components */
- private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+ private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
private def make_query(
property: String,
@@ -106,15 +105,14 @@
reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
}
- private val allow_dups = new CheckBox("Duplicates") {
+ private val allow_dups = new GUI.Check("Duplicates") {
tooltip = "Show all versions of matching theorems"
- selected = false
- reactions += { case ButtonClicked(_) => apply_query() }
+ override def clicked(): Unit = apply_query()
}
- private val apply_button = new Button("<html><b>Apply</b></html>") {
+ private val apply_button = new GUI.Button("<html><b>Apply</b></html>") {
tooltip = "Find theorems meeting specified criteria"
- reactions += { case ButtonClicked(_) => apply_query() }
+ override def clicked(): Unit = apply_query()
}
private val control_panel =
@@ -161,9 +159,9 @@
/* GUI page */
- private val apply_button = new Button("<html><b>Apply</b></html>") {
+ private val apply_button = new GUI.Button("<html><b>Apply</b></html>") {
tooltip = "Find constants by name / type patterns"
- reactions += { case ButtonClicked(_) => apply_query() }
+ override def clicked(): Unit = apply_query()
}
private val control_panel =
@@ -187,25 +185,24 @@
private val print_operation = new Query_Dockable.Operation(view) {
/* items */
- private class Item(val name: String, description: String, sel: Boolean) {
- val checkbox: CheckBox = new CheckBox(name) {
+ private class Item(val name: String, description: String, selected: Boolean) {
+ val gui: GUI.Check = new GUI.Check(name, init = selected) {
tooltip = "Print " + description
- selected = sel
- reactions += { case ButtonClicked(_) => apply_query() }
+ override def clicked(): Unit = apply_query()
}
}
private var _items: List[Item] = Nil
private def selected_items(): List[String] =
- for (item <- _items if item.checkbox.selected) yield item.name
+ for (item <- _items if item.gui.selected) yield item.name
private def update_items(): List[Item] = {
val old_items = _items
def was_selected(name: String): Boolean =
old_items.find(item => item.name == name) match {
case None => false
- case Some(item) => item.checkbox.selected
+ case Some(item) => item.gui.selected
}
_items =
@@ -236,11 +233,12 @@
/* GUI page */
- private val apply_button = new Button("<html><b>Apply</b></html>") {
+ private val apply_button = new GUI.Button("<html><b>Apply</b></html>") {
tooltip = "Apply to current context"
+ override def clicked(): Unit = apply_query()
+
listenTo(keys)
reactions += {
- case ButtonClicked(_) => apply_query()
case evt @ KeyPressed(_, Key.Enter, 0, _) =>
evt.peer.consume()
apply_query()
@@ -252,7 +250,7 @@
def select(): Unit = {
control_panel.contents.clear()
control_panel.contents += query_label
- update_items().foreach(item => control_panel.contents += item.checkbox)
+ 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)
@@ -302,7 +300,7 @@
/* resize */
private def handle_resize(): Unit =
- GUI_Thread.require { operations.foreach(_.pretty_text_area.zoom(zoom.factor)) }
+ GUI_Thread.require { operations.foreach(_.pretty_text_area.zoom(zoom)) }
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
--- a/src/Tools/jEdit/src/session_build.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Sun Aug 14 11:11:11 2022 +0100
@@ -12,9 +12,7 @@
import java.awt.event.{WindowEvent, WindowAdapter}
import javax.swing.{WindowConstants, JDialog}
-import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
- BorderPanel, TextArea, Component, Label}
-import scala.swing.event.ButtonClicked
+import scala.swing.{ScrollPane, FlowPanel, BorderPanel, TextArea, Component, Label}
import org.gjt.sp.jedit.View
@@ -97,7 +95,7 @@
Delay.first(Time.seconds(1.0), gui = true) {
if (can_auto_close) conclude()
else {
- val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } }
+ val button = new GUI.Button("Close") { override def clicked(): Unit = conclude() }
set_actions(button)
button.peer.getRootPane.setDefaultButton(button.peer)
}
@@ -125,21 +123,20 @@
set_actions(new Label("Stopping ..."))
}
- private val stop_button = new Button("Stop") {
- reactions += { case ButtonClicked(_) => stopping() }
+ private val stop_button = new GUI.Button("Stop") {
+ override def clicked(): Unit = stopping()
}
private var do_auto_close = true
private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
- private val auto_close = new CheckBox("Auto close") {
- reactions += {
- case ButtonClicked(_) => do_auto_close = this.selected
+ private val auto_close = new GUI.Check("Auto close", init = do_auto_close) {
+ tooltip = "Automatically close dialog when finished"
+ override def clicked(state: Boolean): Unit = {
+ do_auto_close = state
if (can_auto_close) conclude()
}
}
- auto_close.selected = do_auto_close
- auto_close.tooltip = "Automatically close dialog when finished"
set_actions(stop_button, auto_close)
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -9,8 +9,7 @@
import isabelle._
-import scala.swing.{Button, CheckBox, Orientation, Separator}
-import scala.swing.event.ButtonClicked
+import scala.swing.{Orientation, Separator}
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
@@ -45,11 +44,9 @@
val content = Pretty.separate(XML.Text(data.text) :: data.content)
text_area.update(snapshot, Command.Results.empty, content)
q.answers.foreach { answer =>
- answers.contents += new Button(answer.string) {
- reactions += {
- case ButtonClicked(_) =>
- Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
- }
+ answers.contents += new GUI.Button(answer.string) {
+ override def clicked(): Unit =
+ Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
}
}
case Nil =>
@@ -146,32 +143,17 @@
private val controls =
Wrap_Panel(
List(
- new CheckBox("Auto update") {
- selected = do_update
- reactions += {
- case ButtonClicked(_) =>
- do_update = this.selected
- handle_update(do_update)
+ new GUI.Check("Auto update", init = do_update) {
+ override def clicked(state: Boolean): Unit = {
+ do_update = state
+ handle_update(do_update)
}
},
- new Button("Update") {
- reactions += {
- case ButtonClicked(_) =>
- handle_update(true)
- }
- },
+ new GUI.Button("Update") { override def clicked(): Unit = handle_update(true) },
new Separator(Orientation.Vertical),
- new Button("Show trace") {
- reactions += {
- case ButtonClicked(_) =>
- show_trace()
- }
- },
- new Button("Clear memory") {
- reactions += {
- case ButtonClicked(_) =>
- Simplifier_Trace.clear_memory(PIDE.session)
- }
+ new GUI.Button("Show trace") { override def clicked(): Unit = show_trace() },
+ new GUI.Button("Clear memory") {
+ override def clicked(): Unit = Simplifier_Trace.clear_memory(PIDE.session)
}))
private val answers = Wrap_Panel(Nil, Wrap_Panel.Alignment.Left)
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Sun Aug 14 11:11:11 2022 +0100
@@ -11,7 +11,7 @@
import scala.annotation.tailrec
import scala.collection.immutable.SortedMap
-import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
+import scala.swing.{BorderPanel, Component, Dimension, Frame, Label, TextField}
import scala.swing.event.{Key, KeyPressed}
import scala.util.matching.Regex
@@ -133,7 +133,7 @@
GUI_Thread.require {}
private val pretty_text_area = new Pretty_Text_Area(view)
- private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = do_paint() }
+ private val zoom = new Font_Info.Zoom { override def changed(): Unit = do_paint() }
size = new Dimension(500, 500)
contents = new BorderPanel {
@@ -159,7 +159,7 @@
}
def do_paint(): Unit =
- GUI_Thread.later { pretty_text_area.zoom(zoom.factor) }
+ GUI_Thread.later { pretty_text_area.zoom(zoom) }
def handle_resize(): Unit = do_paint()
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -9,8 +9,7 @@
import isabelle._
-import scala.swing.{Button, Component, Label, CheckBox}
-import scala.swing.event.ButtonClicked
+import scala.swing.{Component, Label}
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
@@ -63,12 +62,12 @@
})
private def handle_resize(): Unit =
- GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
+ GUI_Thread.require { pretty_text_area.zoom(zoom) }
/* controls */
- private def clicked(): Unit = {
+ private def hammer(): Unit = {
provers.addCurrentToHistory()
PIDE.options.string("sledgehammer_provers") = provers.getText
sledgehammer.apply_query(
@@ -84,7 +83,7 @@
private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
override def processKeyEvent(evt: KeyEvent): Unit = {
- if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked()
+ if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) hammer()
super.processKeyEvent(evt)
}
setToolTipText(provers_label.tooltip)
@@ -100,32 +99,30 @@
}
}
- private val isar_proofs = new CheckBox("Isar proofs") {
+ private val isar_proofs = new GUI.Check("Isar proofs") {
tooltip = "Specify whether Isar proofs should be output in addition to \"by\" one-liner"
- selected = false
}
- private val try0 = new CheckBox("Try methods") {
+ private val try0 = new GUI.Check("Try methods", init = true) {
tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
- selected = true
}
- private val apply_query = new Button("<html><b>Apply</b></html>") {
+ private val apply_query = new GUI.Button("<html><b>Apply</b></html>") {
tooltip = "Search for first-order proof using automatic theorem provers"
- reactions += { case ButtonClicked(_) => clicked() }
+ override def clicked(): Unit = hammer()
}
- private val cancel_query = new Button("Cancel") {
+ private val cancel_query = new GUI.Button("Cancel") {
tooltip = "Interrupt unfinished sledgehammering"
- reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() }
+ override def clicked(): Unit = sledgehammer.cancel_query()
}
- private val locate_query = new Button("Locate") {
+ private val locate_query = new GUI.Button("Locate") {
tooltip = "Locate context of current query within source text"
- reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
+ override def clicked(): Unit = sledgehammer.locate_query()
}
- private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+ private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
--- a/src/Tools/jEdit/src/state_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -9,9 +9,6 @@
import isabelle._
-import scala.swing.{Button, CheckBox}
-import scala.swing.event.ButtonClicked
-
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
@@ -46,7 +43,7 @@
})
private def handle_resize(): Unit =
- GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
+ GUI_Thread.require { pretty_text_area.zoom(zoom) }
/* update */
@@ -78,23 +75,25 @@
/* controls */
- private val auto_update_button = new CheckBox("Auto update") {
+ private val auto_update_button = new GUI.Check("Auto update", init = auto_update_enabled) {
tooltip = "Indicate automatic update following cursor movement"
- reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() }
- selected = auto_update_enabled
+ override def clicked(state: Boolean): Unit = {
+ auto_update_enabled = state
+ auto_update()
+ }
}
- private val update_button = new Button("<html><b>Update</b></html>") {
+ private val update_button = new GUI.Button("<html><b>Update</b></html>") {
tooltip = "Update display according to the command at cursor position"
- reactions += { case ButtonClicked(_) => update_request() }
+ override def clicked(): Unit = update_request()
}
- private val locate_button = new Button("Locate") {
+ private val locate_button = new GUI.Button("Locate") {
tooltip = "Locate printed command within source text"
- reactions += { case ButtonClicked(_) => print_state.locate_query() }
+ override def clicked(): Unit = print_state.locate_query()
}
- private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+ private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
--- a/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 13 20:08:24 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sun Aug 14 11:11:11 2022 +0100
@@ -11,7 +11,7 @@
import scala.swing.{Button, TextArea, Label, ListView, Alignment,
ScrollPane, Component, CheckBox, BorderPanel}
-import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
+import scala.swing.event.{MouseClicked, MouseMoved}
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
import javax.swing.{JList, BorderFactory, UIManager}
@@ -43,9 +43,9 @@
case MouseMoved(_, point, _) =>
val index = peer.locationToIndex(point)
val index_location = peer.indexToLocation(index)
- if (index >= 0 && in_checkbox(index_location, point))
+ if (index >= 0 && in_checkbox(index_location, point)) {
tooltip = "Mark as required for continuous checking"
- else if (index >= 0 && in_label(index_location, point)) {
+ } else if (index >= 0 && in_label(index_location, point)) {
val name = listData(index)
val st = nodes_status.overall_node_status(name)
tooltip =
@@ -75,12 +75,12 @@
session_phase.text = " " + phase_text(phase) + " "
}
- private val purge = new Button("Purge") {
+ private val purge = new GUI.Button("Purge") {
tooltip = "Restrict document model to theories required for open editor buffers"
- reactions += { case ButtonClicked(_) => PIDE.editor.purge() }
+ override def clicked(): Unit = PIDE.editor.purge()
}
- private val continuous_checking = new Isabelle.Continuous_Checking
+ private val continuous_checking = new JEdit_Options.continuous_checking.GUI
continuous_checking.focusable = false
private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true)
@@ -96,39 +96,48 @@
private var nodes_status = Document_Status.Nodes_Status.empty
private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
- private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
- geometry match {
- case Some((loc, size)) =>
- loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
- loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
- case None => false
+ private class Geometry {
+ private var location: Point = null
+ private var size: Dimension = null
+
+ def in(location0: Point, p: Point): Boolean = {
+ location != null && size != null &&
+ location0.x + location.x <= p.x && p.x < location0.x + size.width &&
+ location0.y + location.y <= p.y && p.y < location0.y + size.height
}
- private def in_checkbox(loc0: Point, p: Point): Boolean =
- Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p)
+ def update(new_location: Point, new_size: Dimension): Unit = {
+ if (new_location != null && new_size != null) {
+ location = new_location
+ size = new_size
+ }
+ }
+ }
- private def in_label(loc0: Point, p: Point): Boolean =
- Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p)
+ private def in_checkbox(location0: Point, p: Point): Boolean =
+ Node_Renderer_Component != null && Node_Renderer_Component.checkbox_geometry.in(location0, p)
+
+ private def in_label(location0: Point, p: Point): Boolean =
+ Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p)
private object Node_Renderer_Component extends BorderPanel {
opaque = true
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
- var node_name = Document.Node.Name.empty
+ var node_name: Document.Node.Name = Document.Node.Name.empty
- var checkbox_geometry: Option[(Point, Dimension)] = None
- val checkbox = new CheckBox {
+ val checkbox_geometry = new Geometry
+ val checkbox: CheckBox = new CheckBox {
opaque = false
override def paintComponent(gfx: Graphics2D): Unit = {
super.paintComponent(gfx)
- if (location != null && size != null)
- checkbox_geometry = Some((location, size))
+ checkbox_geometry.update(location, size)
}
}
- var label_geometry: Option[(Point, Dimension)] = None
- val label = new Label {
+ val label_geometry = new Geometry
+ val label: Label = new Label {
background = view.getTextArea.getPainter.getBackground
foreground = view.getTextArea.getPainter.getForeground
opaque = false
@@ -163,8 +172,7 @@
}
super.paintComponent(gfx)
- if (location != null && size != null)
- label_geometry = Some((location, size))
+ label_geometry.update(location, size)
}
}