# HG changeset patch
# User wenzelm
# Date 1353875729 -3600
# Node ID 1382ad6d4774828b9d49c958ba2d95da3ba8b60a
# Parent 54be125d8cdcc8774c287f93e76179badd710f27
tuned signature;
diff -r 54be125d8cdc -r 1382ad6d4774 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Nov 25 21:23:20 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Nov 25 21:35:29 2012 +0100
@@ -15,7 +15,7 @@
"src/html_panel.scala"
"src/hyperlink.scala"
"src/info_dockable.scala"
- "src/isabelle_actions.scala"
+ "src/isabelle.scala"
"src/isabelle_encoding.scala"
"src/isabelle_logic.scala"
"src/isabelle_options.scala"
diff -r 54be125d8cdc -r 1382ad6d4774 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml Sun Nov 25 21:23:20 2012 +0100
+++ b/src/Tools/jEdit/src/actions.xml Sun Nov 25 21:35:29 2012 +0100
@@ -44,62 +44,62 @@
- isabelle.jedit.Isabelle_Actions.increase_font_size(view);
+ isabelle.jedit.Isabelle.increase_font_size(view);
- isabelle.jedit.Isabelle_Actions.decrease_font_size(view);
+ isabelle.jedit.Isabelle.decrease_font_size(view);
- isabelle.jedit.Isabelle_Actions.check_buffer(buffer);
+ isabelle.jedit.Isabelle.check_buffer(buffer);
- isabelle.jedit.Isabelle_Actions.cancel_execution();
+ isabelle.jedit.Isabelle.cancel_execution();
- isabelle.jedit.Isabelle_Actions.control_sub(textArea);
+ isabelle.jedit.Isabelle.control_sub(textArea);
- isabelle.jedit.Isabelle_Actions.control_sup(textArea);
+ isabelle.jedit.Isabelle.control_sup(textArea);
- isabelle.jedit.Isabelle_Actions.control_isub(textArea);
+ isabelle.jedit.Isabelle.control_isub(textArea);
- isabelle.jedit.Isabelle_Actions.control_isup(textArea);
+ isabelle.jedit.Isabelle.control_isup(textArea);
- isabelle.jedit.Isabelle_Actions.control_bold(textArea);
+ isabelle.jedit.Isabelle.control_bold(textArea);
- isabelle.jedit.Isabelle_Actions.control_reset(textArea);
+ isabelle.jedit.Isabelle.control_reset(textArea);
- isabelle.jedit.Isabelle_Actions.input_bsub(textArea);
+ isabelle.jedit.Isabelle.input_bsub(textArea);
- isabelle.jedit.Isabelle_Actions.input_bsup(textArea);
+ isabelle.jedit.Isabelle.input_bsup(textArea);
\ No newline at end of file
diff -r 54be125d8cdc -r 1382ad6d4774 src/Tools/jEdit/src/isabelle.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle.scala Sun Nov 25 21:35:29 2012 +0100
@@ -0,0 +1,112 @@
+/* Title: Tools/jEdit/src/isabelle.scala
+ Author: Makarius
+
+Convenience operations for Isabelle/jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.{jEdit, View, Buffer}
+import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+object Isabelle
+{
+ /* dockable windows */
+
+ private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
+
+ def docked_session(view: View): Option[Session_Dockable] =
+ wm(view).getDockableWindow("isabelle-session") match {
+ case dockable: Session_Dockable => Some(dockable)
+ case _ => None
+ }
+
+ def docked_output(view: View): Option[Output_Dockable] =
+ wm(view).getDockableWindow("isabelle-output") match {
+ case dockable: Output_Dockable => Some(dockable)
+ case _ => None
+ }
+
+ def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
+ wm(view).getDockableWindow("isabelle-raw-output") match {
+ case dockable: Raw_Output_Dockable => Some(dockable)
+ case _ => None
+ }
+
+ def docked_protocol(view: View): Option[Protocol_Dockable] =
+ wm(view).getDockableWindow("isabelle-protocol") match {
+ case dockable: Protocol_Dockable => Some(dockable)
+ case _ => None
+ }
+
+
+ /* font size */
+
+ def change_font_size(view: View, change: Int => Int)
+ {
+ val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
+ jEdit.setIntegerProperty("view.fontsize", size)
+ jEdit.propertiesChanged()
+ jEdit.saveSettings()
+ view.getStatus.setMessageAndClear("Text font size: " + size)
+ }
+
+ def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
+ def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
+
+
+ /* full checking */
+
+ def check_buffer(buffer: Buffer)
+ {
+ PIDE.document_model(buffer) match {
+ case None =>
+ case Some(model) => model.full_perspective()
+ }
+ }
+
+ def cancel_execution() { PIDE.session.cancel_execution() }
+
+
+ /* control styles */
+
+ def control_sub(text_area: JEditTextArea)
+ { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
+
+ def control_sup(text_area: JEditTextArea)
+ { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
+
+ def control_isub(text_area: JEditTextArea)
+ { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
+
+ def control_isup(text_area: JEditTextArea)
+ { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
+
+ def control_bold(text_area: JEditTextArea)
+ { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
+
+ def control_reset(text_area: JEditTextArea)
+ { Token_Markup.edit_control_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 54be125d8cdc -r 1382ad6d4774 src/Tools/jEdit/src/isabelle_actions.scala
--- a/src/Tools/jEdit/src/isabelle_actions.scala Sun Nov 25 21:23:20 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-/* Title: Tools/jEdit/src/plugin.scala
- Author: Makarius
-
-Convenience actions for Isabelle/jEdit.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.{jEdit, View, Buffer}
-import org.gjt.sp.jedit.textarea.JEditTextArea
-
-
-object Isabelle_Actions
-{
- /* font size */
-
- def change_font_size(view: View, change: Int => Int)
- {
- val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
- jEdit.setIntegerProperty("view.fontsize", size)
- jEdit.propertiesChanged()
- jEdit.saveSettings()
- view.getStatus.setMessageAndClear("Text font size: " + size)
- }
-
- def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
- def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
-
-
- /* full checking */
-
- def check_buffer(buffer: Buffer)
- {
- PIDE.document_model(buffer) match {
- case None =>
- case Some(model) => model.full_perspective()
- }
- }
-
- def cancel_execution() { PIDE.session.cancel_execution() }
-
-
- /* control styles */
-
- def control_sub(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
-
- def control_sup(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
-
- def control_isub(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
-
- def control_isup(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
-
- def control_bold(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
-
- def control_reset(text_area: JEditTextArea)
- { Token_Markup.edit_control_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 54be125d8cdc -r 1382ad6d4774 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala Sun Nov 25 21:23:20 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Nov 25 21:35:29 2012 +0100
@@ -17,7 +17,6 @@
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
-import org.gjt.sp.jedit.gui.DockableWindowManager
import org.gjt.sp.util.SyntaxUtilities
@@ -104,35 +103,6 @@
Document_View.exit(text_area)
}
}
-
-
- /* dockable windows */
-
- private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
-
- def docked_session(view: View): Option[Session_Dockable] =
- wm(view).getDockableWindow("isabelle-session") match {
- case dockable: Session_Dockable => Some(dockable)
- case _ => None
- }
-
- def docked_output(view: View): Option[Output_Dockable] =
- wm(view).getDockableWindow("isabelle-output") match {
- case dockable: Output_Dockable => Some(dockable)
- case _ => None
- }
-
- def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
- wm(view).getDockableWindow("isabelle-raw-output") match {
- case dockable: Raw_Output_Dockable => Some(dockable)
- case _ => None
- }
-
- def docked_protocol(view: View): Option[Protocol_Dockable] =
- wm(view).getDockableWindow("isabelle-protocol") match {
- case dockable: Protocol_Dockable => Some(dockable)
- case _ => None
- }
}
diff -r 54be125d8cdc -r 1382ad6d4774 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala Sun Nov 25 21:23:20 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala Sun Nov 25 21:35:29 2012 +0100
@@ -51,12 +51,12 @@
}
private val cancel = new Button("Cancel") {
- reactions += { case ButtonClicked(_) => Isabelle_Actions.cancel_execution() }
+ reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
}
cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
private val check = new Button("Check") {
- reactions += { case ButtonClicked(_) => Isabelle_Actions.check_buffer(view.getBuffer) }
+ reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
}
check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")