src/Tools/jEdit/src/completion_popup.scala

       val view = text_area.getView
       val layered = view.getLayeredPane
       val buffer = text_area.getBuffer
       val painter = text_area.getPainter
 
-      val history = PIDE.completion_history.value
+      val history = PIDE.plugin.completion_history.value
       val decode = Isabelle_Encoding.is_active(buffer)
 
       def open_popup(result: Completion.Result)
       {
         val font =

           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.completion_history.update(item)
+                PIDE.plugin.completion_history.update(item)
                 insert(item)
               }
               override def propagate(evt: KeyEvent) {
                 if (view.getKeyEventInterceptor == null)
                   JEdit_Lib.propagate_key(view, evt)

 
     def action()
     {
       GUI.layered_pane(text_field) match {
         case Some(layered) if text_field.isEditable =>
-          val history = PIDE.completion_history.value
+          val history = PIDE.plugin.completion_history.value
 
           val caret = text_field.getCaret.getDot
           val text = text_field.getText
 
           val context = syntax.language_context

               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.completion_history.update(item)
+                    PIDE.plugin.completion_history.update(item)
                     insert(item)
                   }
                   override def propagate(evt: KeyEvent) {
                     if (!evt.isConsumed) text_field.processKeyEvent(evt)
                   }