--- a/src/Tools/jEdit/dist-template/properties/jedit.props Tue Dec 08 23:18:07 2009 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Tue Dec 08 23:45:42 2009 +0100
@@ -171,7 +171,7 @@
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
isabelle-history.dock-position=bottom
-isabelle-raw-output.dock-position=bottom
+isabelle-protocol.dock-position=bottom
isabelle-results.dock-position=bottom
isabelle.activate.shortcut=CS+ENTER
mode.isabelle.sidekick.showStatusWindow.label=true
--- a/src/Tools/jEdit/plugin/Isabelle.props Tue Dec 08 23:18:07 2009 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props Tue Dec 08 23:45:42 2009 +0100
@@ -29,15 +29,15 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-results isabelle.show-raw-output isabelle.show-history
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol isabelle.show-history
isabelle.activate.label=Activate current buffer
-isabelle.show-results.label=Show Results
-isabelle.show-raw-output.label=Show Raw Output
+isabelle.show-output.label=Show Output
+isabelle.show-protocol.label=Show Protocol
isabelle.show-history.label=Show History
#dockables
-isabelle-results.title=Results
-isabelle-raw-output.title=Raw Output
+isabelle-output.title=Output
+isabelle-protocol.title=Protocol
isabelle-history.title=History
#SideKick
--- a/src/Tools/jEdit/plugin/actions.xml Tue Dec 08 23:18:07 2009 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml Tue Dec 08 23:45:42 2009 +0100
@@ -10,14 +10,14 @@
return isabelle.jedit.Isabelle.plugin().is_active(view.getBuffer());
</IS_SELECTED>
</ACTION>
- <ACTION NAME="isabelle.show-results">
+ <ACTION NAME="isabelle.show-output">
<CODE>
- wm.addDockableWindow("isabelle-results");
+ wm.addDockableWindow("isabelle-output");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.show-raw-output">
+ <ACTION NAME="isabelle.show-protocol">
<CODE>
- wm.addDockableWindow("isabelle-raw-output");
+ wm.addDockableWindow("isabelle-protocol");
</CODE>
</ACTION>
<ACTION NAME="isabelle.show-history">
--- a/src/Tools/jEdit/plugin/dockables.xml Tue Dec 08 23:18:07 2009 +0100
+++ b/src/Tools/jEdit/plugin/dockables.xml Tue Dec 08 23:45:42 2009 +0100
@@ -2,11 +2,11 @@
<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
<DOCKABLES>
- <DOCKABLE NAME="isabelle-results" MOVABLE="TRUE">
- new isabelle.jedit.Results_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
+ new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
- new isabelle.jedit.Raw_Output_Dockable(view, position);
+ <DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
+ new isabelle.jedit.Protocol_Dockable(view, position);
</DOCKABLE>
<DOCKABLE NAME="isabelle-history" MOVABLE="TRUE">
new isabelle.jedit.History_Dockable(view, position).peer ();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Dec 08 23:45:42 2009 +0100
@@ -0,0 +1,75 @@
+/*
+ * Dockable window with result message output
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import isabelle.proofdocument.{Command, HTML_Panel}
+
+import scala.actors.Actor._
+
+import javax.swing.JPanel
+import java.awt.{BorderLayout, Dimension}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+
+class Output_Dockable(view: View, position: String) extends JPanel
+{
+ /* outer panel */
+
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+
+ setLayout(new BorderLayout)
+
+
+ /* HTML panel */
+
+ private val html_panel = new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"))
+ add(html_panel, BorderLayout.CENTER)
+
+
+ /* actor wiring */
+
+ private val output_actor = actor {
+ loop {
+ react {
+ case cmd: Command =>
+ val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
+ val body =
+ if (cmd == null) Nil // FIXME ??
+ else cmd.results(theory_view.current_document)
+ html_panel.render(body)
+
+ case bad => System.err.println("output_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ private val properties_actor = actor {
+ loop {
+ react {
+ case _: Unit => html_panel.init(Isabelle.Int_Property("font-size"))
+ case bad => System.err.println("properties_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def addNotify() {
+ super.addNotify()
+ Isabelle.plugin.state_update += output_actor
+ Isabelle.plugin.properties_changed += properties_actor
+ }
+
+ override def removeNotify() {
+ Isabelle.plugin.state_update -= output_actor
+ Isabelle.plugin.properties_changed -= properties_actor
+ super.removeNotify()
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Tue Dec 08 23:45:42 2009 +0100
@@ -0,0 +1,59 @@
+/*
+ * Dockable window for raw process output
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import scala.actors.Actor._
+
+import java.awt.{Dimension, Graphics, BorderLayout}
+import javax.swing.{JPanel, JTextArea, JScrollPane}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.DockableWindowManager
+
+
+class Protocol_Dockable(view: View, position: String) extends JPanel
+{
+ // outer panel
+
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+
+ setLayout(new BorderLayout)
+
+
+ // text area
+
+ private val text_area = new JTextArea
+ add(new JScrollPane(text_area), BorderLayout.CENTER)
+
+
+ /* actor wiring */
+
+ private val raw_actor = actor {
+ loop {
+ react {
+ case result: Isabelle_Process.Result =>
+ Swing_Thread.now { text_area.append(result.toString + "\n") }
+
+ case bad => System.err.println("raw_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def addNotify()
+ {
+ super.addNotify()
+ Isabelle.plugin.raw_results += raw_actor
+ }
+
+ override def removeNotify()
+ {
+ Isabelle.plugin.raw_results -= raw_actor
+ super.removeNotify()
+ }
+}
--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Tue Dec 08 23:18:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-/*
- * Dockable window for raw process output
- *
- * @author Makarius
- */
-
-package isabelle.jedit
-
-
-import scala.actors.Actor._
-
-import java.awt.{Dimension, Graphics, BorderLayout}
-import javax.swing.{JPanel, JTextArea, JScrollPane}
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
-
-
-class Raw_Output_Dockable(view: View, position: String) extends JPanel
-{
- // outer panel
-
- if (position == DockableWindowManager.FLOATING)
- setPreferredSize(new Dimension(500, 250))
-
- setLayout(new BorderLayout)
-
-
- // text area
-
- private val text_area = new JTextArea
- add(new JScrollPane(text_area), BorderLayout.CENTER)
-
-
- /* actor wiring */
-
- private val raw_actor = actor {
- loop {
- react {
- case result: Isabelle_Process.Result =>
- Swing_Thread.now { text_area.append(result.toString + "\n") }
-
- case bad => System.err.println("raw_actor: ignoring bad message " + bad)
- }
- }
- }
-
- override def addNotify()
- {
- super.addNotify()
- Isabelle.plugin.raw_results += raw_actor
- }
-
- override def removeNotify()
- {
- Isabelle.plugin.raw_results -= raw_actor
- super.removeNotify()
- }
-}
--- a/src/Tools/jEdit/src/jedit/results_dockable.scala Tue Dec 08 23:18:07 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-/*
- * Dockable window with result message output
- *
- * @author Makarius
- */
-
-package isabelle.jedit
-
-
-import isabelle.proofdocument.{Command, HTML_Panel}
-
-import scala.actors.Actor._
-
-import javax.swing.JPanel
-import java.awt.{BorderLayout, Dimension}
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.DockableWindowManager
-
-
-
-class Results_Dockable(view: View, position: String) extends JPanel
-{
- /* outer panel */
-
- if (position == DockableWindowManager.FLOATING)
- setPreferredSize(new Dimension(500, 250))
-
- setLayout(new BorderLayout)
-
-
- /* HTML panel */
-
- private val html_panel = new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"))
- add(html_panel, BorderLayout.CENTER)
-
-
- /* actor wiring */
-
- private val results_actor = actor {
- loop {
- react {
- case cmd: Command =>
- val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
- val body =
- if (cmd == null) Nil // FIXME ??
- else cmd.results(theory_view.current_document)
- html_panel.render(body)
-
- case bad => System.err.println("results_actor: ignoring bad message " + bad)
- }
- }
- }
-
- private val properties_actor = actor {
- loop {
- react {
- case _: Unit => html_panel.init(Isabelle.Int_Property("font-size"))
- case bad => System.err.println("properties_actor: ignoring bad message " + bad)
- }
- }
- }
-
- override def addNotify() {
- super.addNotify()
- Isabelle.plugin.state_update += results_actor
- Isabelle.plugin.properties_changed += properties_actor
- }
-
- override def removeNotify() {
- Isabelle.plugin.state_update -= results_actor
- Isabelle.plugin.properties_changed -= properties_actor
- super.removeNotify()
- }
-}
--- a/src/Tools/jEdit/src/proofdocument/theory_view.scala Tue Dec 08 23:18:07 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala Tue Dec 08 23:45:42 2009 +0100
@@ -19,7 +19,7 @@
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
-import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker, Raw_Output_Dockable}
+import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker}
object Theory_View