diff --git a/src/Pure/GUI/gui.scala b/src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala
+++ b/src/Pure/GUI/gui.scala
@@ -1,443 +1,459 @@
/* Title: Pure/GUI/gui.scala
Author: Makarius
Basic GUI tools (for AWT/Swing).
*/
package isabelle
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, JComboBox, LookAndFeel, UIManager, SwingUtilities}
import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
Orientation}
import scala.swing.event.{ButtonClicked, SelectionChanged}
object GUI {
/* Swing look-and-feel */
def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.setup()
def current_laf: String = UIManager.getLookAndFeel.getClass.getName()
def is_macos_laf: Boolean =
Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf
class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service {
def info: UIManager.LookAndFeelInfo =
new UIManager.LookAndFeelInfo(laf.getName, laf.getClass.getName)
}
lazy val look_and_feels: List[Look_And_Feel] =
Isabelle_System.make_services(classOf[Look_And_Feel])
def init_lafs(): Unit = {
val old_lafs =
Set(
"com.sun.java.swing.plaf.motif.MotifLookAndFeel",
"com.sun.java.swing.plaf.windows.WindowsClassicLookAndFeel")
val lafs =
UIManager.getInstalledLookAndFeels().toList
.filterNot(info => old_lafs(info.getClassName))
val more_lafs = look_and_feels.map(_.info)
UIManager.setInstalledLookAndFeels((more_lafs ::: lafs).toArray)
}
/* additional look-and-feels */
/* plain focus traversal, notably for text fields */
def plain_focus_traversal(component: Component): Unit = {
val dummy_button = new JButton
def apply(id: Int): Unit =
component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
}
/* simple dialogs */
def scrollable_text(
raw_txt: String,
width: Int = 60,
height: Int = 20,
editable: Boolean = false
) : ScrollPane = {
val txt = Output.clean_yxml(raw_txt)
val text = new TextArea(txt)
if (width > 0) text.columns = width
if (height > 0 && split_lines(txt).length > height) text.rows = height
text.editable = editable
new ScrollPane(text)
}
private def simple_dialog(
kind: Int,
default_title: String,
parent: Component,
title: String,
message: Iterable[Any]
): Unit = {
GUI_Thread.now {
val java_message =
message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }).
toArray.asInstanceOf[Array[AnyRef]]
JOptionPane.showMessageDialog(parent, java_message,
if (title == null) default_title else title, kind)
}
}
def dialog(parent: Component, title: String, message: Any*): Unit =
simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
def warning_dialog(parent: Component, title: String, message: Any*): Unit =
simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
def error_dialog(parent: Component, title: String, message: Any*): Unit =
simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
GUI_Thread.now {
val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
JOptionPane.showConfirmDialog(parent,
java_message.toArray.asInstanceOf[Array[AnyRef]], title,
option_type, JOptionPane.QUESTION_MESSAGE)
}
/* 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() }
}
/* list selector */
object Selector {
- sealed abstract class Entry[A] {
- def get_item: Option[A] =
- this match {
- case item: Item[_] => Some(item.item)
+ sealed abstract class Entry[A] { def get_value: Option[A] = Value.unapply(this) }
+ object Value {
+ def unapply[A](entry: Entry[A]): Option[A] =
+ entry match {
+ case item: Item[_] => Some(item.value)
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
+ def item[A](value: A): Entry[A] = Item(value, "", 0)
+ def item_description[A](value: A, description: String): Entry[A] = Item(value, description, 0)
+
+ private case class Item[A](value: A, description: String, batch: Int) extends Entry[A] {
+ override def toString: String = proper_string(description) getOrElse value.toString
}
- case class Separator[A](name: String = "", batch: Int = 0) extends Entry[A] {
- override def toString: String = "" + name + ""
+ private case class Separator[A](batch: Int) extends Entry[A] {
+ override def toString: String = "---"
}
- def item(name: String, batch: Int = 0): Item[String] = Item(name, batch = batch)
- def separator(batch: Int = 0): Separator[String] = Separator(batch = batch)
+ private def make_entries[A](batches: List[List[Entry[A]]]): List[Entry[A]] = {
+ val item_batches =
+ batches.map(_.flatMap(
+ { case item: Item[_] => Some(item.asInstanceOf[Item[A]]) case _ => None }))
+ val sep_entries: List[Entry[A]] =
+ item_batches.filter(_.nonEmpty).zipWithIndex.flatMap({ case (batch, i) =>
+ Separator[A](i) :: batch.map(_.copy(batch = i))
+ })
+ sep_entries.tail
+ }
}
- class Selector[A](val entries: List[Selector.Entry[A]])
- extends ComboBox[Selector.Entry[A]](entries) {
+ class Selector[A](batches: List[Selector.Entry[A]]*)
+ extends ComboBox[Selector.Entry[A]](Selector.make_entries(batches.toList)) {
def changed(): Unit = {}
+ lazy val entries: List[Selector.Entry[A]] = Selector.make_entries(batches.toList)
+
+ def find_value(pred: A => Boolean): Option[Selector.Entry[A]] =
+ entries.find({ case item: Selector.Item[A] => pred(item.value) case _ => false })
+
+ def selection_value: Option[A] = selection.item.get_value
+
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 _: Selector.Separator[_] => render_separator
case _ => default_renderer.componentFor(list, selected, focus, entry, i)
}
}
listenTo(selection)
reactions += { case SelectionChanged(_) => changed() }
}
/* zoom factor */
private val Zoom_Factor = "([0-9]+)%?".r
class Zoom extends Selector[String](
List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
- .map(GUI.Selector.item(_))
+ .map(GUI.Selector.item)
) {
def factor: Int = parse(selection.item.toString)
private def parse(text: String): Int =
text match {
case Zoom_Factor(s) =>
val i = Integer.parseInt(s)
if (10 <= i && i < 1000) i else 100
case _ => 100
}
private def print(i: Int): String = i.toString + "%"
def set_item(i: Int): Unit = {
peer.getEditor match {
case null =>
case editor => editor.setItem(print(i))
}
}
makeEditable()(c =>
- new ComboBox.BuiltInEditor(c)(text => Selector.Item(print(parse(text))), _.toString))
+ new ComboBox.BuiltInEditor(c)(text => Selector.item(print(parse(text))), _.toString))
peer.getEditor.getEditorComponent match {
case text: JTextField => text.setColumns(4)
case _ =>
}
selection.index = 3
}
/* tooltip with multi-line support */
def tooltip_lines(text: String): String =
if (text == null || text == "") null
else "" + HTML.output(text) + ""
/* icon */
def isabelle_icon(): ImageIcon =
new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif"))
def isabelle_icons(): List[ImageIcon] =
for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif"))
yield new ImageIcon(getClass.getClassLoader.getResource(icon))
def isabelle_image(): Image = isabelle_icon().getImage
/* location within multi-screen environment */
final case class Screen_Location(point: Point, bounds: Rectangle) {
def relative(parent: Component, size: Dimension): Point = {
val w = size.width
val h = size.height
val x0 = parent.getLocationOnScreen.x
val y0 = parent.getLocationOnScreen.y
val x1 = x0 + parent.getWidth - w
val y1 = y0 + parent.getHeight - h
val x2 = point.x min (bounds.x + bounds.width - w)
val y2 = point.y min (bounds.y + bounds.height - h)
val location = new Point((x2 min x1) max x0, (y2 min y1) max y0)
SwingUtilities.convertPointFromScreen(location, parent)
location
}
}
def screen_location(component: Component, point: Point): Screen_Location = {
val screen_point = new Point(point.x, point.y)
if (component != null) SwingUtilities.convertPointToScreen(screen_point, component)
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
val screen_bounds =
(for {
device <- ge.getScreenDevices.iterator
config <- device.getConfigurations.iterator
bounds = config.getBounds
} yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
Screen_Location(screen_point, screen_bounds)
}
def mouse_location(): Screen_Location =
screen_location(null, MouseInfo.getPointerInfo.getLocation)
/* screen size */
sealed case class Screen_Size(bounds: Rectangle, insets: Insets) {
def full_screen_bounds: Rectangle =
if (Platform.is_linux) {
// avoid menu bar and docking areas
new Rectangle(
bounds.x + insets.left,
bounds.y + insets.top,
bounds.width - insets.left - insets.right,
bounds.height - insets.top - insets.bottom)
}
else if (Platform.is_macos) {
// avoid menu bar, but ignore docking areas
new Rectangle(
bounds.x,
bounds.y + insets.top,
bounds.width,
bounds.height - insets.top)
}
else bounds
}
def screen_size(component: Component): Screen_Size = {
val config = component.getGraphicsConfiguration
val bounds = config.getBounds
val insets = Toolkit.getDefaultToolkit.getScreenInsets(config)
Screen_Size(bounds, insets)
}
/* component hierachy */
def get_parent(component: Component): Option[Container] =
component.getParent match {
case null => None
case parent => Some(parent)
}
def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
private var next_elem = get_parent(component)
def hasNext: Boolean = next_elem.isDefined
def next(): Container =
next_elem match {
case Some(parent) =>
next_elem = get_parent(parent)
parent
case None => Iterator.empty.next()
}
}
def parent_window(component: Component): Option[Window] =
ancestors(component).collectFirst({ case x: Window => x })
def layered_pane(component: Component): Option[JLayeredPane] =
parent_window(component) match {
case Some(w: JWindow) => Some(w.getLayeredPane)
case Some(w: JFrame) => Some(w.getLayeredPane)
case Some(w: JDialog) => Some(w.getLayeredPane)
case _ => None
}
def traverse_components(component: Component, apply: Component => Unit): Unit = {
def traverse(comp: Component): Unit = {
apply(comp)
comp match {
case cont: Container =>
for (i <- 0 until cont.getComponentCount)
traverse(cont.getComponent(i))
case _ =>
}
}
traverse(component)
}
/* font operations */
def copy_font(font: Font): Font =
if (font == null) null
else new Font(font.getFamily, font.getStyle, font.getSize)
def line_metrics(font: Font): LineMetrics =
font.getLineMetrics("", new FontRenderContext(null, false, false))
def transform_font(font: Font, transform: AffineTransform): Font =
font.deriveFont(JMap.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
def label_font(): Font = (new JLabel).getFont
/* Isabelle fonts */
def imitate_font(
font: Font,
family: String = Isabelle_Fonts.sans,
scale: Double = 1.0
): Font = {
val font1 = new Font(family, font.getStyle, font.getSize)
val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt)
}
def imitate_font_css(
font: Font,
family: String = Isabelle_Fonts.sans,
scale: Double = 1.0
): String = {
val font1 = new Font(family, font.getStyle, font.getSize)
val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
"font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
}
def use_isabelle_fonts(): Unit = {
val default_font = label_font()
val ui = UIManager.getDefaults
for (prop <-
List(
"ToggleButton.font",
"CheckBoxMenuItem.font",
"Label.font",
"Menu.font",
"MenuItem.font",
"PopupMenu.font",
"Table.font",
"TableHeader.font",
"TextArea.font",
"TextField.font",
"TextPane.font",
"ToolTip.font",
"Tree.font")) {
val font = ui.get(prop) match { case font: Font => font case _ => default_font }
ui.put(prop, GUI.imitate_font(font))
}
}
}
class FlatLightLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatLightLaf)
class FlatDarkLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatDarkLaf)
diff --git a/src/Tools/jEdit/src/document_dockable.scala b/src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala
+++ b/src/Tools/jEdit/src/document_dockable.scala
@@ -1,278 +1,278 @@
/* Title: Tools/jEdit/src/document_dockable.scala
Author: Makarius
Dockable window for document build support.
*/
package isabelle.jedit
import isabelle._
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component}
import org.gjt.sp.jedit.{jEdit, View}
object Document_Dockable {
/* 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")
val RUNNING = Value("running")
val FINISHED = Value("finished")
}
sealed case class Result(output: List[XML.Tree] = Nil) {
def failed: Boolean = output.exists(Protocol.is_error)
}
object State {
def empty(): State = State()
def finish(result: Result): State = State(output = result.output)
}
sealed case class State(
progress: Log_Progress = new Log_Progress,
process: Future[Unit] = Future.value(()),
output: List[XML.Tree] = Nil,
status: Status.Value = Status.FINISHED)
}
class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
GUI_Thread.require {}
/* component state -- owned by GUI thread */
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)
private val message_pane = new TabbedPane
private def show_state(): Unit = GUI_Thread.later {
val st = current_state.value
pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output)
st.status match {
case Document_Dockable.Status.WAITING =>
process_indicator.update("Waiting for PIDE document content ...", 5)
case Document_Dockable.Status.RUNNING =>
process_indicator.update("Running document build process ...", 15)
case Document_Dockable.Status.FINISHED =>
process_indicator.update(null, 0)
}
}
private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later {
message_pane.selection.page = page
}
/* text area with zoom/resize */
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 val delay_resize: Delay =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
/* progress log */
private val log_area =
new TextArea {
editable = false
font = GUI.copy_font((new Label).font)
}
private val scroll_log_area = new ScrollPane(log_area)
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)
}
}
/* document build process */
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) {
val progress = init_progress()
val process =
Future.thread[Unit](name = "document_build") {
show_page(log_page)
val res =
Exn.capture {
progress.echo("Start " + Date.now())
for (i <- 1 to 200) {
progress.echo("message " + i)
Time.seconds(0.1).sleep()
}
progress.echo("Stop " + Date.now())
}
val msg =
res match {
case Exn.Res(_) => Protocol.make_message(XML.string("OK"))
case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn)))
}
val result = Document_Dockable.Result(output = List(msg))
current_state.change(_ => Document_Dockable.State.finish(result))
show_state()
show_page(output_page)
}
st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)
}
else st
}
show_state()
}
/* controls */
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))
+ new GUI.Selector[String](
+ doc_sessions.map(GUI.Selector.item),
+ all_sessions.map(GUI.Selector.item)
) {
val title = "Session"
}
}
private val build_button =
new GUI.Button("Build") {
tooltip = "Build document"
override def clicked(): Unit = build_document()
}
private val cancel_button =
new GUI.Button("Cancel") {
tooltip = "Cancel build process"
override def clicked(): Unit = cancel()
}
private val view_button =
new GUI.Button("View") {
tooltip = "View document"
override def clicked(): Unit = Document_Dockable.view_document()
}
private val controls =
Wrap_Panel(List(document_session, process_indicator.component, build_button,
view_button, cancel_button))
add(controls.peer, BorderLayout.NORTH)
override def focusOnDefaultComponent(): Unit = build_button.requestFocus()
/* message pane with pages */
private val output_controls =
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
private val output_page =
new TabbedPane.Page("Output", new BorderPanel {
layout(output_controls) = BorderPanel.Position.North
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_controls) = BorderPanel.Position.North
layout(scroll_log_area) = BorderPanel.Position.Center
}, "Raw log of build process")
message_pane.pages ++= List(log_page, output_page)
set_content(message_pane)
/* main */
private val main =
Session.Consumer[Session.Global_Options](getClass.getName) {
case _: Session.Global_Options =>
GUI_Thread.later { handle_resize() }
}
override def init(): Unit = {
init_state()
PIDE.session.global_options += main
handle_resize()
}
override def exit(): Unit = {
PIDE.session.global_options -= main
delay_resize.revoke()
}
}
diff --git a/src/Tools/jEdit/src/jedit_sessions.scala b/src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala
+++ b/src/Tools/jEdit/src/jedit_sessions.scala
@@ -1,146 +1,138 @@
/* Title: Tools/jEdit/src/jedit_sessions.scala
Author: Makarius
Isabelle/jEdit session information, based on implicit process environment
and explicit options.
*/
package isabelle.jedit
import isabelle._
object JEdit_Sessions {
/* session options */
def session_dirs: List[Path] =
Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-")
def session_no_build: Boolean =
Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"
def session_options(options: Options): Options = {
val options1 =
Isabelle_System.getenv("JEDIT_BUILD_MODE") match {
case "default" => options
case mode => options.bool.update("system_heaps", mode == "system")
}
val options2 =
Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
case "" => options1
case s => options1.string.update("ML_process_policy", s)
}
options2
}
def sessions_structure(
options: Options = PIDE.options.value,
dirs: List[Path] = session_dirs
): Sessions.Structure = {
Sessions.load_structure(session_options(options), dirs = dirs)
}
/* raw logic info */
private val jedit_logic_option = "jedit_logic"
def logic_name(options: Options): String =
Isabelle_System.default_logic(
Isabelle_System.getenv("JEDIT_LOGIC"),
options.string(jedit_logic_option))
def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
def logic_include_sessions: List[String] =
space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
def logic_info(options: Options): Option[Sessions.Info] =
try { sessions_structure(options = options).get(logic_name(options)) }
catch { case ERROR(_) => None }
def logic_root(options: Options): Position.T =
if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none
else Position.none
/* logic selector */
def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = {
GUI_Thread.require {}
- val default_entry =
- GUI.Selector.Item("", description = "default (" + logic_name(options.value) + ")")
+ val sessions = sessions_structure(options = options.value)
+ val all_sessions = sessions.imports_topological_order
+ val main_sessions = all_sessions.filter(name => sessions(name).main_group)
- val session_entries = {
- val sessions = sessions_structure(options = options.value)
- val all_sessions = sessions.imports_topological_order
- val main_sessions = all_sessions.filter(name => sessions(name).main_group)
+ val default_entry =
+ GUI.Selector.item_description("", "default (" + logic_name(options.value) + ")")
- main_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) :::
- all_sessions.sorted.map(GUI.Selector.item(_, batch = 1))
- }
-
- new GUI.Selector(default_entry :: session_entries) with JEdit_Options.Entry {
+ new GUI.Selector[String](
+ default_entry :: main_sessions.map(GUI.Selector.item),
+ all_sessions.sorted.map(GUI.Selector.item)
+ ) 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 {
- case item: GUI.Selector.Item[_] => item.item == logic
- case _ => false
- } match {
- case Some(entry) => selection.item = entry
- case None =>
- }
+ for (entry <- find_value(_ == logic)) selection.item = entry
}
def save(): Unit =
- for (item <- selection.item.get_item) options.string(jedit_logic_option) = item
+ for (logic <- selection_value) options.string(jedit_logic_option) = logic
override def changed(): Unit = if (autosave) save()
load()
}
}
/* session build process */
def session_base_info(options: Options): Sessions.Base_Info =
Sessions.base_info(options,
dirs = JEdit_Sessions.session_dirs,
include_sessions = logic_include_sessions,
session = logic_name(options),
session_ancestor = logic_ancestor,
session_requirements = logic_requirements)
def session_build(
options: Options,
progress: Progress = new Progress,
no_build: Boolean = false
): Int = {
Build.build(session_options(options),
selection = Sessions.Selection.session(PIDE.resources.session_base.session_name),
progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs,
infos = PIDE.resources.session_base_info.infos).rc
}
def session_start(options0: Options): Unit = {
val session = PIDE.session
val options = session_options(options0)
val sessions_structure = PIDE.resources.session_base_info.sessions_structure
val store = Sessions.store(options)
session.phase_changed += PIDE.plugin.session_phase_changed
Isabelle_Process.start(session, options, sessions_structure, store,
logic = PIDE.resources.session_base.session_name,
modes =
(space_explode(',', options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)
}
}
diff --git a/src/Tools/jEdit/src/jedit_spell_checker.scala b/src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala
@@ -1,105 +1,105 @@
/* Title: Tools/jEdit/src/jedit_spell_checker.scala
Author: Makarius
Specific spell-checker support for Isabelle/jEdit.
*/
package isabelle.jedit
import isabelle._
import javax.swing.JMenuItem
import org.gjt.sp.jedit.menu.EnhancedMenuItem
import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
object JEdit_Spell_Checker {
/* completion */
def completion(
rendering: JEdit_Rendering,
explicit: Boolean,
caret: Text.Offset
): Option[Completion.Result] = {
PIDE.plugin.spell_checker.get match {
case Some(spell_checker) if explicit =>
spell_checker.completion(rendering, caret)
case _ => None
}
}
/* context menu */
def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = {
val result =
for {
spell_checker <- PIDE.plugin.spell_checker.get
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
range = JEdit_Lib.point_range(text_area.getBuffer, offset)
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} yield (spell_checker, word)
result match {
case Some((spell_checker, word)) =>
val context = jEdit.getActionContext()
def item(name: String): JMenuItem =
new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
val complete_items =
if (spell_checker.complete(word).nonEmpty) List(item("isabelle.complete-word"))
else Nil
val update_items =
if (spell_checker.check(word))
List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
else
List(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
val reset_items =
spell_checker.reset_enabled() match {
case 0 => Nil
case n =>
val name = "isabelle.reset-words"
val label = context.getAction(name).getLabel
List(new EnhancedMenuItem(label + " (" + n + ")", name, context))
}
complete_items ::: update_items ::: reset_items
case None => Nil
}
}
/* dictionaries */
def dictionaries_selector(): JEdit_Options.Entry = {
GUI_Thread.require {}
val option_name = "spell_checker_dictionary"
val opt = PIDE.options.value.check_name(option_name)
- new GUI.Selector(Spell_Checker.dictionaries.map(GUI.Selector.Item(_))) 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)
Spell_Checker.get_dictionary(lang) match {
- case Some(dict) => selection.item = GUI.Selector.Item(dict)
+ case Some(dict) => selection.item = GUI.Selector.item(dict)
case None =>
}
}
def save(): Unit =
- for (item <- selection.item.get_item) PIDE.options.string(option_name) = item.lang
+ for (dict <- selection_value) PIDE.options.string(option_name) = dict.lang
load()
}
}
}