# HG changeset patch
# User wenzelm
# Date 1377805786 -7200
# Node ID fd27b8f5a479d41d8cbb2203261adc9931fd5d24
# Parent  f567c1c7b1802045d1f187c73e20bc9e31a18b09
added action isabelle.complete, using standard jEdit keyboard shortcut;

diff -r f567c1c7b180 -r fd27b8f5a479 NEWS
--- 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".
 
diff -r f567c1c7b180 -r fd27b8f5a479 src/Tools/jEdit/src/actions.xml
--- 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);
diff -r f567c1c7b180 -r fd27b8f5a479 src/Tools/jEdit/src/completion_popup.scala
--- 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 =
diff -r f567c1c7b180 -r fd27b8f5a479 src/Tools/jEdit/src/isabelle.scala
--- 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)
diff -r f567c1c7b180 -r fd27b8f5a479 src/Tools/jEdit/src/jEdit.props
--- 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