# HG changeset patch # User wenzelm # Date 1377772713 -7200 # Node ID 1760c01f1c7894f542e40825c790d88655fe6318 # Parent 473ea1ed7503b80f4e8e40e229c0a10ba5e58e44 maintain Completion_Popup.Text_Area as client property like Document_View; global Completion_Popup.Text_Area init/exit like SideKickPlugin; eliminated old SideKick completion -- cover all Isabelle modes uniformly; dynamic lookup of Isabelle.mode_syntax -- NB: buffer mode might be undefined in intermediate stages; diff -r 473ea1ed7503 -r 1760c01f1c78 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Thu Aug 29 10:24:43 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Thu Aug 29 12:38:33 2013 +0200 @@ -32,11 +32,45 @@ object Text_Area { - def apply(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax]): Text_Area = - new Text_Area(text_area, get_syntax) + private val key = new Object + + def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] = + text_area.getClientProperty(key) match { + case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion) + case _ => None + } + + def exit(text_area: JEditTextArea) + { + Swing_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: JEditTextArea): Boolean = + { + Swing_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, get_syntax: => Option[Outer_Syntax]) + class Text_Area private(text_area: JEditTextArea) { /* popup state */ @@ -106,7 +140,7 @@ val painter = text_area.getPainter if (buffer.isEditable) { - get_syntax match { + Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { case Some(syntax) => val caret = text_area.getCaretPosition val result = @@ -155,6 +189,23 @@ } } } + + + /* 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) + } } } @@ -214,7 +265,7 @@ /* event handling */ - private val key_listener = + private val inner_key_listener = JEdit_Lib.key_listener( key_pressed = (e: KeyEvent) => { @@ -240,7 +291,7 @@ key_typed = propagate _ ) - list_view.peer.addKeyListener(key_listener) + list_view.peer.addKeyListener(inner_key_listener) list_view.peer.addMouseListener(new MouseAdapter { override def mouseClicked(e: MouseEvent) { diff -r 473ea1ed7503 -r 1760c01f1c78 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Thu Aug 29 10:24:43 2013 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Thu Aug 29 12:38:33 2013 +0200 @@ -149,19 +149,13 @@ /* key listener */ - private val completion_popup = - Completion_Popup.Text_Area(text_area, PIDE.get_recent_syntax) - - def dismissed_popups(): Boolean = completion_popup.dismissed() - private val key_listener = JEdit_Lib.key_listener( key_pressed = (evt: KeyEvent) => { if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView)) evt.consume - }, - key_typed = completion_popup.input _ + } ) diff -r 473ea1ed7503 -r 1760c01f1c78 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 10:24:43 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 12:38:33 2013 +0200 @@ -16,6 +16,20 @@ object Isabelle { + /* editor modes */ + + val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news") + + def mode_syntax(name: String): Option[Outer_Syntax] = + name match { + case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax + case "isabelle-options" => Some(Options.options_syntax) + case "isabelle-root" => Some(Build.root_syntax) + case "isabelle-news" => Some(Outer_Syntax.empty) + case _ => None + } + + /* dockable windows */ private def wm(view: View): DockableWindowManager = view.getDockableWindowManager diff -r 473ea1ed7503 -r 1760c01f1c78 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 29 10:24:43 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 29 12:38:33 2013 +0200 @@ -10,18 +10,12 @@ import isabelle._ -import scala.collection.Set -import scala.collection.immutable.TreeSet -import scala.util.matching.Regex - -import java.awt.Component import javax.swing.tree.DefaultMutableTreeNode import javax.swing.text.Position -import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList} +import javax.swing.Icon -import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} -import errorlist.DefaultErrorSource -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} +import org.gjt.sp.jedit.Buffer +import sidekick.{SideKickParser, SideKickParsedData, IAsset} object Isabelle_Sidekick @@ -58,9 +52,11 @@ } -class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax]) - extends SideKickParser(name) +class Isabelle_Sidekick(name: String) extends SideKickParser(name) { + override def supportsCompletion = false + + /* parsing */ @volatile protected var stopped = false @@ -68,7 +64,7 @@ def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false - def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = + def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { stopped = false @@ -77,7 +73,7 @@ val root = data.root data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength)) - val syntax = get_syntax + val syntax = Isabelle.mode_syntax(name) val ok = if (syntax.isDefined) { val ok = parser(buffer, syntax.get, data) @@ -89,65 +85,13 @@ data } - - - /* completion */ - - override def supportsCompletion = true - override def canCompleteAnywhere = true - - override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion = - { - Swing_Thread.assert() - - val buffer = pane.getBuffer - JEdit_Lib.buffer_lock(buffer) { - get_syntax match { - case None => null - case Some(syntax) => - val line = buffer.getLineOfOffset(caret) - val start = buffer.getLineStartOffset(line) - val text = buffer.getSegment(start, caret - start) - - syntax.completion.complete(text) match { - case None => null - case Some((word, cs)) => - val ds = - (if (Isabelle_Encoding.is_active(buffer)) - cs.map(Symbol.decode(_)).sorted - else cs).filter(_ != word) - if (ds.isEmpty) null - else - new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { - override def getRenderer() = - new ListCellRenderer[Any] { - val default_renderer = - (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]] - - override def getListCellRendererComponent( - list: JList[_ <: Any], value: Any, index: Int, - selected: Boolean, focus: Boolean): Component = - { - val renderer: Component = - default_renderer.getListCellRendererComponent( - list, value, index, selected, focus) - renderer.setFont(pane.getTextArea.getPainter.getFont) - renderer - } - } - } - } - } - } - } } class Isabelle_Sidekick_Structure( name: String, - get_syntax: => Option[Outer_Syntax], node_name: Buffer => Option[Document.Node.Name]) - extends Isabelle_Sidekick(name, get_syntax) + extends Isabelle_Sidekick(name) { import Thy_Syntax.Structure @@ -186,22 +130,19 @@ } -class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure( - "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name) -{ - override def supportsCompletion = false -} +class Isabelle_Sidekick_Default extends + Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.buffer_node_name) -class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure( - "isabelle-options", Some(Options.options_syntax), PIDE.thy_load.buffer_node_dummy) +class Isabelle_Sidekick_Options extends + Isabelle_Sidekick_Structure("isabelle-options", PIDE.thy_load.buffer_node_dummy) -class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure( - "isabelle-root", Some(Build.root_syntax), PIDE.thy_load.buffer_node_dummy) +class Isabelle_Sidekick_Root extends + Isabelle_Sidekick_Structure("isabelle-root", PIDE.thy_load.buffer_node_dummy) -class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw", PIDE.get_recent_syntax) +class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw") { override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { @@ -234,10 +175,10 @@ } -class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news", Some(Outer_Syntax.empty)) +class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news") { - private val Heading1 = new Regex("""^New in (.*)\w*$""") - private val Heading2 = new Regex("""^\*\*\*\w*(.*)\w*\*\*\*\w*$""") + private val Heading1 = """^New in (.*)\w*$""".r + private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode = new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop)) @@ -260,7 +201,5 @@ true } - - override def supportsCompletion = false } diff -r 473ea1ed7503 -r 1760c01f1c78 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Thu Aug 29 10:24:43 2013 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Aug 29 12:38:33 2013 +0200 @@ -131,6 +131,16 @@ def buffer_text(buffer: JEditBuffer): String = buffer_lock(buffer) { buffer.getText(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_name(buffer: Buffer): String = buffer.getSymlinkPath diff -r 473ea1ed7503 -r 1760c01f1c78 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Aug 29 10:24:43 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Thu Aug 29 12:38:33 2013 +0200 @@ -59,10 +59,8 @@ { var dismissed = false - for { - text_area <- JEdit_Lib.jedit_text_areas(view) - doc_view <- document_view(text_area) - } { if (doc_view.dismissed_popups()) dismissed = true } + JEdit_Lib.jedit_text_areas(view).foreach(text_area => + if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true) if (Pretty_Tooltip.dismissed_all()) dismissed = true @@ -73,6 +71,7 @@ /* document model and view */ def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer) + def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area) def document_views(buffer: Buffer): List[Document_View] = @@ -285,6 +284,12 @@ PIDE.dismissed_popups(text_area.getView) PIDE.exit_view(buffer, text_area) } + + if (msg.getWhat == EditPaneUpdate.CREATED) + Completion_Popup.Text_Area.init(text_area) + + if (msg.getWhat == EditPaneUpdate.DESTROYED) + Completion_Popup.Text_Area.exit(text_area) } case msg: PropertiesChanged => @@ -314,6 +319,8 @@ if (ModeProvider.instance.isInstanceOf[ModeProvider]) ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) + JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _) + val content = Isabelle_Logic.session_content(false) val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax) @@ -334,6 +341,8 @@ override def stop() { + JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _) + if (PIDE.startup_failure.isEmpty) PIDE.options.value.save_prefs() diff -r 473ea1ed7503 -r 1760c01f1c78 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Thu Aug 29 10:24:43 2013 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Thu Aug 29 12:38:33 2013 +0200 @@ -285,10 +285,7 @@ def refresh_buffer(buffer: JEditBuffer) { buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker) - // FIXME potential NPE ahead!?! - val mode = buffer.getMode - val name = mode.getName - val marker = markers.get(name) + val marker = markers.get(JEdit_Lib.buffer_mode(buffer)) marker.map(buffer.setTokenMarker(_)) } }