explicit menu action to complete word;
authorwenzelm
Tue Apr 15 11:26:17 2014 +0200 (2014-04-15 ago)
changeset 565865ef60881681d
parent 56585 a0e844c6e1ed
child 56587 83777a91f5de
explicit menu action to complete word;
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/context_menu.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Tools/jEdit/src/actions.xml	Tue Apr 15 11:05:48 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/actions.xml	Tue Apr 15 11:26:17 2014 +0200
     1.3 @@ -59,7 +59,12 @@
     1.4  	</ACTION>
     1.5  	<ACTION NAME="isabelle.complete">
     1.6  	  <CODE>
     1.7 -	    isabelle.jedit.Isabelle.complete(view);
     1.8 +	    isabelle.jedit.Isabelle.complete(view, false);
     1.9 +	  </CODE>
    1.10 +	</ACTION>
    1.11 +	<ACTION NAME="isabelle.complete-word">
    1.12 +	  <CODE>
    1.13 +	    isabelle.jedit.Isabelle.complete(view, true);
    1.14  	  </CODE>
    1.15  	</ACTION>
    1.16  	<ACTION NAME="isabelle.control-sub">
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 11:05:48 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 15 11:26:17 2014 +0200
     2.3 @@ -62,13 +62,13 @@
     2.4          case None => None
     2.5        }
     2.6  
     2.7 -    def action(text_area: TextArea): Boolean =
     2.8 +    def action(text_area: TextArea, word_only: Boolean): Boolean =
     2.9        apply(text_area) match {
    2.10          case Some(text_area_completion) =>
    2.11            if (text_area_completion.active_range.isDefined)
    2.12 -            text_area_completion.action()
    2.13 +            text_area_completion.action(word_only = word_only)
    2.14            else
    2.15 -            text_area_completion.action(immediate = true, explicit = true)
    2.16 +            text_area_completion.action(immediate = true, explicit = true, word_only = word_only)
    2.17            true
    2.18          case None => false
    2.19        }
    2.20 @@ -243,8 +243,11 @@
    2.21        }
    2.22      }
    2.23  
    2.24 -    def action(immediate: Boolean = false, explicit: Boolean = false, delayed: Boolean = false)
    2.25 -      : Boolean =
    2.26 +    def action(
    2.27 +      immediate: Boolean = false,
    2.28 +      explicit: Boolean = false,
    2.29 +      delayed: Boolean = false,
    2.30 +      word_only: Boolean = false): Boolean =
    2.31      {
    2.32        val view = text_area.getView
    2.33        val layered = view.getLayeredPane
    2.34 @@ -331,16 +334,19 @@
    2.35          }
    2.36          if (no_completion) false
    2.37          else {
    2.38 -          val result0 =
    2.39 -            Completion.Result.merge(history,
    2.40 -              semantic_completion, syntax_completion(history, explicit, opt_rendering))
    2.41            val result =
    2.42 +          {
    2.43 +            val result0 =
    2.44 +              if (word_only) None
    2.45 +              else
    2.46 +                Completion.Result.merge(history,
    2.47 +                  semantic_completion, syntax_completion(history, explicit, opt_rendering))
    2.48              opt_rendering match {
    2.49                case None => result0
    2.50                case Some(rendering) =>
    2.51                  Completion.Result.merge(history, result0, spell_checker_completion(rendering))
    2.52              }
    2.53 -
    2.54 +          }
    2.55            result match {
    2.56              case Some(result) =>
    2.57                result.items match {
     3.1 --- a/src/Tools/jEdit/src/context_menu.scala	Tue Apr 15 11:05:48 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/context_menu.scala	Tue Apr 15 11:26:17 2014 +0200
     3.3 @@ -43,6 +43,7 @@
     3.4      result match {
     3.5        case Some(false) =>
     3.6          List(
     3.7 +          action_item("isabelle.complete-word"),
     3.8            action_item("isabelle.include-word"),
     3.9            action_item("isabelle.include-word-permanently"),
    3.10            action_item("isabelle.reset-words"))
     4.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 11:05:48 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Apr 15 11:26:17 2014 +0200
     4.3 @@ -253,9 +253,9 @@
     4.4  
     4.5    /* completion */
     4.6  
     4.7 -  def complete(view: View)
     4.8 +  def complete(view: View, word_only: Boolean)
     4.9    {
    4.10 -    if (!Completion_Popup.Text_Area.action(view.getTextArea))
    4.11 +    if (!Completion_Popup.Text_Area.action(view.getTextArea, word_only))
    4.12        CompleteWord.completeWord(view)
    4.13    }
    4.14  
     5.1 --- a/src/Tools/jEdit/src/jEdit.props	Tue Apr 15 11:05:48 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/jEdit.props	Tue Apr 15 11:26:17 2014 +0200
     5.3 @@ -194,6 +194,7 @@
     5.4  isabelle-theories.dock-position=right
     5.5  isabelle.complete.label=Complete Isabelle text
     5.6  isabelle.complete.shortcut2=C+b
     5.7 +isabelle.complete-word.label=Complete word
     5.8  isabelle.control-bold.label=Control bold
     5.9  isabelle.control-bold.shortcut=C+e RIGHT
    5.10  isabelle.control-reset.label=Control reset