improved editing support for control styles;
separate module for Isabelle actions;
--- a/NEWS Sat Nov 24 12:39:58 2012 +0100
+++ b/NEWS Sat Nov 24 14:50:19 2012 +0100
@@ -77,6 +77,10 @@
options, including tuning parameters for editor reactivity and color
schemes.
+* Improved editing support for control styles: subscript, superscript,
+bold, reset of style -- operating on single symbols or text
+selections. Cf. keyboard short-cuts C+e DOWN/UP/RIGHT/LEFT.
+
* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates
from Oracle provide better multi-platform experience. This version is
now bundled exclusively with Isabelle.
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Nov 24 12:39:58 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Nov 24 14:50:19 2012 +0100
@@ -15,6 +15,7 @@
"src/html_panel.scala"
"src/hyperlink.scala"
"src/info_dockable.scala"
+ "src/isabelle_actions.scala"
"src/isabelle_encoding.scala"
"src/isabelle_logic.scala"
"src/isabelle_options.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Sat Nov 24 12:39:58 2012 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Sat Nov 24 14:50:19 2012 +0100
@@ -31,12 +31,14 @@
isabelle.check-buffer.shortcut=C+e SPACE
isabelle.cancel-execution.label=Cancel current proof checking process
isabelle.cancel-execution.shortcut=C+e BACK_SPACE
-isabelle.input-isub.label=Input subscript
-isabelle.input-isub.shortcut=C+e DOWN
-isabelle.input-isup.label=Input superscript
-isabelle.input-isup.shortcut=C+e UP
-isabelle.input-bold.label=Input bold face
-isabelle.input-bold.shortcut=C+e RIGHT
+isabelle.control-isub.label=Control subscript
+isabelle.control-isub.shortcut=C+e DOWN
+isabelle.control-isup.label=Control superscript
+isabelle.control-isup.shortcut=C+e UP
+isabelle.control-bold.label=Control bold
+isabelle.control-bold.shortcut=C+e RIGHT
+isabelle.control-reset.label=Control reset
+isabelle.control-reset.shortcut=C+e LEFT
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
--- a/src/Tools/jEdit/src/actions.xml Sat Nov 24 12:39:58 2012 +0100
+++ b/src/Tools/jEdit/src/actions.xml Sat Nov 24 14:50:19 2012 +0100
@@ -42,49 +42,54 @@
wm.addDockableWindow("isabelle-symbols");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.input-sub">
+ <ACTION NAME="isabelle.check-buffer">
+ <CODE>
+ isabelle.jedit.Isabelle_Actions.check_buffer(buffer);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.cancel-execution">
<CODE>
- isabelle.jedit.Isabelle.input_sub(textArea);
+ isabelle.jedit.Isabelle_Actions.cancel_execution();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.control-sub">
+ <CODE>
+ isabelle.jedit.Isabelle_Actions.control_sub(textArea);
</CODE>
</ACTION>
- <ACTION NAME="isabelle.input-sup">
+ <ACTION NAME="isabelle.control-sup">
<CODE>
- isabelle.jedit.Isabelle.input_sup(textArea);
+ isabelle.jedit.Isabelle_Actions.control_sup(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.control-isub">
+ <CODE>
+ isabelle.jedit.Isabelle_Actions.control_isub(textArea);
</CODE>
</ACTION>
- <ACTION NAME="isabelle.input-isub">
+ <ACTION NAME="isabelle.control-isup">
<CODE>
- isabelle.jedit.Isabelle.input_isub(textArea);
+ isabelle.jedit.Isabelle_Actions.control_isup(textArea);
</CODE>
</ACTION>
- <ACTION NAME="isabelle.input-isup">
+ <ACTION NAME="isabelle.control-bold">
<CODE>
- isabelle.jedit.Isabelle.input_isup(textArea);
+ isabelle.jedit.Isabelle_Actions.control_bold(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.control-reset">
+ <CODE>
+ isabelle.jedit.Isabelle_Actions.control_reset(textArea);
</CODE>
</ACTION>
<ACTION NAME="isabelle.input-bsub">
<CODE>
- isabelle.jedit.Isabelle.input_bsub(textArea);
+ isabelle.jedit.Isabelle_Actions.input_bsub(textArea);
</CODE>
</ACTION>
<ACTION NAME="isabelle.input-bsup">
<CODE>
- isabelle.jedit.Isabelle.input_bsup(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.input-bold">
- <CODE>
- isabelle.jedit.Isabelle.input_bold(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.check-buffer">
- <CODE>
- isabelle.jedit.Isabelle.check_buffer(buffer);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.cancel-execution">
- <CODE>
- isabelle.jedit.Isabelle.cancel_execution();
+ isabelle.jedit.Isabelle_Actions.input_bsup(textArea);
</CODE>
</ACTION>
</ACTIONS>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_actions.scala Sat Nov 24 14:50:19 2012 +0100
@@ -0,0 +1,67 @@
+/* Title: Tools/jEdit/src/plugin.scala
+ Author: Makarius
+
+Convenience actions for Isabelle/jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.textarea.JEditTextArea
+
+
+object Isabelle_Actions
+{
+ /* full checking */
+
+ def check_buffer(buffer: Buffer)
+ {
+ Isabelle.document_model(buffer) match {
+ case None =>
+ case Some(model) => model.full_perspective()
+ }
+ }
+
+
+ def cancel_execution() { Isabelle.session.cancel_execution() }
+
+ /* control styles */
+
+ def control_sub(text_area: JEditTextArea)
+ { Token_Markup.edit_ctrl_style(text_area, Symbol.sub_decoded) }
+
+ def control_sup(text_area: JEditTextArea)
+ { Token_Markup.edit_ctrl_style(text_area, Symbol.sup_decoded) }
+
+ def control_isub(text_area: JEditTextArea)
+ { Token_Markup.edit_ctrl_style(text_area, Symbol.isub_decoded) }
+
+ def control_isup(text_area: JEditTextArea)
+ { Token_Markup.edit_ctrl_style(text_area, Symbol.isup_decoded) }
+
+ def control_bold(text_area: JEditTextArea)
+ { Token_Markup.edit_ctrl_style(text_area, Symbol.bold_decoded) }
+
+ def control_reset(text_area: JEditTextArea)
+ { Token_Markup.edit_ctrl_style(text_area, "") }
+
+
+ /* block styles */
+
+ private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
+ {
+ s1.foreach(text_area.userInput(_))
+ s2.foreach(text_area.userInput(_))
+ s2.foreach(_ => text_area.goToPrevCharacter(false))
+ }
+
+ def input_bsub(text_area: JEditTextArea)
+ { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
+
+ def input_bsup(text_area: JEditTextArea)
+ { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
+}
+
--- a/src/Tools/jEdit/src/plugin.scala Sat Nov 24 12:39:58 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sat Nov 24 14:50:19 2012 +0100
@@ -141,34 +141,6 @@
case dockable: Protocol_Dockable => Some(dockable)
case _ => None
}
-
-
- /* convenience actions */
-
- private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
- {
- s1.foreach(text_area.userInput(_))
- s2.foreach(text_area.userInput(_))
- s2.foreach(_ => text_area.goToPrevCharacter(false))
- }
-
- def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
- def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
- def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
- def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
- def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
- def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
- def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
-
- def check_buffer(buffer: Buffer)
- {
- document_model(buffer) match {
- case None =>
- case Some(model) => model.full_perspective()
- }
- }
-
- def cancel_execution() { session.cancel_execution() }
}
--- a/src/Tools/jEdit/src/session_dockable.scala Sat Nov 24 12:39:58 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala Sat Nov 24 14:50:19 2012 +0100
@@ -51,12 +51,12 @@
}
private val cancel = new Button("Cancel") {
- reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
+ reactions += { case ButtonClicked(_) => Isabelle_Actions.cancel_execution() }
}
cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
private val check = new Button("Check") {
- reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
+ reactions += { case ButtonClicked(_) => Isabelle_Actions.check_buffer(view.getBuffer) }
}
check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
--- a/src/Tools/jEdit/src/token_markup.scala Sat Nov 24 12:39:58 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Sat Nov 24 14:50:19 2012 +0100
@@ -17,6 +17,7 @@
import org.gjt.sp.jedit.{jEdit, Mode}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
+import org.gjt.sp.jedit.textarea.{TextArea, Selection}
import org.gjt.sp.jedit.buffer.JEditBuffer
import javax.swing.text.Segment
@@ -24,6 +25,55 @@
object Token_Markup
{
+ /* editing support for control symbols */
+
+ private val is_ctrl_style =
+ Set(Symbol.sub_decoded, Symbol.sup_decoded,
+ Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded)
+
+ def update_ctrl_style(ctrl: String, text: String): String =
+ {
+ val result = new StringBuilder
+ for (sym <- Symbol.iterator(text) if !is_ctrl_style(sym)) {
+ if (Symbol.is_controllable(sym)) result ++= ctrl
+ result ++= sym
+ }
+ result.toString
+ }
+
+ def edit_ctrl_style(text_area: TextArea, ctrl: String)
+ {
+ Swing_Thread.assert()
+
+ val buffer = text_area.getBuffer
+
+ text_area.getSelection.toList match {
+ case Nil if ctrl == "" =>
+ try {
+ buffer.beginCompoundEdit()
+ val caret = text_area.getCaretPosition
+ if (caret > 0 && is_ctrl_style(buffer.getText(caret - 1, 1)))
+ text_area.backspace()
+ }
+ finally {
+ buffer.endCompoundEdit()
+ }
+ case Nil if ctrl != "" =>
+ text_area.setSelectedText(ctrl)
+ case sels =>
+ try {
+ buffer.beginCompoundEdit()
+ sels.foreach(sel =>
+ text_area.setSelectedText(sel,
+ update_ctrl_style(ctrl, text_area.getSelectedText(sel))))
+ }
+ finally {
+ buffer.endCompoundEdit()
+ }
+ }
+ }
+
+
/* font operations */
private def font_metrics(font: Font): LineMetrics =