# HG changeset patch # User immler@in.tum.de # Date 1251363069 -7200 # Node ID d179fcb04cbc9c497c08ac9b30da7015dfa85a06 # Parent c99878d7bec70007a561f4cad0e1b727b52dcd1c output_info specific to prover diff -r c99878d7bec7 -r d179fcb04cbc src/Tools/jEdit/src/jedit/OutputDockable.scala --- 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() + } } diff -r c99878d7bec7 -r d179fcb04cbc src/Tools/jEdit/src/jedit/Plugin.scala --- 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 _ => } } diff -r c99878d7bec7 -r d179fcb04cbc src/Tools/jEdit/src/jedit/ProverSetup.scala --- 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 diff -r c99878d7bec7 -r d179fcb04cbc src/Tools/jEdit/src/jedit/TheoryView.scala --- 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() { diff -r c99878d7bec7 -r d179fcb04cbc src/Tools/jEdit/src/prover/Prover.scala --- 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)