--- a/src/Tools/jEdit/src/jedit/OutputDockable.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/OutputDockable.scala Thu Aug 27 10:51:09 2009 +0200
@@ -8,7 +8,7 @@
package isabelle.jedit
-import java.awt.{Dimension, GridLayout}
+import java.awt.{Dimension, Graphics, GridLayout}
import javax.swing.{JPanel, JTextArea, JScrollPane}
import org.gjt.sp.jedit.View
@@ -22,4 +22,10 @@
setLayout(new GridLayout(1, 1))
add(new JScrollPane(new JTextArea))
+
+ def set_text(output_text_view: JTextArea) {
+ removeAll()
+ add(new JScrollPane(output_text_view))
+ revalidate()
+ }
}
--- a/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 10:51:09 2009 +0200
@@ -133,17 +133,16 @@
override def handleMessage(msg: EBMessage)
{
msg match {
- case epu: EditPaneUpdate => epu.getWhat match {
- case EditPaneUpdate.BUFFER_CHANGED =>
- val buffer = epu.getEditPane.getBuffer
- (mapping get buffer) map (_.theory_view.activate)
- buffer.propertiesChanged()
- case EditPaneUpdate.BUFFER_CHANGING =>
- val buffer = epu.getEditPane.getBuffer
- if (buffer != null)
- (mapping get buffer) map (_.theory_view.deactivate)
- case _ =>
- }
+ case epu: EditPaneUpdate =>
+ val buffer = epu.getEditPane.getBuffer
+ epu.getWhat match {
+ case EditPaneUpdate.BUFFER_CHANGED =>
+ (mapping get buffer) map (_.theory_view.activate)
+ case EditPaneUpdate.BUFFER_CHANGING =>
+ if (buffer != null)
+ (mapping get buffer) map (_.theory_view.deactivate)
+ case _ =>
+ }
case _ =>
}
}
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Aug 27 10:51:09 2009 +0200
@@ -24,7 +24,6 @@
var prover: Prover = null
var theory_view: TheoryView = null
- val output_text_view = new JTextArea
def activate(view: View)
{
@@ -36,22 +35,6 @@
theory_view.activate()
prover.set_document(theory_view.change_receiver, buffer.getName)
- // register output-view
- prover.output_info += (text =>
- {
- output_text_view.append(text + "\n")
- val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
- // link process output if dockable is active
- if (dockable != null) {
- val output_dockable = dockable.asInstanceOf[OutputDockable]
- if (output_dockable.getComponent(0) != output_text_view ) {
- output_dockable.asInstanceOf[OutputDockable].removeAll
- output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view))
- output_dockable.revalidate
- }
- }
- })
-
}
def deactivate
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 10:51:09 2009 +0200
@@ -79,6 +79,16 @@
text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
buffer.addBufferListener(this)
+
+ val dockable =
+ text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
+ if (dockable != null) {
+ val output_dockable = dockable.asInstanceOf[OutputDockable]
+ val output_text_view = prover.output_text_view
+ output_dockable.set_text(output_text_view)
+ }
+
+ buffer.propertiesChanged()
}
def deactivate() {
--- a/src/Tools/jEdit/src/prover/Prover.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Aug 27 10:51:09 2009 +0200
@@ -16,6 +16,7 @@
import scala.actors.Actor._
import org.gjt.sp.util.Log
+import javax.swing.JTextArea
import isabelle.jedit.Isabelle
import isabelle.proofdocument.{ProofDocument, Change, Token}
@@ -83,10 +84,12 @@
/* event handling */
+ val output_info = new EventBus[Isabelle_Process.Result]
+ var change_receiver: Actor = null
- val output_info = new EventBus[String]
- var change_receiver: Actor = null
-
+ val output_text_view = new JTextArea
+ output_info += (result => output_text_view.append(result.toString + "\n"))
+
private def handle_result(result: Isabelle_Process.Result)
{
def command_change(c: Command) = change_receiver ! c
@@ -101,7 +104,7 @@
if (result.kind == Isabelle_Process.Kind.STDOUT ||
result.kind == Isabelle_Process.Kind.STDIN)
- output_info.event(result.toString)
+ output_info.event(result)
else {
result.kind match {
@@ -115,7 +118,7 @@
command.add_result(state, process.parse_message(result))
command_change(command)
} else {
- output_info.event(result.toString)
+ output_info.event(result)
}
case Isabelle_Process.Kind.STATUS =>
@@ -141,7 +144,7 @@
// document edits
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
if document_versions.exists(_.id == doc_id) =>
- output_info.event(result.toString)
+ output_info.event(result)
val doc = document_versions.find(_.id == doc_id).get
for {
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
@@ -159,17 +162,17 @@
// command status
case XML.Elem(Markup.UNPROCESSED, _, _)
if command != null =>
- output_info.event(result.toString)
+ output_info.event(result)
command.set_status(state, Command.Status.UNPROCESSED)
command_change(command)
case XML.Elem(Markup.FINISHED, _, _)
if command != null =>
- output_info.event(result.toString)
+ output_info.event(result)
command.set_status(state, Command.Status.FINISHED)
command_change(command)
case XML.Elem(Markup.FAILED, _, _)
if command != null =>
- output_info.event(result.toString)
+ output_info.event(result)
command.set_status(state, Command.Status.FAILED)
command_change(command)
case XML.Elem(kind, attr, body)