--- a/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 21:17:46 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Thu Aug 29 21:49:46 2013 +0200
@@ -11,7 +11,7 @@
import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
object Isabelle
@@ -163,6 +163,17 @@
}
+ /* completion */
+
+ def complete(view: View)
+ {
+ Completion_Popup.Text_Area(view.getTextArea) match {
+ case Some(text_area_completion) => text_area_completion.action(true)
+ case None => CompleteWord.completeWord(view)
+ }
+ }
+
+
/* control styles */
def control_sub(text_area: JEditTextArea)