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,272 +1,311 @@ /* Title: Pure/GUI/gui.scala Author: Makarius Basic GUI tools (for AWT/Swing). */ package isabelle -import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException} -import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager} -import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics} +import java.awt.{Component, Container, Font, Image, KeyboardFocusManager, Window, Point, + Rectangle, Dimension, GraphicsEnvironment, MouseInfo} +import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute} import java.awt.geom.AffineTransform -import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog, - JButton, JTextField, JLabel} - - -import scala.collection.JavaConverters -import scala.swing.{ComboBox, TextArea, ScrollPane} +import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane, + JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities} +import scala.swing.{ComboBox, ScrollPane, TextArea} import scala.swing.event.SelectionChanged object GUI { /* Swing look-and-feel */ def find_laf(name: String): Option[String] = UIManager.getInstalledLookAndFeels(). find(c => c.getName == name || c.getClassName == name). map(_.getClassName) def get_laf(): String = find_laf(System.getProperty("isabelle.laf")) getOrElse { if (Platform.is_windows || Platform.is_macos) UIManager.getSystemLookAndFeelClassName() else UIManager.getCrossPlatformLookAndFeelClassName() } def init_laf(): Unit = UIManager.setLookAndFeel(get_laf()) def is_macos_laf(): Boolean = Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName def is_windows_laf(): Boolean = Platform.is_windows && UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName /* plain focus traversal, notably for text fields */ def plain_focus_traversal(component: Component) { 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]) { 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) } /* zoom box */ private val Zoom_Factor = "([0-9]+)%?".r abstract class Zoom_Box extends ComboBox[String]( List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) { def changed: Unit def factor: Int = parse(selection.item) private def parse(text: String): Int = 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) { peer.getEditor match { case null => case editor => editor.setItem(print(i)) } } makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x)) peer.getEditor.getEditorComponent match { case text: JTextField => text.setColumns(4) case _ => } selection.index = 3 listenTo(selection) reactions += { case SelectionChanged(_) => changed } } /* 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) + + /* 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) { def traverse(comp: Component) { 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(java.util.Map.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() { 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)) } } } diff --git a/src/Tools/jEdit/src/completion_popup.scala b/src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala +++ b/src/Tools/jEdit/src/completion_popup.scala @@ -1,711 +1,711 @@ /* Title: Tools/jEdit/src/completion_popup.scala Author: Makarius Completion popup. */ package isabelle.jedit import isabelle._ import java.awt.{Color, Font, Point, BorderLayout, Dimension} import java.awt.event.{KeyEvent, KeyListener, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} import java.io.{File => JFile} import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities} import javax.swing.border.LineBorder import javax.swing.text.DefaultCaret import scala.swing.{ListView, ScrollPane} import scala.swing.event.MouseClicked import org.gjt.sp.jedit.View import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection} import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround} import org.gjt.sp.util.StandardUtilities object Completion_Popup { /** items with HTML rendering **/ private class Item(val item: Completion.Item) { private val html = item.description match { case a :: bs => "" + HTML.output(Symbol.print_newlines(a)) + "" + HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "" case Nil => "" } override def toString: String = html } /** jEdit text area **/ object Text_Area { private val key = new Object def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] = { GUI_Thread.require {} text_area.getClientProperty(key) match { case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion) case _ => None } } def active_range(text_area: TextArea): Option[Text.Range] = apply(text_area) match { case Some(text_area_completion) => text_area_completion.active_range case None => None } def action(text_area: TextArea, word_only: Boolean): Boolean = apply(text_area) match { case Some(text_area_completion) => if (text_area_completion.active_range.isDefined) text_area_completion.action(word_only = word_only) else text_area_completion.action(immediate = true, explicit = true, word_only = word_only) true case None => false } def exit(text_area: JEditTextArea) { GUI_Thread.require {} apply(text_area) match { case None => case Some(text_area_completion) => text_area_completion.deactivate() text_area.putClientProperty(key, null) } } def init(text_area: JEditTextArea): Completion_Popup.Text_Area = { exit(text_area) val text_area_completion = new Text_Area(text_area) text_area.putClientProperty(key, text_area_completion) text_area_completion.activate() text_area_completion } def dismissed(text_area: TextArea): Boolean = { GUI_Thread.require {} apply(text_area) match { case Some(text_area_completion) => text_area_completion.dismissed() case None => false } } } class Text_Area private(text_area: JEditTextArea) { // owned by GUI thread private var completion_popup: Option[Completion_Popup] = None def active_range: Option[Text.Range] = completion_popup match { case Some(completion) => completion.active_range case None => None } /* rendering */ def rendering(rendering: JEdit_Rendering, line_range: Text.Range): Option[Text.Info[Color]] = { active_range match { case Some(range) => range.try_restrict(line_range) case None => val caret = text_area.getCaretPosition if (line_range.contains(caret)) { rendering.before_caret_range(caret).try_restrict(line_range) match { case Some(range) if !range.is_singularity => val range0 = Completion.Result.merge(Completion.History.empty, syntax_completion(Completion.History.empty, true, Some(rendering)), rendering.path_completion(caret), Document_Model.bibtex_completion(Completion.History.empty, rendering, caret)) .map(_.range) rendering.semantic_completion(range0, range) match { case None => range0 case Some(Text.Info(_, Completion.No_Completion)) => None case Some(Text.Info(range1, _: Completion.Names)) => Some(range1) } case _ => None } } else None } }.map(range => Text.Info(range, rendering.completion_color)) /* syntax completion */ def syntax_completion( history: Completion.History, explicit: Boolean, opt_rendering: Option[JEdit_Rendering]): Option[Completion.Result] = { val buffer = text_area.getBuffer val unicode = Isabelle_Encoding.is_active(buffer) Isabelle.buffer_syntax(buffer) match { case Some(syntax) => val context = (for { rendering <- opt_rendering if PIDE.options.bool("jedit_completion_context") caret_range = rendering.before_caret_range(text_area.getCaretPosition) context <- rendering.language_context(caret_range) } yield context) getOrElse syntax.language_context val caret = text_area.getCaretPosition val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine) val line_start = line_range.start for { line_text <- JEdit_Lib.get_text(buffer, line_range) result <- syntax.complete( history, unicode, explicit, line_start, line_text, caret - line_start, context) } yield result case None => None } } /* completion action: text area */ private def insert(item: Completion.Item) { GUI_Thread.require {} val buffer = text_area.getBuffer val range = item.range if (buffer.isEditable) { JEdit_Lib.buffer_edit(buffer) { JEdit_Lib.get_text(buffer, range) match { case Some(text) if text == item.original => text_area.getSelectionAtOffset(text_area.getCaretPosition) match { /*rectangular selection as "tall caret"*/ case selection : Selection.Rect if selection.getStart(buffer, text_area.getCaretLine) == range.stop => text_area.moveCaretPosition(range.stop) (0 until Character.codePointCount(item.original, 0, item.original.length)) .foreach(_ => text_area.backspace()) text_area.setSelectedText(selection, item.replacement) text_area.moveCaretPosition(text_area.getCaretPosition + item.move) /*other selections: rectangular, multiple range, ...*/ case selection if selection != null && selection.getStart(buffer, text_area.getCaretLine) == range.start && selection.getEnd(buffer, text_area.getCaretLine) == range.stop => text_area.moveCaretPosition(range.stop + item.move) text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement)) /*no selection*/ case _ => buffer.remove(range.start, range.length) buffer.insert(range.start, item.replacement) text_area.moveCaretPosition(range.start + item.replacement.length + item.move) Isabelle.indent_input(text_area) } case _ => } } } } def action( immediate: Boolean = false, explicit: Boolean = false, delayed: Boolean = false, word_only: Boolean = false): Boolean = { val view = text_area.getView val layered = view.getLayeredPane val buffer = text_area.getBuffer val painter = text_area.getPainter val history = PIDE.plugin.completion_history.value val unicode = Isabelle_Encoding.is_active(buffer) def open_popup(result: Completion.Result) { val font = painter.getFont.deriveFont( Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale"))) val range = result.range val loc1 = text_area.offsetToXY(range.start) if (loc1 != null) { val loc2 = SwingUtilities.convertPoint(painter, loc1.x, loc1.y + painter.getLineHeight, layered) val items = result.items.map(new Item(_)) val completion = new Completion_Popup(Some(range), layered, loc2, font, items) { override def complete(item: Completion.Item) { PIDE.plugin.completion_history.update(item) insert(item) } override def propagate(evt: KeyEvent) { if (view.getKeyEventInterceptor == null) JEdit_Lib.propagate_key(view, evt) else if (view.getKeyEventInterceptor == inner_key_listener) { try { view.setKeyEventInterceptor(null) JEdit_Lib.propagate_key(view, evt) } finally { if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener) } } if (evt.getID == KeyEvent.KEY_TYPED) input(evt) } override def shutdown(focus: Boolean) { if (view.getKeyEventInterceptor == inner_key_listener) view.setKeyEventInterceptor(null) if (focus) text_area.requestFocus JEdit_Lib.invalidate_range(text_area, range) } } dismissed() completion_popup = Some(completion) view.setKeyEventInterceptor(completion.inner_key_listener) JEdit_Lib.invalidate_range(text_area, range) Pretty_Tooltip.dismissed_all() completion.show_popup(false) } } if (buffer.isEditable) { val caret = text_area.getCaretPosition val opt_rendering = Document_View.get(text_area).map(_.get_rendering()) val result0 = syntax_completion(history, explicit, opt_rendering) val (no_completion, semantic_completion) = { opt_rendering match { case Some(rendering) => rendering.semantic_completion_result(history, unicode, result0.map(_.range), rendering.before_caret_range(caret)) case None => (false, None) } } if (no_completion) false else { val result = { val result1 = if (word_only) None else Completion.Result.merge(history, semantic_completion, result0) opt_rendering match { case None => result1 case Some(rendering) => Completion.Result.merge(history, result1, JEdit_Spell_Checker.completion(rendering, explicit, caret), rendering.path_completion(caret), Document_Model.bibtex_completion(history, rendering, caret)) } } result match { case Some(result) => result.items match { case List(item) if result.unique && item.immediate && immediate => insert(item) true case _ :: _ if !delayed => open_popup(result) false case _ => false } case None => false } } } else false } /* input key events */ def input(evt: KeyEvent) { GUI_Thread.require {} if (!evt.isConsumed) { val special = JEdit_Lib.special_key(evt) if (PIDE.options.bool("jedit_completion")) { dismissed() if (evt.getKeyChar != '\b') { val immediate = PIDE.options.bool("jedit_completion_immediate") if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { input_delay.revoke() action(immediate = immediate) } else { if (!special && action(immediate = immediate, delayed = true)) input_delay.revoke() else input_delay.invoke() } } } val selection = text_area.getSelection() if (!special && (selection == null || selection.isEmpty)) Isabelle.indent_input(text_area) } } private val input_delay = Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) { action() } /* dismiss popup */ def dismissed(): Boolean = { GUI_Thread.require {} completion_popup match { case Some(completion) => completion.hide_popup() completion_popup = None true case None => false } } /* activation */ private val outer_key_listener = JEdit_Lib.key_listener(key_typed = input) private def activate() { text_area.addKeyListener(outer_key_listener) } private def deactivate() { dismissed() text_area.removeKeyListener(outer_key_listener) } } /** history text field **/ class History_Text_Field( name: String = null, instant_popups: Boolean = false, enter_adds_to_history: Boolean = true, syntax: Outer_Syntax = Outer_Syntax.empty) extends HistoryTextField(name, instant_popups, enter_adds_to_history) { text_field => // see https://forums.oracle.com/thread/1361677 if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret) // owned by GUI thread private var completion_popup: Option[Completion_Popup] = None /* dismiss */ private def dismissed(): Boolean = { completion_popup match { case Some(completion) => completion.hide_popup() completion_popup = None true case None => false } } /* insert */ private def insert(item: Completion.Item) { GUI_Thread.require {} val range = item.range if (text_field.isEditable) { val content = text_field.getText range.try_substring(content) match { case Some(text) if text == item.original => text_field.setText( content.substring(0, range.start) + item.replacement + content.substring(range.stop)) text_field.getCaret.setDot(range.start + item.replacement.length + item.move) case _ => } } } /* completion action: text field */ def action() { GUI.layered_pane(text_field) match { case Some(layered) if text_field.isEditable => val history = PIDE.plugin.completion_history.value val caret = text_field.getCaret.getDot val text = text_field.getText val context = syntax.language_context syntax.complete(history, true, false, 0, text, caret, context) match { case Some(result) => val fm = text_field.getFontMetrics(text_field.getFont) val loc = SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered) val items = result.items.map(new Item(_)) val completion = new Completion_Popup(None, layered, loc, text_field.getFont, items) { override def complete(item: Completion.Item) { PIDE.plugin.completion_history.update(item) insert(item) } override def propagate(evt: KeyEvent) { if (!evt.isConsumed) text_field.processKeyEvent(evt) } override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus } } dismissed() completion_popup = Some(completion) completion.show_popup(true) case None => } case _ => } } /* process key event */ private def process(evt: KeyEvent) { if (PIDE.options.bool("jedit_completion")) { dismissed() if (evt.getKeyChar != '\b') { val special = JEdit_Lib.special_key(evt) if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { process_delay.revoke() action() } else process_delay.invoke() } } } private val process_delay = Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) { action() } override def processKeyEvent(evt0: KeyEvent) { val evt = KeyEventWorkaround.processKeyEvent(evt0) if (evt != null) { evt.getID match { case KeyEvent.KEY_PRESSED => val key_code = evt.getKeyCode if (key_code == KeyEvent.VK_ESCAPE) { if (dismissed()) evt.consume } case KeyEvent.KEY_TYPED => super.processKeyEvent(evt) process(evt) evt.consume case _ => } if (!evt.isConsumed) super.processKeyEvent(evt) } } } } class Completion_Popup private( opt_range: Option[Text.Range], layered: JLayeredPane, location: Point, font: Font, items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout) { completion => GUI_Thread.require {} require(items.nonEmpty) val multi: Boolean = items.length > 1 /* actions */ def complete(item: Completion.Item) { } def propagate(evt: KeyEvent) { } def shutdown(focus: Boolean) { } /* list view */ private val list_view = new ListView(items) list_view.font = font list_view.selection.intervalMode = ListView.IntervalMode.Single list_view.peer.setFocusTraversalKeysEnabled(false) list_view.peer.setVisibleRowCount(items.length min 8) list_view.peer.setSelectedIndex(0) for (cond <- List(JComponent.WHEN_FOCUSED, JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null) private def complete_selected(): Boolean = { list_view.selection.items.toList match { case item :: _ => complete(item.item); true case _ => false } } private def move_items(n: Int) { val i = list_view.peer.getSelectedIndex val j = ((i + n) min (items.length - 1)) max 0 if (i != j) { list_view.peer.setSelectedIndex(j) list_view.peer.ensureIndexIsVisible(j) } } private def move_pages(n: Int) { val page_size = list_view.peer.getVisibleRowCount - 1 move_items(page_size * n) } /* event handling */ val inner_key_listener: KeyListener = JEdit_Lib.key_listener( key_pressed = (e: KeyEvent) => { if (!e.isConsumed) { e.getKeyCode match { case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") => if (complete_selected()) e.consume hide_popup() case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") => if (complete_selected()) e.consume hide_popup() case KeyEvent.VK_ESCAPE => hide_popup() e.consume case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi => move_items(-1) e.consume case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi => move_items(1) e.consume case KeyEvent.VK_PAGE_UP if multi => move_pages(-1) e.consume case KeyEvent.VK_PAGE_DOWN if multi => move_pages(1) e.consume case _ => if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) hide_popup() } } propagate(e) }, key_typed = propagate ) list_view.peer.addKeyListener(inner_key_listener) list_view.peer.addMouseListener(new MouseAdapter { override def mouseClicked(e: MouseEvent) { if (complete_selected()) e.consume hide_popup() } }) list_view.peer.addFocusListener(new FocusAdapter { override def focusLost(e: FocusEvent) { hide_popup() } }) /* main content */ override def getFocusTraversalKeysEnabled = false completion.setBorder(new LineBorder(Color.BLACK)) completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent]) /* popup */ def active_range: Option[Text.Range] = if (isDisplayable) opt_range else None private val popup = { - val screen = JEdit_Lib.screen_location(layered, location) + val screen = GUI.screen_location(layered, location) val size = { val geometry = JEdit_Lib.window_geometry(completion, completion) val bounds = JEdit_Rendering.popup_bounds val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight new Dimension(w, h) } new Popup(layered, completion, screen.relative(layered, size), size) } private def show_popup(focus: Boolean) { popup.show if (focus) list_view.requestFocus } private def hide_popup() { shutdown(list_view.peer.isFocusOwner) popup.hide } } diff --git a/src/Tools/jEdit/src/jedit_lib.scala b/src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala +++ b/src/Tools/jEdit/src/jedit_lib.scala @@ -1,409 +1,370 @@ /* Title: Tools/jEdit/src/jedit_lib.scala Author: Makarius Misc library functions for jEdit. */ package isabelle.jedit import isabelle._ import java.io.{File => JFile} import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit} import java.awt.event.{InputEvent, KeyEvent, KeyListener} import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} import scala.util.parsing.input.CharSequenceReader import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane} import org.gjt.sp.jedit.io.{FileVFS, VFSManager} import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator} import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager} import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} object JEdit_Lib { /* jEdit directories */ def directories: List[JFile] = (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_)) - /* 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) - 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) - } - - /* window geometry measurement */ private lazy val dummy_window = new JWindow final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int) { def deco_width: Int = width - inner_width def deco_height: Int = height - inner_height } def window_geometry(outer: Container, inner: Component): Window_Geometry = { GUI_Thread.require {} val old_content = dummy_window.getContentPane dummy_window.setContentPane(outer) dummy_window.pack dummy_window.revalidate val geometry = Window_Geometry( dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight) dummy_window.setContentPane(old_content) geometry } /* files */ def is_file(name: String): Boolean = VFSManager.getVFSForPath(name).isInstanceOf[FileVFS] def check_file(name: String): Option[JFile] = if (is_file(name)) Some(new JFile(name)) else None /* buffers */ def buffer_text(buffer: JEditBuffer): String = buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } def buffer_reader(buffer: JEditBuffer): CharSequenceReader = Scan.char_reader(buffer.getSegment(0, buffer.getLength)) def buffer_mode(buffer: JEditBuffer): String = { val mode = buffer.getMode if (mode == null) "" else { val name = mode.getName if (name == null) "" else name } } def buffer_line_manager(buffer: JEditBuffer): LineManager = Untyped.get[LineManager](buffer, "lineMgr") def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer)) def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A = { val undo_in_progress = buffer.isUndoInProgress def set(b: Boolean) { Untyped.set[Boolean](buffer, "undoInProgress", b) } try { set(true); body } finally { set(undo_in_progress) } } /* main jEdit components */ def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator def jedit_buffer(name: String): Option[Buffer] = jedit_buffers().find(buffer => buffer_name(buffer) == name) def jedit_buffer(name: Document.Node.Name): Option[Buffer] = jedit_buffer(name.node) def jedit_views(): Iterator[View] = jEdit.getViews().iterator def jedit_view(view: View = null): View = if (view == null) jEdit.getActiveView() else view def jedit_edit_panes(view: View): Iterator[EditPane] = if (view == null) Iterator.empty else view.getEditPanes().iterator.filter(_ != null) def jedit_text_areas(view: View): Iterator[JEditTextArea] = if (view == null) Iterator.empty else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null) def jedit_text_areas(): Iterator[JEditTextArea] = jedit_views().flatMap(jedit_text_areas) def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = jedit_text_areas().filter(_.getBuffer == buffer) def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.readLock(); body } finally { buffer.readUnlock() } } def buffer_edit[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.beginCompoundEdit(); body } finally { buffer.endCompoundEdit() } } /* get text */ def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = try { Some(buffer.getText(range.start, range.length)) } catch { case _: ArrayIndexOutOfBoundsException => None } /* point range */ def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range = if (offset < 0) Text.Range.offside else buffer_lock(buffer) { def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) try { val c = text(offset) if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) Text.Range(offset, offset + 2) else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1))) Text.Range(offset - 1, offset + 1) else Text.Range(offset, offset + 1) } catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } } /* text ranges */ def buffer_range(buffer: JEditBuffer): Text.Range = Text.Range(0, buffer.getLength) def line_range(buffer: JEditBuffer, line: Int): Text.Range = Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength) def caret_range(text_area: TextArea): Text.Range = point_range(text_area.getBuffer, text_area.getCaretPosition) def visible_range(text_area: TextArea): Option[Text.Range] = { val buffer = text_area.getBuffer val n = text_area.getVisibleLines if (n > 0) { val start = text_area.getScreenLineStartOffset(0) val raw_end = text_area.getScreenLineEndOffset(n - 1) val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength Some(Text.Range(start, end)) } else None } def invalidate_range(text_area: TextArea, range: Text.Range) { val buffer = text_area.getBuffer buffer_range(buffer).try_restrict(range) match { case Some(range1) if !range1.is_singularity => try { text_area.invalidateLineRange( buffer.getLineOfOffset(range1.start), buffer.getLineOfOffset(range1.stop)) } catch { case _: ArrayIndexOutOfBoundsException => } case _ => } } def invalidate(text_area: TextArea) { val visible_lines = text_area.getVisibleLines if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines) } /* graphics range */ case class Gfx_Range(x: Int, y: Int, length: Int) // NB: jEdit always normalizes \r\n and \r to \n // NB: last line lacks \n def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = { val metric = pretty_metric(text_area.getPainter) val char_width = (metric.unit * metric.average).round.toInt val buffer = text_area.getBuffer val end = buffer.getLength val stop = range.stop val (p, q, r) = try { val p = text_area.offsetToXY(range.start) val (q, r) = if (get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n")) (text_area.offsetToXY(stop - 1), char_width) else if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end)) else (text_area.offsetToXY(stop), 0) (p, q, r) } catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } if (p != null && q != null && p.x < q.x + r && p.y == q.y) Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) else None } /* pixel range */ def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] = { // coordinates wrt. inner painter component val painter = text_area.getPainter if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) { val offset = text_area.xyToOffset(x, y, false) if (offset >= 0) { val range = point_range(text_area.getBuffer, offset) gfx_range(text_area, range) match { case Some(g) if g.x <= x && x < g.x + g.length => Some(range) case _ => None } } else None } else None } /* pretty text metric */ abstract class Pretty_Metric extends Pretty.Metric { def average: Double } def pretty_metric(painter: TextAreaPainter): Pretty_Metric = new Pretty_Metric { def string_width(s: String): Double = painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth val unit: Double = string_width(Symbol.space) max 1.0 val average: Double = string_width("mix") / (3 * unit) def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit } /* icons */ def load_icon(name: String): Icon = { val name1 = if (name.startsWith("idea-icons/")) { val file = Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar").file.toURI.toASCIIString "jar:" + file + "!/" + name } else name val icon = GUIUtilities.loadIcon(name1) if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name) else icon } def load_image_icon(name: String): ImageIcon = load_icon(name) match { case icon: ImageIcon => icon case _ => error("Bad image icon: " + name) } /* key event handling */ def request_focus_view(alt_view: View = null) { isabelle.jedit_base.JEdit_Lib.request_focus_view(alt_view) } def propagate_key(view: View, evt: KeyEvent) { if (view != null && !evt.isConsumed) view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false) } def key_listener( key_typed: KeyEvent => Unit = _ => (), key_pressed: KeyEvent => Unit = _ => (), key_released: KeyEvent => Unit = _ => ()): KeyListener = { def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit) { val evt = KeyEventWorkaround.processKeyEvent(evt0) if (evt != null) handle(evt) } new KeyListener { def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) } def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) } def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) } } } def special_key(evt: KeyEvent): Boolean = { // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java val mod = evt.getModifiersEx (mod & InputEvent.CTRL_DOWN_MASK) != 0 && (mod & InputEvent.ALT_DOWN_MASK) == 0 || (mod & InputEvent.CTRL_DOWN_MASK) == 0 && (mod & InputEvent.ALT_DOWN_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED || (mod & InputEvent.META_DOWN_MASK) != 0 } def command_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 def shift_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0 def modifier_string(evt: InputEvent): String = KeyEventTranslator.getModifierString(evt) match { case null => "" case s => s } } diff --git a/src/Tools/jEdit/src/pretty_tooltip.scala b/src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala +++ b/src/Tools/jEdit/src/pretty_tooltip.scala @@ -1,290 +1,290 @@ /* Title: Tools/jEdit/src/pretty_tooltip.scala Author: Makarius Tooltip based on Pretty_Text_Area. */ package isabelle.jedit import isabelle._ import java.awt.{Color, Point, BorderLayout, Dimension} import java.awt.event.{FocusAdapter, FocusEvent} import javax.swing.{JPanel, JComponent, SwingUtilities, JLayeredPane} import javax.swing.border.LineBorder import scala.swing.{FlowPanel, Label} import scala.swing.event.MouseClicked import org.gjt.sp.jedit.View import org.gjt.sp.jedit.textarea.TextArea object Pretty_Tooltip { /* tooltip hierarchy */ // owned by GUI thread private var stack: List[Pretty_Tooltip] = Nil private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] = { GUI_Thread.require {} if (stack.contains(tip)) Some(stack.span(_ != tip)) else None } private def descendant(parent: JComponent): Option[Pretty_Tooltip] = GUI_Thread.require { stack.find(tip => tip.original_parent == parent) } def apply( view: View, parent: JComponent, location: Point, rendering: JEdit_Rendering, results: Command.Results, info: Text.Info[XML.Body]) { GUI_Thread.require {} stack match { case top :: _ if top.results == results && top.info == info => case _ => GUI.layered_pane(parent) match { case None => case Some(layered) => val (old, rest) = GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match { case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) case None => (stack, Nil) } 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 } } } /* pending event and active state */ // owned by GUI thread private var pending: Option[() => Unit] = None private var active = true private val pending_delay = Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) { pending match { case Some(body) => pending = None; body() case None => } } def invoke(body: () => Unit): Unit = GUI_Thread.require { if (active) { pending = Some(body) pending_delay.invoke() } } def revoke(): Unit = GUI_Thread.require { pending = None pending_delay.revoke() } private lazy val reactivate_delay = Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) { active = true } private def deactivate(): Unit = GUI_Thread.require { revoke() active = false reactivate_delay.invoke() } /* dismiss */ private lazy val focus_delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { dismiss_unfocused() } def dismiss_unfocused() { stack.span(tip => !tip.pretty_text_area.isFocusOwner) match { case (Nil, _) => case (unfocused, rest) => deactivate() unfocused.foreach(_.hide_popup) stack = rest } } def dismiss(tip: Pretty_Tooltip) { deactivate() hierarchy(tip) match { case Some((old, _ :: rest)) => rest match { case top :: _ => top.request_focus case Nil => JEdit_Lib.request_focus_view() } old.foreach(_.hide_popup) tip.hide_popup stack = rest case _ => } } def dismiss_descendant(parent: JComponent): Unit = descendant(parent).foreach(dismiss) def dismissed_all(): Boolean = { deactivate() if (stack.isEmpty) false else { JEdit_Lib.request_focus_view() stack.foreach(_.hide_popup) stack = Nil true } } } class Pretty_Tooltip private( view: View, layered: JLayeredPane, val original_parent: JComponent, location: Point, rendering: JEdit_Rendering, private val results: Command.Results, private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout) { tip => GUI_Thread.require {} /* controls */ private val close = new Label { icon = rendering.tooltip_close_icon tooltip = "Close tooltip window" listenTo(mouse.clicks) reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) } } private val detach = new Label { icon = rendering.tooltip_detach_icon tooltip = "Detach tooltip window" listenTo(mouse.clicks) reactions += { case _: MouseClicked => Info_Dockable(view, rendering.snapshot, results, info.info) Pretty_Tooltip.dismiss(tip) } } private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) { background = rendering.tooltip_color } /* text area */ 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) } pretty_text_area.addFocusListener(new FocusAdapter { override def focusGained(e: FocusEvent) { tip_border(true) Pretty_Tooltip.focus_delay.invoke() } override def focusLost(e: FocusEvent) { tip_border(false) Pretty_Tooltip.focus_delay.invoke() } }) pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale"))) /* main content */ def tip_border(has_focus: Boolean) { tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY)) tip.repaint() } tip_border(true) override def getFocusTraversalKeysEnabled = false tip.setBackground(rendering.tooltip_color) tip.add(controls.peer, BorderLayout.NORTH) tip.add(pretty_text_area) /* popup */ private val popup = { - val screen = JEdit_Lib.screen_location(layered, location) + val screen = GUI.screen_location(layered, location) val size = { val bounds = JEdit_Rendering.popup_bounds val w_max = layered.getWidth min (screen.bounds.width * bounds).toInt val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt val painter = pretty_text_area.getPainter val geometry = JEdit_Lib.window_geometry(tip, painter) val metric = JEdit_Lib.pretty_metric(painter) val margin = ((rendering.tooltip_margin * metric.average) min ((w_max - geometry.deco_width) / metric.unit).toInt) max 20 val formatted = Pretty.formatted(info.info, margin = margin, metric = metric) val lines = XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)( (n: Int, s: String) => n + s.iterator.count(_ == '\n')) val h = painter.getLineHeight * lines + geometry.deco_height val margin1 = if (h <= h_max) (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) }) else margin val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width new Dimension(w min w_max, h min h_max) } new Popup(layered, tip, screen.relative(layered, size), size) } private def show_popup { popup.show pretty_text_area.requestFocus pretty_text_area.update(rendering.snapshot, results, info.info) } private def hide_popup: Unit = popup.hide private def request_focus: Unit = pretty_text_area.requestFocus }