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;

--- 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) {

--- 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 _
+        }
     )
 
 

--- 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

--- 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
 }
 

--- 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
 
 

--- 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()
 

--- 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(_))
   }
 }