improved editing support for control styles;
authorwenzelm
Sat Nov 24 14:50:19 2012 +0100 (2012-11-24)
changeset 501832b3e24e1c9e7
parent 50182 30177ec0be36
child 50184 5a16f42a9b44
improved editing support for control styles;
separate module for Isabelle actions;
NEWS
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/isabelle_actions.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_dockable.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/NEWS	Sat Nov 24 12:39:58 2012 +0100
     1.2 +++ b/NEWS	Sat Nov 24 14:50:19 2012 +0100
     1.3 @@ -77,6 +77,10 @@
     1.4  options, including tuning parameters for editor reactivity and color
     1.5  schemes.
     1.6  
     1.7 +* Improved editing support for control styles: subscript, superscript,
     1.8 +bold, reset of style -- operating on single symbols or text
     1.9 +selections.  Cf. keyboard short-cuts C+e DOWN/UP/RIGHT/LEFT.
    1.10 +
    1.11  * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
    1.12  from Oracle provide better multi-platform experience.  This version is
    1.13  now bundled exclusively with Isabelle.
     2.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sat Nov 24 12:39:58 2012 +0100
     2.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Nov 24 14:50:19 2012 +0100
     2.3 @@ -15,6 +15,7 @@
     2.4    "src/html_panel.scala"
     2.5    "src/hyperlink.scala"
     2.6    "src/info_dockable.scala"
     2.7 +  "src/isabelle_actions.scala"
     2.8    "src/isabelle_encoding.scala"
     2.9    "src/isabelle_logic.scala"
    2.10    "src/isabelle_options.scala"
     3.1 --- a/src/Tools/jEdit/src/Isabelle.props	Sat Nov 24 12:39:58 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Sat Nov 24 14:50:19 2012 +0100
     3.3 @@ -31,12 +31,14 @@
     3.4  isabelle.check-buffer.shortcut=C+e SPACE
     3.5  isabelle.cancel-execution.label=Cancel current proof checking process
     3.6  isabelle.cancel-execution.shortcut=C+e BACK_SPACE
     3.7 -isabelle.input-isub.label=Input subscript
     3.8 -isabelle.input-isub.shortcut=C+e DOWN
     3.9 -isabelle.input-isup.label=Input superscript
    3.10 -isabelle.input-isup.shortcut=C+e UP
    3.11 -isabelle.input-bold.label=Input bold face
    3.12 -isabelle.input-bold.shortcut=C+e RIGHT
    3.13 +isabelle.control-isub.label=Control subscript
    3.14 +isabelle.control-isub.shortcut=C+e DOWN
    3.15 +isabelle.control-isup.label=Control superscript
    3.16 +isabelle.control-isup.shortcut=C+e UP
    3.17 +isabelle.control-bold.label=Control bold
    3.18 +isabelle.control-bold.shortcut=C+e RIGHT
    3.19 +isabelle.control-reset.label=Control reset
    3.20 +isabelle.control-reset.shortcut=C+e LEFT
    3.21  
    3.22  #menu actions
    3.23  plugin.isabelle.jedit.Plugin.menu.label=Isabelle
     4.1 --- a/src/Tools/jEdit/src/actions.xml	Sat Nov 24 12:39:58 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/actions.xml	Sat Nov 24 14:50:19 2012 +0100
     4.3 @@ -42,49 +42,54 @@
     4.4  			wm.addDockableWindow("isabelle-symbols");
     4.5  		</CODE>
     4.6  	</ACTION>
     4.7 -	<ACTION NAME="isabelle.input-sub">
     4.8 +	<ACTION NAME="isabelle.check-buffer">
     4.9 +	  <CODE>
    4.10 +	    isabelle.jedit.Isabelle_Actions.check_buffer(buffer);
    4.11 +	  </CODE>
    4.12 +	</ACTION>
    4.13 +	<ACTION NAME="isabelle.cancel-execution">
    4.14  	  <CODE>
    4.15 -	    isabelle.jedit.Isabelle.input_sub(textArea);
    4.16 +	    isabelle.jedit.Isabelle_Actions.cancel_execution();
    4.17 +	  </CODE>
    4.18 +	</ACTION>
    4.19 +	<ACTION NAME="isabelle.control-sub">
    4.20 +	  <CODE>
    4.21 +	    isabelle.jedit.Isabelle_Actions.control_sub(textArea);
    4.22  	  </CODE>
    4.23  	</ACTION>
    4.24 -	<ACTION NAME="isabelle.input-sup">
    4.25 +	<ACTION NAME="isabelle.control-sup">
    4.26  	  <CODE>
    4.27 -	    isabelle.jedit.Isabelle.input_sup(textArea);
    4.28 +	    isabelle.jedit.Isabelle_Actions.control_sup(textArea);
    4.29 +	  </CODE>
    4.30 +	</ACTION>
    4.31 +	<ACTION NAME="isabelle.control-isub">
    4.32 +	  <CODE>
    4.33 +	    isabelle.jedit.Isabelle_Actions.control_isub(textArea);
    4.34  	  </CODE>
    4.35  	</ACTION>
    4.36 -	<ACTION NAME="isabelle.input-isub">
    4.37 +	<ACTION NAME="isabelle.control-isup">
    4.38  	  <CODE>
    4.39 -	    isabelle.jedit.Isabelle.input_isub(textArea);
    4.40 +	    isabelle.jedit.Isabelle_Actions.control_isup(textArea);
    4.41  	  </CODE>
    4.42  	</ACTION>
    4.43 -	<ACTION NAME="isabelle.input-isup">
    4.44 +	<ACTION NAME="isabelle.control-bold">
    4.45  	  <CODE>
    4.46 -	    isabelle.jedit.Isabelle.input_isup(textArea);
    4.47 +	    isabelle.jedit.Isabelle_Actions.control_bold(textArea);
    4.48 +	  </CODE>
    4.49 +	</ACTION>
    4.50 +	<ACTION NAME="isabelle.control-reset">
    4.51 +	  <CODE>
    4.52 +	    isabelle.jedit.Isabelle_Actions.control_reset(textArea);
    4.53  	  </CODE>
    4.54  	</ACTION>
    4.55  	<ACTION NAME="isabelle.input-bsub">
    4.56  	  <CODE>
    4.57 -	    isabelle.jedit.Isabelle.input_bsub(textArea);
    4.58 +	    isabelle.jedit.Isabelle_Actions.input_bsub(textArea);
    4.59  	  </CODE>
    4.60  	</ACTION>
    4.61  	<ACTION NAME="isabelle.input-bsup">
    4.62  	  <CODE>
    4.63 -	    isabelle.jedit.Isabelle.input_bsup(textArea);
    4.64 -	  </CODE>
    4.65 -	</ACTION>
    4.66 -	<ACTION NAME="isabelle.input-bold">
    4.67 -	  <CODE>
    4.68 -	    isabelle.jedit.Isabelle.input_bold(textArea);
    4.69 -	  </CODE>
    4.70 -	</ACTION>
    4.71 -	<ACTION NAME="isabelle.check-buffer">
    4.72 -	  <CODE>
    4.73 -	    isabelle.jedit.Isabelle.check_buffer(buffer);
    4.74 -	  </CODE>
    4.75 -	</ACTION>
    4.76 -	<ACTION NAME="isabelle.cancel-execution">
    4.77 -	  <CODE>
    4.78 -	    isabelle.jedit.Isabelle.cancel_execution();
    4.79 +	    isabelle.jedit.Isabelle_Actions.input_bsup(textArea);
    4.80  	  </CODE>
    4.81  	</ACTION>
    4.82  </ACTIONS>
    4.83 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sat Nov 24 14:50:19 2012 +0100
     5.3 @@ -0,0 +1,67 @@
     5.4 +/*  Title:      Tools/jEdit/src/plugin.scala
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Convenience actions for Isabelle/jEdit.
     5.8 +*/
     5.9 +
    5.10 +package isabelle.jedit
    5.11 +
    5.12 +
    5.13 +import isabelle._
    5.14 +
    5.15 +import org.gjt.sp.jedit.Buffer
    5.16 +import org.gjt.sp.jedit.textarea.JEditTextArea
    5.17 +
    5.18 +
    5.19 +object Isabelle_Actions
    5.20 +{
    5.21 +  /* full checking */
    5.22 +
    5.23 +  def check_buffer(buffer: Buffer)
    5.24 +  {
    5.25 +    Isabelle.document_model(buffer) match {
    5.26 +      case None =>
    5.27 +      case Some(model) => model.full_perspective()
    5.28 +    }
    5.29 +  }
    5.30 +
    5.31 +
    5.32 +  def cancel_execution() { Isabelle.session.cancel_execution() }
    5.33 +
    5.34 +  /* control styles */
    5.35 +
    5.36 +  def control_sub(text_area: JEditTextArea)
    5.37 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.sub_decoded) }
    5.38 +
    5.39 +  def control_sup(text_area: JEditTextArea)
    5.40 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.sup_decoded) }
    5.41 +
    5.42 +  def control_isub(text_area: JEditTextArea)
    5.43 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.isub_decoded) }
    5.44 +
    5.45 +  def control_isup(text_area: JEditTextArea)
    5.46 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.isup_decoded) }
    5.47 +
    5.48 +  def control_bold(text_area: JEditTextArea)
    5.49 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.bold_decoded) }
    5.50 +
    5.51 +  def control_reset(text_area: JEditTextArea)
    5.52 +  { Token_Markup.edit_ctrl_style(text_area, "") }
    5.53 +
    5.54 +
    5.55 +  /* block styles */
    5.56 +
    5.57 +  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
    5.58 +  {
    5.59 +    s1.foreach(text_area.userInput(_))
    5.60 +    s2.foreach(text_area.userInput(_))
    5.61 +    s2.foreach(_ => text_area.goToPrevCharacter(false))
    5.62 +  }
    5.63 +
    5.64 +  def input_bsub(text_area: JEditTextArea)
    5.65 +  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
    5.66 +
    5.67 +  def input_bsup(text_area: JEditTextArea)
    5.68 +  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
    5.69 +}
    5.70 +
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Nov 24 12:39:58 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Nov 24 14:50:19 2012 +0100
     6.3 @@ -141,34 +141,6 @@
     6.4        case dockable: Protocol_Dockable => Some(dockable)
     6.5        case _ => None
     6.6      }
     6.7 -
     6.8 -
     6.9 -  /* convenience actions */
    6.10 -
    6.11 -  private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
    6.12 -  {
    6.13 -    s1.foreach(text_area.userInput(_))
    6.14 -    s2.foreach(text_area.userInput(_))
    6.15 -    s2.foreach(_ => text_area.goToPrevCharacter(false))
    6.16 -  }
    6.17 -
    6.18 -  def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
    6.19 -  def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
    6.20 -  def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
    6.21 -  def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
    6.22 -  def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
    6.23 -  def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
    6.24 -  def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
    6.25 -
    6.26 -  def check_buffer(buffer: Buffer)
    6.27 -  {
    6.28 -    document_model(buffer) match {
    6.29 -      case None =>
    6.30 -      case Some(model) => model.full_perspective()
    6.31 -    }
    6.32 -  }
    6.33 -
    6.34 -  def cancel_execution() { session.cancel_execution() }
    6.35  }
    6.36  
    6.37  
     7.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Nov 24 12:39:58 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Nov 24 14:50:19 2012 +0100
     7.3 @@ -51,12 +51,12 @@
     7.4    }
     7.5  
     7.6    private val cancel = new Button("Cancel") {
     7.7 -    reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
     7.8 +    reactions += { case ButtonClicked(_) => Isabelle_Actions.cancel_execution() }
     7.9    }
    7.10    cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
    7.11  
    7.12    private val check = new Button("Check") {
    7.13 -    reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
    7.14 +    reactions += { case ButtonClicked(_) => Isabelle_Actions.check_buffer(view.getBuffer) }
    7.15    }
    7.16    check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
    7.17  
     8.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 12:39:58 2012 +0100
     8.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 14:50:19 2012 +0100
     8.3 @@ -17,6 +17,7 @@
     8.4  import org.gjt.sp.jedit.{jEdit, Mode}
     8.5  import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
     8.6    ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
     8.7 +import org.gjt.sp.jedit.textarea.{TextArea, Selection}
     8.8  import org.gjt.sp.jedit.buffer.JEditBuffer
     8.9  
    8.10  import javax.swing.text.Segment
    8.11 @@ -24,6 +25,55 @@
    8.12  
    8.13  object Token_Markup
    8.14  {
    8.15 +  /* editing support for control symbols */
    8.16 +
    8.17 +  private val is_ctrl_style =
    8.18 +    Set(Symbol.sub_decoded, Symbol.sup_decoded,
    8.19 +      Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded)
    8.20 +
    8.21 +  def update_ctrl_style(ctrl: String, text: String): String =
    8.22 +  {
    8.23 +    val result = new StringBuilder
    8.24 +    for (sym <- Symbol.iterator(text) if !is_ctrl_style(sym)) {
    8.25 +      if (Symbol.is_controllable(sym)) result ++= ctrl
    8.26 +      result ++= sym
    8.27 +    }
    8.28 +    result.toString
    8.29 +  }
    8.30 +
    8.31 +  def edit_ctrl_style(text_area: TextArea, ctrl: String)
    8.32 +  {
    8.33 +    Swing_Thread.assert()
    8.34 +
    8.35 +    val buffer = text_area.getBuffer
    8.36 +
    8.37 +    text_area.getSelection.toList match {
    8.38 +      case Nil if ctrl == "" =>
    8.39 +        try {
    8.40 +          buffer.beginCompoundEdit()
    8.41 +          val caret = text_area.getCaretPosition
    8.42 +          if (caret > 0 && is_ctrl_style(buffer.getText(caret - 1, 1)))
    8.43 +            text_area.backspace()
    8.44 +        }
    8.45 +        finally {
    8.46 +          buffer.endCompoundEdit()
    8.47 +        }
    8.48 +      case Nil if ctrl != "" =>
    8.49 +        text_area.setSelectedText(ctrl)
    8.50 +      case sels =>
    8.51 +        try {
    8.52 +          buffer.beginCompoundEdit()
    8.53 +          sels.foreach(sel =>
    8.54 +            text_area.setSelectedText(sel,
    8.55 +              update_ctrl_style(ctrl, text_area.getSelectedText(sel))))
    8.56 +        }
    8.57 +        finally {
    8.58 +          buffer.endCompoundEdit()
    8.59 +        }
    8.60 +    }
    8.61 +  }
    8.62 +
    8.63 +
    8.64    /* font operations */
    8.65  
    8.66    private def font_metrics(font: Font): LineMetrics =