explicit menu action to complete word;

--- a/src/Tools/jEdit/src/actions.xml	Tue Apr 15 11:05:48 2014 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Tue Apr 15 11:26:17 2014 +0200
@@ -59,7 +59,12 @@
 	</ACTION>
 	<ACTION NAME="isabelle.complete">
 	  <CODE>
-	    isabelle.jedit.Isabelle.complete(view);
+	    isabelle.jedit.Isabelle.complete(view, false);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.complete-word">
+	  <CODE>
+	    isabelle.jedit.Isabelle.complete(view, true);
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.control-sub">

--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 11:05:48 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 11:26:17 2014 +0200
@@ -62,13 +62,13 @@
         case None => None
       }
 
-    def action(text_area: TextArea): Boolean =
+    def action(text_area: TextArea, word_only: Boolean): Boolean =
       apply(text_area) match {
         case Some(text_area_completion) =>
           if (text_area_completion.active_range.isDefined)
-            text_area_completion.action()
+            text_area_completion.action(word_only = word_only)
           else
-            text_area_completion.action(immediate = true, explicit = true)
+            text_area_completion.action(immediate = true, explicit = true, word_only = word_only)
           true
         case None => false
       }
@@ -243,8 +243,11 @@
       }
     }
 
-    def action(immediate: Boolean = false, explicit: Boolean = false, delayed: Boolean = false)
-      : Boolean =
+    def action(
+      immediate: Boolean = false,
+      explicit: Boolean = false,
+      delayed: Boolean = false,
+      word_only: Boolean = false): Boolean =
     {
       val view = text_area.getView
       val layered = view.getLayeredPane
@@ -331,16 +334,19 @@
         }
         if (no_completion) false
         else {
-          val result0 =
-            Completion.Result.merge(history,
-              semantic_completion, syntax_completion(history, explicit, opt_rendering))
           val result =
+          {
+            val result0 =
+              if (word_only) None
+              else
+                Completion.Result.merge(history,
+                  semantic_completion, syntax_completion(history, explicit, opt_rendering))
             opt_rendering match {
               case None => result0
               case Some(rendering) =>
                 Completion.Result.merge(history, result0, spell_checker_completion(rendering))
             }
-
+          }
           result match {
             case Some(result) =>
               result.items match {

--- a/src/Tools/jEdit/src/context_menu.scala	Tue Apr 15 11:05:48 2014 +0200
+++ b/src/Tools/jEdit/src/context_menu.scala	Tue Apr 15 11:26:17 2014 +0200
@@ -43,6 +43,7 @@
     result match {
       case Some(false) =>
         List(
+          action_item("isabelle.complete-word"),
           action_item("isabelle.include-word"),
           action_item("isabelle.include-word-permanently"),
           action_item("isabelle.reset-words"))

--- a/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 11:05:48 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 11:26:17 2014 +0200
@@ -253,9 +253,9 @@
 
   /* completion */
 
-  def complete(view: View)
+  def complete(view: View, word_only: Boolean)
   {
-    if (!Completion_Popup.Text_Area.action(view.getTextArea))
+    if (!Completion_Popup.Text_Area.action(view.getTextArea, word_only))
       CompleteWord.completeWord(view)
   }
 

--- a/src/Tools/jEdit/src/jEdit.props	Tue Apr 15 11:05:48 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Tue Apr 15 11:26:17 2014 +0200
@@ -194,6 +194,7 @@
 isabelle-theories.dock-position=right
 isabelle.complete.label=Complete Isabelle text
 isabelle.complete.shortcut2=C+b
+isabelle.complete-word.label=Complete word
 isabelle.control-bold.label=Control bold
 isabelle.control-bold.shortcut=C+e RIGHT
 isabelle.control-reset.label=Control reset