--- a/src/Pure/GUI/gui.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/GUI/gui.scala Thu Nov 10 08:13:28 2022 +0100
@@ -9,11 +9,14 @@
import java.util.{Map => JMap}
import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
+import java.awt.event.{KeyAdapter, KeyEvent, ItemListener, ItemEvent}
import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
import java.awt.geom.AffineTransform
import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
- JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
-import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea}
+ JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities}
+
+import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
+ Orientation}
import scala.swing.event.{ButtonClicked, SelectionChanged}
@@ -127,9 +130,74 @@
reactions += { case ButtonClicked(_) => clicked(selected); clicked() }
}
- class Selector[A](val entries: List[A]) extends ComboBox[A](entries) {
+
+ /* list selector */
+
+ object Selector {
+ sealed abstract class Entry[A] {
+ def get_item: Option[A] =
+ this match {
+ case item: Item[_] => Some(item.item)
+ case _ => None
+ }
+ }
+ case class Item[A](item: A, description: String = "", batch: Int = 0) extends Entry[A] {
+ override def toString: String = proper_string(description) getOrElse item.toString
+ }
+ case class Separator[A](name: String = "", batch: Int = 0) extends Entry[A] {
+ override def toString: String = "<b>" + name + "</b>"
+ }
+
+ def item(name: String, batch: Int = 0): Item[String] = Item(name, batch = batch)
+ def separator(batch: Int = 0): Separator[String] = Separator(batch = batch)
+ }
+
+ class Selector[A](val entries: List[Selector.Entry[A]])
+ extends ComboBox[Selector.Entry[A]](entries) {
def changed(): Unit = {}
+ override lazy val peer: JComboBox[Selector.Entry[A]] =
+ new JComboBox[Selector.Entry[A]](ComboBox.newConstantModel(entries)) with SuperMixin {
+ private var key_released = false
+ private var sep_selected = false
+
+ addKeyListener(new KeyAdapter {
+ override def keyPressed(e: KeyEvent): Unit = { key_released = false }
+ override def keyReleased(e: KeyEvent): Unit = { key_released = true }
+ })
+
+ override def setSelectedIndex(i: Int): Unit = {
+ getItemAt(i) match {
+ case _: Selector.Separator[_] =>
+ if (key_released) { sep_selected = true }
+ else {
+ val k = getSelectedIndex()
+ val j = if (i > k) i + 1 else i - 1
+ if (0 <= j && j < dataModel.getSize()) super.setSelectedIndex(j)
+ }
+ case _ => super.setSelectedIndex(i)
+ }
+ }
+
+ override def setPopupVisible(visible: Boolean): Unit = {
+ if (sep_selected) { sep_selected = false}
+ else super.setPopupVisible(visible)
+ }
+ }
+
+ private val default_renderer = renderer
+ private val render_separator = new Separator
+ private val render_label = new Label
+ renderer =
+ (list: ListView[_ <: Selector.Entry[A]], selected: Boolean, focus: Boolean, entry: Selector.Entry[A], i: Int) => {
+ entry match {
+ case sep: Selector.Separator[_] =>
+ if (sep.name.isEmpty) render_separator
+ else { render_label.text = entry.toString; render_label }
+ case _ => default_renderer.componentFor(list, selected, focus, entry, i)
+ }
+ }
+
listenTo(selection)
reactions += { case SelectionChanged(_) => changed() }
}
@@ -141,8 +209,9 @@
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)
+ def factor: Int = parse(selection.item.toString)
private def parse(text: String): Int =
text match {
@@ -161,7 +230,8 @@
}
}
- makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
+ makeEditable()(c =>
+ new ComboBox.BuiltInEditor(c)(text => Selector.Item(print(parse(text))), _.toString))
peer.getEditor.getEditorComponent match {
case text: JTextField => text.setColumns(4)
case _ =>
--- a/src/Pure/PIDE/session.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/PIDE/session.scala Thu Nov 10 08:13:28 2022 +0100
@@ -85,20 +85,22 @@
/* syslog */
- private[Session] class Syslog(limit: Int) {
- private var queue = Queue.empty[XML.Elem]
+ class Syslog(limit: Int) {
+ private var queue = Queue.empty[String]
private var length = 0
- def += (msg: XML.Elem): Unit = synchronized {
+ def += (msg: String): Unit = synchronized {
queue = queue.enqueue(msg)
length += 1
if (length > limit) queue = queue.dequeue._2
}
- def content: String = synchronized {
- cat_lines(queue.iterator.map(XML.content)) +
+ def content(): String = synchronized {
+ cat_lines(queue.iterator) +
(if (length > limit) "\n(A total of " + length + " messages...)" else "")
}
+
+ override def toString: String = "Syslog(" + length + ")"
}
@@ -221,8 +223,9 @@
/* syslog */
- private val syslog = new Session.Syslog(syslog_limit)
- def syslog_content(): String = syslog.content
+ def make_syslog(): Session.Syslog = new Session.Syslog(syslog_limit)
+
+ val syslog: Session.Syslog = make_syslog()
/* pipelined change parsing */
@@ -577,7 +580,7 @@
arg match {
case output: Prover.Output =>
if (output.is_syslog) {
- syslog += output.message
+ syslog += XML.content(output.message)
syslog_messages.post(output)
}
--- a/src/Pure/System/isabelle_process.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/System/isabelle_process.scala Thu Nov 10 08:13:28 2022 +0100
@@ -56,7 +56,7 @@
startup.fulfill("")
case Session.Terminated(result) =>
if (!result.ok && !startup.is_finished) {
- val syslog = session.syslog_content()
+ val syslog = session.syslog.content()
val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog)
startup.fulfill(err)
}
--- a/src/Pure/Thy/sessions.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Nov 10 08:13:28 2022 +0100
@@ -507,6 +507,9 @@
def dirs: List[Path] = dir :: directories
+ def main_group: Boolean = groups.contains("main")
+ def doc_group: Boolean = groups.contains("doc")
+
def timeout_ignored: Boolean =
!options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
--- a/src/Pure/Tools/spell_checker.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Pure/Tools/spell_checker.scala Thu Nov 10 08:13:28 2022 +0100
@@ -85,12 +85,14 @@
}
}
- def dictionaries: List[Dictionary] =
+ lazy val dictionaries: List[Dictionary] =
for {
path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
if path.is_file
} yield new Dictionary(path)
+ def get_dictionary(lang: String): Option[Dictionary] = dictionaries.find(_.lang == lang)
+
/* create spell checker */
@@ -260,7 +262,7 @@
if (options.bool("spell_checker")) {
val lang = options.string("spell_checker_dictionary")
if (current_spell_checker._1 != lang) {
- Spell_Checker.dictionaries.find(_.lang == lang) match {
+ Spell_Checker.get_dictionary(lang) match {
case Some(dictionary) =>
val spell_checker =
Exn.capture { Spell_Checker(dictionary) } match {
--- a/src/Tools/jEdit/src/document_dockable.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Thu Nov 10 08:13:28 2022 +0100
@@ -18,8 +18,40 @@
object Document_Dockable {
- def document_output(): Path =
- Path.explode("$ISABELLE_HOME_USER/document/root.pdf")
+ /* document output */
+
+ def document_name: String = "document"
+ def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
+ def document_output(): Path = document_output_dir() + Path.basic(document_name)
+
+ def view_document(): Unit = {
+ val path = Document_Dockable.document_output().pdf
+ if (path.is_file) Isabelle_System.pdf_viewer(path)
+ }
+
+ class Log_Progress extends Progress {
+ def show(text: String): Unit = {}
+
+ private val syslog = PIDE.session.make_syslog()
+
+ private def update(text: String = syslog.content()): Unit = GUI_Thread.require { show(text) }
+ private val delay =
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() }
+
+ override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
+ override def theory(theory: Progress.Theory): Unit = echo(theory.message)
+
+ def load(): Unit = {
+ val path = document_output().log
+ val text = if (path.is_file) File.read(path) else ""
+ GUI_Thread.later { delay.revoke(); update(text) }
+ }
+
+ update()
+ }
+
+
+ /* state */
object Status extends Enumeration {
val WAITING = Value("waiting")
@@ -32,16 +64,15 @@
}
object State {
- val empty: State = State()
+ def empty(): State = State()
def finish(result: Result): State = State(output = result.output)
}
sealed case class State(
- progress: Progress = new Progress,
+ progress: Log_Progress = new Log_Progress,
process: Future[Unit] = Future.value(()),
output: List[XML.Tree] = Nil,
- status: Status.Value = Status.FINISHED
- )
+ status: Status.Value = Status.FINISHED)
}
class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
@@ -50,7 +81,7 @@
/* component state -- owned by GUI thread */
- private val current_state = Synchronized(Document_Dockable.State.empty)
+ private val current_state = Synchronized(Document_Dockable.State.empty())
private val process_indicator = new Process_Indicator
private val pretty_text_area = new Pretty_Text_Area(view)
@@ -94,28 +125,22 @@
/* progress log */
- private val log_area = new TextArea {
- editable = false
- columns = 60
- rows = 24
- }
- log_area.font = GUI.copy_font((new Label).font)
-
+ private val log_area =
+ new TextArea {
+ editable = false
+ font = GUI.copy_font((new Label).font)
+ }
private val scroll_log_area = new ScrollPane(log_area)
- private def init_progress() = {
- GUI_Thread.later { log_area.text = "" }
- new Progress {
- override def echo(txt: String): Unit =
- GUI_Thread.later {
- log_area.append(txt + "\n")
+ def init_progress(): Document_Dockable.Log_Progress =
+ new Document_Dockable.Log_Progress {
+ override def show(text: String): Unit =
+ if (text != log_area.text) {
+ log_area.text = text
val vertical = scroll_log_area.peer.getVerticalScrollBar
vertical.setValue(vertical.getMaximum)
}
-
- override def theory(theory: Progress.Theory): Unit = echo(theory.message)
}
- }
/* document build process */
@@ -123,6 +148,9 @@
private def cancel(): Unit =
current_state.change { st => st.process.cancel(); st }
+ private def init_state(): Unit =
+ current_state.change { _ => Document_Dockable.State(progress = init_progress()) }
+
private def build_document(): Unit = {
current_state.change { st =>
if (st.process.is_finished) {
@@ -133,7 +161,10 @@
val res =
Exn.capture {
progress.echo("Start " + Date.now())
- Time.seconds(2.0).sleep()
+ for (i <- 1 to 200) {
+ progress.echo("message " + i)
+ Time.seconds(0.1).sleep()
+ }
progress.echo("Stop " + Date.now())
}
val msg =
@@ -153,18 +184,20 @@
show_state()
}
- private def view_document(): Unit = {
- val path = Document_Dockable.document_output()
- if (path.is_file) Isabelle_System.pdf_viewer(path)
- }
-
/* controls */
- private val document_session: GUI.Selector[String] =
- new GUI.Selector(JEdit_Sessions.sessions_structure().build_topological_order.sorted) {
+ private val document_session: GUI.Selector[String] = {
+ val sessions = JEdit_Sessions.sessions_structure()
+ val all_sessions = sessions.build_topological_order.sorted
+ val doc_sessions = all_sessions.filter(name => sessions(name).doc_group)
+ new GUI.Selector(
+ doc_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) :::
+ all_sessions.map(GUI.Selector.item(_, batch = 1))
+ ) {
val title = "Session"
}
+ }
private val build_button =
new GUI.Button("<html><b>Build</b></html>") {
@@ -181,7 +214,7 @@
private val view_button =
new GUI.Button("View") {
tooltip = "View document"
- override def clicked(): Unit = view_document()
+ override def clicked(): Unit = Document_Dockable.view_document()
}
private val controls =
@@ -204,9 +237,19 @@
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
}, "Output from build process")
+ private val load_button =
+ new GUI.Button("Load") {
+ tooltip = "Load final log file"
+ override def clicked(): Unit = current_state.value.progress.load()
+ }
+
+ private val log_controls =
+ Wrap_Panel(List(load_button))
+
private val log_page =
new TabbedPane.Page("Log", new BorderPanel {
- layout(log_area) = BorderPanel.Position.Center
+ layout(log_controls) = BorderPanel.Position.North
+ layout(scroll_log_area) = BorderPanel.Position.Center
}, "Raw log of build process")
message_pane.pages ++= List(log_page, output_page)
@@ -223,6 +266,7 @@
}
override def init(): Unit = {
+ init_state()
PIDE.session.global_options += main
handle_resize()
}
--- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 10 08:13:28 2022 +0100
@@ -69,35 +69,38 @@
/* logic selector */
- private sealed case class Logic_Entry(name: String = "", description: String = "") {
- override def toString: String = proper_string(description) getOrElse name
- }
-
def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = {
GUI_Thread.require {}
- val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")")
+ val default_entry =
+ GUI.Selector.Item("", description = "default (" + logic_name(options.value) + ")")
val session_entries = {
val sessions = sessions_structure(options = options.value)
- val (main_sessions, other_sessions) =
- sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main"))
- (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name))
+ val all_sessions = sessions.imports_topological_order
+ val main_sessions = all_sessions.filter(name => sessions(name).main_group)
+
+ main_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) :::
+ all_sessions.sorted.map(GUI.Selector.item(_, batch = 1))
}
- new GUI.Selector[Logic_Entry](default_entry :: session_entries)
- with JEdit_Options.Entry {
+ new GUI.Selector(default_entry :: session_entries) with JEdit_Options.Entry {
name = jedit_logic_option
tooltip = "Logic session name (change requires restart)"
val title = "Logic"
def load(): Unit = {
val logic = options.string(jedit_logic_option)
- entries.find(_.name == logic) match {
+ entries.find {
+ case item: GUI.Selector.Item[_] => item.item == logic
+ case _ => false
+ } match {
case Some(entry) => selection.item = entry
case None =>
}
}
- def save(): Unit = options.string(jedit_logic_option) = selection.item.name
+ def save(): Unit =
+ for (item <- selection.item.get_item) options.string(jedit_logic_option) = item
+
override def changed(): Unit = if (autosave) save()
load()
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Thu Nov 10 08:13:28 2022 +0100
@@ -85,18 +85,19 @@
val option_name = "spell_checker_dictionary"
val opt = PIDE.options.value.check_name(option_name)
- new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with JEdit_Options.Entry {
+ new GUI.Selector(Spell_Checker.dictionaries.map(GUI.Selector.Item(_))) with JEdit_Options.Entry {
name = option_name
tooltip = GUI.tooltip_lines(opt.print_default)
val title = opt.title()
def load(): Unit = {
val lang = PIDE.options.string(option_name)
- entries.find(_.lang == lang) match {
- case Some(entry) => selection.item = entry
+ Spell_Checker.get_dictionary(lang) match {
+ case Some(dict) => selection.item = GUI.Selector.Item(dict)
case None =>
}
}
- def save(): Unit = PIDE.options.string(option_name) = selection.item.lang
+ def save(): Unit =
+ for (item <- selection.item.get_item) PIDE.options.string(option_name) = item.lang
load()
}
--- a/src/Tools/jEdit/src/main_plugin.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Thu Nov 10 08:13:28 2022 +0100
@@ -183,7 +183,7 @@
case Session.Terminated(result) if !result.ok =>
GUI_Thread.later {
GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
- "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
+ "Isabelle Syslog", GUI.scrollable_text(session.syslog.content()))
}
case Session.Ready if !shutting_down.value =>
--- a/src/Tools/jEdit/src/monitor_dockable.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Thu Nov 10 08:13:28 2022 +0100
@@ -64,10 +64,11 @@
/* controls */
- private val select_data = new GUI.Selector[String](ML_Statistics.all_fields.map(_._1)) {
- tooltip = "Select visualized data collection"
- override def changed(): Unit = { data_name = selection.item; update_chart() }
- }
+ private val select_data =
+ new GUI.Selector(ML_Statistics.all_fields.map { case (a, _) => GUI.Selector.item(a) }) {
+ tooltip = "Select visualized data collection"
+ override def changed(): Unit = { data_name = selection.item.toString; update_chart() }
+ }
private val limit_data = new TextField("200", 5) {
tooltip = "Limit for accumulated data"
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Thu Nov 10 08:13:28 2022 +0100
@@ -60,12 +60,12 @@
case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
case None => (stack, Nil)
}
- old.foreach(_.hide_popup)
+ 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
+ tip.show_popup()
}
}
}
@@ -123,7 +123,7 @@
case (Nil, _) =>
case (unfocused, rest) =>
deactivate()
- unfocused.foreach(_.hide_popup)
+ unfocused.foreach(_.hide_popup())
stack = rest
}
}
@@ -133,11 +133,11 @@
hierarchy(tip) match {
case Some((old, _ :: rest)) =>
rest match {
- case top :: _ => top.request_focus
+ case top :: _ => top.request_focus()
case Nil => JEdit_Lib.request_focus_view()
}
- old.foreach(_.hide_popup)
- tip.hide_popup
+ old.foreach(_.hide_popup())
+ tip.hide_popup()
stack = rest
case _ =>
}
@@ -151,7 +151,7 @@
if (stack.isEmpty) false
else {
JEdit_Lib.request_focus_view()
- stack.foreach(_.hide_popup)
+ stack.foreach(_.hide_popup())
stack = Nil
true
}
@@ -202,7 +202,7 @@
val pretty_text_area: Pretty_Text_Area =
new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
- override def get_background() = Some(rendering.tooltip_color)
+ override def get_background(): Option[Color] = Some(rendering.tooltip_color)
}
pretty_text_area.addFocusListener(new FocusAdapter {
@@ -269,14 +269,14 @@
new Popup(layered, tip, screen.relative(layered, size), size)
}
- private def show_popup: Unit = {
+ private def show_popup(): Unit = {
popup.show
pretty_text_area.requestFocus()
pretty_text_area.update(rendering.snapshot, results, info.info)
}
- private def hide_popup: Unit = popup.hide
+ private def hide_popup(): Unit = popup.hide
- private def request_focus: Unit = pretty_text_area.requestFocus()
+ private def request_focus(): Unit = pretty_text_area.requestFocus()
}
--- a/src/Tools/jEdit/src/syslog_dockable.scala Wed Nov 09 16:36:22 2022 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Thu Nov 10 08:13:28 2022 +0100
@@ -20,7 +20,7 @@
private val syslog = new TextArea()
private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
- val text = PIDE.session.syslog_content()
+ val text = PIDE.session.syslog.content()
if (text != syslog.text) syslog.text = text
}