isabelle: comparison src/Tools/jEdit/src/completion

equal deleted inserted replaced

-:b3ca4a6ed74b
+:87ebf5a50283
 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
+object Completion_Popup {
-{
 /** items with HTML rendering **/
-private class Item(val item: Completion.Item)
+private class Item(val item: Completion.Item) {
-{
 private val html =
 item.description match {
 case a :: bs =>
 "<html><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" +
 HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>"
 /** jEdit text area **/
-object Text_Area
+object Text_Area {
-{
 private val key = new Object
-def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
+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
 }
 text_area_completion.action(immediate = true, explicit = true, word_only = word_only)
 true
 case None => false
 }
-def exit(text_area: JEditTextArea): Unit =
+def exit(text_area: JEditTextArea): Unit = {
-{
 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 =
+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 =
+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)
+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 {
 }
 /* rendering */
-def rendering(rendering: JEdit_Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
+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)) {
 /* syntax completion */
 def syntax_completion(
 history: Completion.History,
 explicit: Boolean,
-opt_rendering: Option[JEdit_Rendering]): Option[Completion.Result] =
+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) =>
 }
 /* completion action: text area */
-private def insert(item: Completion.Item): Unit =
+private def insert(item: Completion.Item): Unit = {
-{
 GUI_Thread.require {}
 val buffer = text_area.getBuffer
 val range = item.range
 if (buffer.isEditable) {
 def action(
 immediate: Boolean = false,
 explicit: Boolean = false,
 delayed: Boolean = false,
-word_only: Boolean = false): Boolean =
+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): Unit =
+def open_popup(result: Completion.Result): Unit = {
-{
 val font =
 painter.getFont.deriveFont(
 Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
 val range = result.range
 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)
+new Completion_Popup(Some(range), layered, loc2, font, items) {
-{
+override def complete(item: Completion.Item): Unit = {
-override def complete(item: Completion.Item): Unit =
-{
 PIDE.plugin.completion_history.update(item)
 insert(item)
 }
-override def propagate(evt: KeyEvent): Unit =
+override def propagate(evt: KeyEvent): Unit = {
-{
 if (view.getKeyEventInterceptor == null)
 JEdit_Lib.propagate_key(view, evt)
 else if (view.getKeyEventInterceptor == inner_key_listener) {
 try {
 view.setKeyEventInterceptor(null)
 if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener)
 }
 }
 if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
 }
-override def shutdown(focus: Boolean): Unit =
+override def shutdown(focus: Boolean): Unit = {
-{
 if (view.getKeyEventInterceptor == inner_key_listener)
 view.setKeyEventInterceptor(null)
 if (focus) text_area.requestFocus()
 JEdit_Lib.invalidate_range(text_area, range)
 }
 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) =
+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 result = {
-{
 val result1 =
 if (word_only) None
 else Completion.Result.merge(history, semantic_completion, result0)
 opt_rendering match {
 case None => result1
 }
 /* input key events */
-def input(evt: KeyEvent): Unit =
+def input(evt: KeyEvent): Unit = {
-{
 GUI_Thread.require {}
 if (!evt.isConsumed) {
 val special = JEdit_Lib.special_key(evt)
 }
 /* dismiss popup */
-def dismissed(): Boolean =
+def dismissed(): Boolean = {
-{
 GUI_Thread.require {}
 completion_popup match {
 case Some(completion) =>
 completion.hide_popup()
 JEdit_Lib.key_listener(key_typed = input)
 private def activate(): Unit =
 text_area.addKeyListener(outer_key_listener)
-private def deactivate(): Unit =
+private def deactivate(): Unit = {
-{
 dismissed()
 text_area.removeKeyListener(outer_key_listener)
 }
 }
 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)
+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)
 private var completion_popup: Option[Completion_Popup] = None
 /* dismiss */
-private def dismissed(): Boolean =
+private def dismissed(): Boolean = {
-{
 completion_popup match {
 case Some(completion) =>
 completion.hide_popup()
 completion_popup = None
 true
 }
 /* insert */
-private def insert(item: Completion.Item): Unit =
+private def insert(item: Completion.Item): Unit = {
-{
 GUI_Thread.require {}
 val range = item.range
 if (text_field.isEditable) {
 val content = text_field.getText
 }
 /* completion action: text field */
-def action(): Unit =
+def action(): Unit = {
-{
 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 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)
+new Completion_Popup(None, layered, loc, text_field.getFont, items) {
-{
+override def complete(item: Completion.Item): Unit = {
-override def complete(item: Completion.Item): Unit =
-{
 PIDE.plugin.completion_history.update(item)
 insert(item)
 }
 override def propagate(evt: KeyEvent): Unit =
 if (!evt.isConsumed) text_field.processKeyEvent(evt)
 }
 /* process key event */
-private def process(evt: KeyEvent): Unit =
+private def process(evt: KeyEvent): Unit = {
-{
 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) {
 private val process_delay =
 Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
 action()
 }
-override def processKeyEvent(evt0: KeyEvent): Unit =
+override def processKeyEvent(evt0: KeyEvent): Unit = {
-{
 val evt = KeyEventWorkaround.processKeyEvent(evt0)
 if (evt != null) {
 evt.getID match {
 case KeyEvent.KEY_PRESSED =>
 val key_code = evt.getKeyCode
 class Completion_Popup private(
 opt_range: Option[Text.Range],
 layered: JLayeredPane,
 location: Point,
 font: Font,
-items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
+items: List[Completion_Popup.Item]
-{
+) extends JPanel(new BorderLayout) {
 completion =>
 GUI_Thread.require {}
 require(items.nonEmpty, "no completion items")
 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 =
+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): Unit =
+private def move_items(n: Int): Unit = {
-{
 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): Unit =
+private def move_pages(n: Int): Unit = {
-{
 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) =>
+key_pressed = (e: KeyEvent) => {
-{
+if (!e.isConsumed) {
-if (!e.isConsumed) {
+e.getKeyCode match {
-e.getKeyCode match {
+case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
-case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
+if (complete_selected()) e.consume
-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()
-case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
+}
-if (complete_selected()) e.consume
+}
-hide_popup()
+propagate(e)
-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): Unit =
+override def mouseClicked(e: MouseEvent): Unit = {
-{
 if (complete_selected()) e.consume
 hide_popup()
 }
 })
 /* popup */
 def active_range: Option[Text.Range] =
 if (isDisplayable) opt_range else None
-private val popup =
+private val popup = {
-{
 val screen = GUI.screen_location(layered, location)
-val size =
+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): Unit =
+private def show_popup(focus: Boolean): Unit = {
-{
 popup.show
 if (focus) list_view.requestFocus()
 }
-private def hide_popup(): Unit =
+private def hide_popup(): Unit = {
-{
 shutdown(list_view.peer.isFocusOwner)
 popup.hide
 }
 }

changeset 75393	87ebf5a50283
parent 73367	77ef8bef0593
child 75394	42267c650205