--- a/NEWS Thu Aug 29 21:17:46 2013 +0200
+++ b/NEWS Thu Aug 29 21:49:46 2013 +0200
@@ -96,6 +96,9 @@
completed in backslash forms, e.g. \forall or \<forall> that both
produce the Isabelle symbol \<forall> in its Unicode rendering.
+* Standard jEdit completion via C+b uses action isabelle.complete
+with fall-back on complete-word for non-Isabelle buffers.
+
* Improved support for Linux look-and-feel "GTK+", see also "Utilities
/ Global Options / Appearance".
--- a/src/Tools/jEdit/src/actions.xml Thu Aug 29 21:17:46 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml Thu Aug 29 21:49:46 2013 +0200
@@ -117,6 +117,11 @@
isabelle.jedit.Isabelle.decrease_font_size(view);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.complete">
+ <CODE>
+ isabelle.jedit.Isabelle.complete(view);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.control-sub">
<CODE>
isabelle.jedit.Isabelle.control_sub(textArea);
--- a/src/Tools/jEdit/src/completion_popup.scala Thu Aug 29 21:17:46 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Thu Aug 29 21:49:46 2013 +0200
@@ -155,10 +155,6 @@
else input_delay.invoke()
}
}
- else {
- dismissed()
- input_delay.revoke()
- }
}
private val input_delay =
--- 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)
--- a/src/Tools/jEdit/src/jEdit.props Thu Aug 29 21:17:46 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Thu Aug 29 21:49:46 2013 +0200
@@ -190,6 +190,8 @@
isabelle-sledgehammer.dock-position=bottom
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
+isabelle.complete.label=Complete text
+isabelle.complete.shortcut=C+b
isabelle.control-bold.label=Control bold
isabelle.control-bold.shortcut=C+e RIGHT
isabelle.control-reset.label=Control reset