# HG changeset patch # User wenzelm # Date 1353765019 -3600 # Node ID 2b3e24e1c9e7f9d30a44bdb7cc0891707aca69ec # Parent 30177ec0be36e944d77dbeb5552c04ec35ab69cd improved editing support for control styles; separate module for Isabelle actions; diff -r 30177ec0be36 -r 2b3e24e1c9e7 NEWS --- 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. diff -r 30177ec0be36 -r 2b3e24e1c9e7 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 30177ec0be36 -r 2b3e24e1c9e7 src/Tools/jEdit/src/Isabelle.props --- 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 diff -r 30177ec0be36 -r 2b3e24e1c9e7 src/Tools/jEdit/src/actions.xml --- 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"); - + + + isabelle.jedit.Isabelle_Actions.check_buffer(buffer); + + + - isabelle.jedit.Isabelle.input_sub(textArea); + isabelle.jedit.Isabelle_Actions.cancel_execution(); + + + + + isabelle.jedit.Isabelle_Actions.control_sub(textArea); - + - isabelle.jedit.Isabelle.input_sup(textArea); + isabelle.jedit.Isabelle_Actions.control_sup(textArea); + + + + + isabelle.jedit.Isabelle_Actions.control_isub(textArea); - + - isabelle.jedit.Isabelle.input_isub(textArea); + isabelle.jedit.Isabelle_Actions.control_isup(textArea); - + - isabelle.jedit.Isabelle.input_isup(textArea); + isabelle.jedit.Isabelle_Actions.control_bold(textArea); + + + + + isabelle.jedit.Isabelle_Actions.control_reset(textArea); - isabelle.jedit.Isabelle.input_bsub(textArea); + isabelle.jedit.Isabelle_Actions.input_bsub(textArea); - isabelle.jedit.Isabelle.input_bsup(textArea); - - - - - isabelle.jedit.Isabelle.input_bold(textArea); - - - - - isabelle.jedit.Isabelle.check_buffer(buffer); - - - - - isabelle.jedit.Isabelle.cancel_execution(); + isabelle.jedit.Isabelle_Actions.input_bsup(textArea); \ No newline at end of file diff -r 30177ec0be36 -r 2b3e24e1c9e7 src/Tools/jEdit/src/isabelle_actions.scala --- /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) } +} + diff -r 30177ec0be36 -r 2b3e24e1c9e7 src/Tools/jEdit/src/plugin.scala --- 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() } } diff -r 30177ec0be36 -r 2b3e24e1c9e7 src/Tools/jEdit/src/session_dockable.scala --- 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") diff -r 30177ec0be36 -r 2b3e24e1c9e7 src/Tools/jEdit/src/token_markup.scala --- 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 =