maintain Completion_Popup.Text_Area as client property like Document_View;
authorwenzelm
Thu Aug 29 12:38:33 2013 +0200 (2013-08-29)
changeset 532741760c01f1c78
parent 53273 473ea1ed7503
child 53275 b34aac6511ab
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;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:24:43 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 12:38:33 2013 +0200
     1.3 @@ -32,11 +32,45 @@
     1.4  
     1.5    object Text_Area
     1.6    {
     1.7 -    def apply(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax]): Text_Area =
     1.8 -      new Text_Area(text_area, get_syntax)
     1.9 +    private val key = new Object
    1.10 +
    1.11 +    def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] =
    1.12 +      text_area.getClientProperty(key) match {
    1.13 +        case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
    1.14 +        case _ => None
    1.15 +      }
    1.16 +
    1.17 +    def exit(text_area: JEditTextArea)
    1.18 +    {
    1.19 +      Swing_Thread.require()
    1.20 +      apply(text_area) match {
    1.21 +        case None =>
    1.22 +        case Some(text_area_completion) =>
    1.23 +          text_area_completion.deactivate()
    1.24 +          text_area.putClientProperty(key, null)
    1.25 +      }
    1.26 +    }
    1.27 +
    1.28 +    def init(text_area: JEditTextArea): Completion_Popup.Text_Area =
    1.29 +    {
    1.30 +      exit(text_area)
    1.31 +      val text_area_completion = new Text_Area(text_area)
    1.32 +      text_area.putClientProperty(key, text_area_completion)
    1.33 +      text_area_completion.activate()
    1.34 +      text_area_completion
    1.35 +    }
    1.36 +
    1.37 +    def dismissed(text_area: JEditTextArea): Boolean =
    1.38 +    {
    1.39 +      Swing_Thread.require()
    1.40 +      apply(text_area) match {
    1.41 +        case Some(text_area_completion) => text_area_completion.dismissed()
    1.42 +        case None => false
    1.43 +      }
    1.44 +    }
    1.45    }
    1.46  
    1.47 -  class Text_Area private(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax])
    1.48 +  class Text_Area private(text_area: JEditTextArea)
    1.49    {
    1.50      /* popup state */
    1.51  
    1.52 @@ -106,7 +140,7 @@
    1.53          val painter = text_area.getPainter
    1.54  
    1.55          if (buffer.isEditable) {
    1.56 -          get_syntax match {
    1.57 +          Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    1.58              case Some(syntax) =>
    1.59                val caret = text_area.getCaretPosition
    1.60                val result =
    1.61 @@ -155,6 +189,23 @@
    1.62            }
    1.63          }
    1.64        }
    1.65 +
    1.66 +
    1.67 +    /* activation */
    1.68 +
    1.69 +    private val outer_key_listener =
    1.70 +      JEdit_Lib.key_listener(key_typed = input _)
    1.71 +
    1.72 +    private def activate()
    1.73 +    {
    1.74 +      text_area.addKeyListener(outer_key_listener)
    1.75 +    }
    1.76 +
    1.77 +    private def deactivate()
    1.78 +    {
    1.79 +      dismissed()
    1.80 +      text_area.removeKeyListener(outer_key_listener)
    1.81 +    }
    1.82    }
    1.83  }
    1.84  
    1.85 @@ -214,7 +265,7 @@
    1.86  
    1.87    /* event handling */
    1.88  
    1.89 -  private val key_listener =
    1.90 +  private val inner_key_listener =
    1.91      JEdit_Lib.key_listener(
    1.92        key_pressed = (e: KeyEvent) =>
    1.93          {
    1.94 @@ -240,7 +291,7 @@
    1.95        key_typed = propagate _
    1.96      )
    1.97  
    1.98 -  list_view.peer.addKeyListener(key_listener)
    1.99 +  list_view.peer.addKeyListener(inner_key_listener)
   1.100  
   1.101    list_view.peer.addMouseListener(new MouseAdapter {
   1.102      override def mouseClicked(e: MouseEvent) {
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 10:24:43 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 12:38:33 2013 +0200
     2.3 @@ -149,19 +149,13 @@
     2.4  
     2.5    /* key listener */
     2.6  
     2.7 -  private val completion_popup =
     2.8 -    Completion_Popup.Text_Area(text_area, PIDE.get_recent_syntax)
     2.9 -
    2.10 -  def dismissed_popups(): Boolean = completion_popup.dismissed()
    2.11 -
    2.12    private val key_listener =
    2.13      JEdit_Lib.key_listener(
    2.14        key_pressed = (evt: KeyEvent) =>
    2.15          {
    2.16            if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
    2.17              evt.consume
    2.18 -        },
    2.19 -      key_typed = completion_popup.input _
    2.20 +        }
    2.21      )
    2.22  
    2.23  
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 10:24:43 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 12:38:33 2013 +0200
     3.3 @@ -16,6 +16,20 @@
     3.4  
     3.5  object Isabelle
     3.6  {
     3.7 +  /* editor modes */
     3.8 +
     3.9 +  val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news")
    3.10 +
    3.11 +  def mode_syntax(name: String): Option[Outer_Syntax] =
    3.12 +    name match {
    3.13 +      case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax
    3.14 +      case "isabelle-options" => Some(Options.options_syntax)
    3.15 +      case "isabelle-root" => Some(Build.root_syntax)
    3.16 +      case "isabelle-news" => Some(Outer_Syntax.empty)
    3.17 +      case _ => None
    3.18 +    }
    3.19 +
    3.20 +
    3.21    /* dockable windows */
    3.22  
    3.23    private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
     4.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 29 10:24:43 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 29 12:38:33 2013 +0200
     4.3 @@ -10,18 +10,12 @@
     4.4  
     4.5  import isabelle._
     4.6  
     4.7 -import scala.collection.Set
     4.8 -import scala.collection.immutable.TreeSet
     4.9 -import scala.util.matching.Regex
    4.10 -
    4.11 -import java.awt.Component
    4.12  import javax.swing.tree.DefaultMutableTreeNode
    4.13  import javax.swing.text.Position
    4.14 -import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList}
    4.15 +import javax.swing.Icon
    4.16  
    4.17 -import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
    4.18 -import errorlist.DefaultErrorSource
    4.19 -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
    4.20 +import org.gjt.sp.jedit.Buffer
    4.21 +import sidekick.{SideKickParser, SideKickParsedData, IAsset}
    4.22  
    4.23  
    4.24  object Isabelle_Sidekick
    4.25 @@ -58,9 +52,11 @@
    4.26  }
    4.27  
    4.28  
    4.29 -class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
    4.30 -  extends SideKickParser(name)
    4.31 +class Isabelle_Sidekick(name: String) extends SideKickParser(name)
    4.32  {
    4.33 +  override def supportsCompletion = false
    4.34 +
    4.35 +
    4.36    /* parsing */
    4.37  
    4.38    @volatile protected var stopped = false
    4.39 @@ -68,7 +64,7 @@
    4.40  
    4.41    def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
    4.42  
    4.43 -  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    4.44 +  def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
    4.45    {
    4.46      stopped = false
    4.47  
    4.48 @@ -77,7 +73,7 @@
    4.49      val root = data.root
    4.50      data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
    4.51  
    4.52 -    val syntax = get_syntax
    4.53 +    val syntax = Isabelle.mode_syntax(name)
    4.54      val ok =
    4.55        if (syntax.isDefined) {
    4.56          val ok = parser(buffer, syntax.get, data)
    4.57 @@ -89,65 +85,13 @@
    4.58  
    4.59      data
    4.60    }
    4.61 -
    4.62 -
    4.63 -  /* completion */
    4.64 -
    4.65 -  override def supportsCompletion = true
    4.66 -  override def canCompleteAnywhere = true
    4.67 -
    4.68 -  override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
    4.69 -  {
    4.70 -    Swing_Thread.assert()
    4.71 -
    4.72 -    val buffer = pane.getBuffer
    4.73 -    JEdit_Lib.buffer_lock(buffer) {
    4.74 -      get_syntax match {
    4.75 -        case None => null
    4.76 -        case Some(syntax) =>
    4.77 -          val line = buffer.getLineOfOffset(caret)
    4.78 -          val start = buffer.getLineStartOffset(line)
    4.79 -          val text = buffer.getSegment(start, caret - start)
    4.80 -
    4.81 -          syntax.completion.complete(text) match {
    4.82 -            case None => null
    4.83 -            case Some((word, cs)) =>
    4.84 -              val ds =
    4.85 -                (if (Isabelle_Encoding.is_active(buffer))
    4.86 -                  cs.map(Symbol.decode(_)).sorted
    4.87 -                 else cs).filter(_ != word)
    4.88 -              if (ds.isEmpty) null
    4.89 -              else
    4.90 -                new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) {
    4.91 -                  override def getRenderer() =
    4.92 -                    new ListCellRenderer[Any] {
    4.93 -                      val default_renderer =
    4.94 -                        (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]]
    4.95 -
    4.96 -                      override def getListCellRendererComponent(
    4.97 -                          list: JList[_ <: Any], value: Any, index: Int,
    4.98 -                          selected: Boolean, focus: Boolean): Component =
    4.99 -                      {
   4.100 -                        val renderer: Component =
   4.101 -                          default_renderer.getListCellRendererComponent(
   4.102 -                            list, value, index, selected, focus)
   4.103 -                        renderer.setFont(pane.getTextArea.getPainter.getFont)
   4.104 -                        renderer
   4.105 -                      }
   4.106 -                    }
   4.107 -                }
   4.108 -          }
   4.109 -      }
   4.110 -    }
   4.111 -  }
   4.112  }
   4.113  
   4.114  
   4.115  class Isabelle_Sidekick_Structure(
   4.116      name: String,
   4.117 -    get_syntax: => Option[Outer_Syntax],
   4.118      node_name: Buffer => Option[Document.Node.Name])
   4.119 -  extends Isabelle_Sidekick(name, get_syntax)
   4.120 +  extends Isabelle_Sidekick(name)
   4.121  {
   4.122    import Thy_Syntax.Structure
   4.123  
   4.124 @@ -186,22 +130,19 @@
   4.125  }
   4.126  
   4.127  
   4.128 -class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
   4.129 -  "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name)
   4.130 -{
   4.131 -  override def supportsCompletion = false
   4.132 -}
   4.133 +class Isabelle_Sidekick_Default extends
   4.134 +  Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.buffer_node_name)
   4.135  
   4.136  
   4.137 -class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
   4.138 -  "isabelle-options", Some(Options.options_syntax), PIDE.thy_load.buffer_node_dummy)
   4.139 +class Isabelle_Sidekick_Options extends
   4.140 +  Isabelle_Sidekick_Structure("isabelle-options", PIDE.thy_load.buffer_node_dummy)
   4.141  
   4.142  
   4.143 -class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
   4.144 -  "isabelle-root", Some(Build.root_syntax), PIDE.thy_load.buffer_node_dummy)
   4.145 +class Isabelle_Sidekick_Root extends
   4.146 +  Isabelle_Sidekick_Structure("isabelle-root", PIDE.thy_load.buffer_node_dummy)
   4.147  
   4.148  
   4.149 -class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw", PIDE.get_recent_syntax)
   4.150 +class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
   4.151  {
   4.152    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   4.153    {
   4.154 @@ -234,10 +175,10 @@
   4.155  }
   4.156  
   4.157  
   4.158 -class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news", Some(Outer_Syntax.empty))
   4.159 +class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
   4.160  {
   4.161 -  private val Heading1 = new Regex("""^New in (.*)\w*$""")
   4.162 -  private val Heading2 = new Regex("""^\*\*\*\w*(.*)\w*\*\*\*\w*$""")
   4.163 +  private val Heading1 = """^New in (.*)\w*$""".r
   4.164 +  private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
   4.165  
   4.166    private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
   4.167      new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
   4.168 @@ -260,7 +201,5 @@
   4.169  
   4.170      true
   4.171    }
   4.172 -
   4.173 -  override def supportsCompletion = false
   4.174  }
   4.175  
     5.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 29 10:24:43 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Aug 29 12:38:33 2013 +0200
     5.3 @@ -131,6 +131,16 @@
     5.4    def buffer_text(buffer: JEditBuffer): String =
     5.5      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
     5.6  
     5.7 +  def buffer_mode(buffer: JEditBuffer): String =
     5.8 +  {
     5.9 +    val mode = buffer.getMode
    5.10 +    if (mode == null) ""
    5.11 +    else {
    5.12 +      val name = mode.getName
    5.13 +      if (name == null) "" else name
    5.14 +    }
    5.15 +  }
    5.16 +
    5.17    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    5.18  
    5.19  
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 10:24:43 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 12:38:33 2013 +0200
     6.3 @@ -59,10 +59,8 @@
     6.4    {
     6.5      var dismissed = false
     6.6  
     6.7 -    for {
     6.8 -      text_area <- JEdit_Lib.jedit_text_areas(view)
     6.9 -      doc_view <- document_view(text_area)
    6.10 -    } { if (doc_view.dismissed_popups()) dismissed = true }
    6.11 +    JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
    6.12 +      if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)
    6.13  
    6.14      if (Pretty_Tooltip.dismissed_all()) dismissed = true
    6.15  
    6.16 @@ -73,6 +71,7 @@
    6.17    /* document model and view */
    6.18  
    6.19    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
    6.20 +
    6.21    def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
    6.22  
    6.23    def document_views(buffer: Buffer): List[Document_View] =
    6.24 @@ -285,6 +284,12 @@
    6.25                PIDE.dismissed_popups(text_area.getView)
    6.26                PIDE.exit_view(buffer, text_area)
    6.27              }
    6.28 +
    6.29 +            if (msg.getWhat == EditPaneUpdate.CREATED)
    6.30 +              Completion_Popup.Text_Area.init(text_area)
    6.31 +
    6.32 +            if (msg.getWhat == EditPaneUpdate.DESTROYED)
    6.33 +              Completion_Popup.Text_Area.exit(text_area)
    6.34            }
    6.35  
    6.36          case msg: PropertiesChanged =>
    6.37 @@ -314,6 +319,8 @@
    6.38        if (ModeProvider.instance.isInstanceOf[ModeProvider])
    6.39          ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
    6.40  
    6.41 +      JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
    6.42 +
    6.43        val content = Isabelle_Logic.session_content(false)
    6.44        val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
    6.45  
    6.46 @@ -334,6 +341,8 @@
    6.47  
    6.48    override def stop()
    6.49    {
    6.50 +    JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
    6.51 +
    6.52      if (PIDE.startup_failure.isEmpty)
    6.53        PIDE.options.value.save_prefs()
    6.54  
     7.1 --- a/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 10:24:43 2013 +0200
     7.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Aug 29 12:38:33 2013 +0200
     7.3 @@ -285,10 +285,7 @@
     7.4    def refresh_buffer(buffer: JEditBuffer)
     7.5    {
     7.6      buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
     7.7 -    // FIXME potential NPE ahead!?!
     7.8 -    val mode = buffer.getMode
     7.9 -    val name = mode.getName
    7.10 -    val marker = markers.get(name)
    7.11 +    val marker = markers.get(JEdit_Lib.buffer_mode(buffer))
    7.12      marker.map(buffer.setTokenMarker(_))
    7.13    }
    7.14  }