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,440 +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_value: Option[A] = - this match { + object Value { + def unapply[A](entry: Entry[A]): Option[A] = + entry match { case item: Item[_] => Some(item.value) case _ => None } } - case class Item[A](value: A, description: String = "", batch: Int = 0) extends Entry[A] { + sealed abstract class Entry[A] { def get_value: Option[A] = Value.unapply(this) } + 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](batch: Int = 0) extends Entry[A] { + 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) + def item[A](value: A): Entry[A] = Item(value, "", 0) + def item_description[A](value: A, description: String): Entry[A] = Item(value, description, 0) + + def make_entries[A](batches: List[List[Entry[A]]]): List[Entry[A]] = { + val item_batches: List[List[Item[A]]] = + 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 renderer = (list: ListView[_ <: Selector.Entry[A]], selected: Boolean, focus: Boolean, entry: Selector.Entry[A], i: Int) => { entry match { 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.value == 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_value) 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_value) PIDE.options.string(option_name) = item.lang + for (dict <- selection_value) PIDE.options.string(option_name) = dict.lang load() } } }