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,443 @@ /* 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] = + def get_value: Option[A] = this match { - case item: Item[_] => Some(item.item) + 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 + case class Item[A](value: A, description: String = "", batch: Int = 0) 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 + "" } 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() } } /* 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(_)) ) { 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)) 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/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,146 @@ /* 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 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) 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 { 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 item: GUI.Selector.Item[_] => item.value == logic case _ => false } match { case Some(entry) => selection.item = entry case None => } } def save(): Unit = - for (item <- selection.item.get_item) options.string(jedit_logic_option) = item + for (item <- selection.item.get_value) options.string(jedit_logic_option) = item 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 { 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 None => } } def save(): Unit = - for (item <- selection.item.get_item) PIDE.options.string(option_name) = item.lang + for (item <- selection.item.get_value) PIDE.options.string(option_name) = item.lang load() } } }