# HG changeset patch # User wenzelm # Date 1260312342 -3600 # Node ID bb5d68f7fd5e7a810cb550fed750150a13fe8455 # Parent 1a79c9b9af825fc42b7c042de7a8e55135c25e9c renamed "raw output" to "protocol"; renamed "results" to "output"; diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/dist-template/properties/jedit.props --- 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 diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/plugin/actions.xml --- 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()); - + - wm.addDockableWindow("isabelle-results"); + wm.addDockableWindow("isabelle-output"); - + - wm.addDockableWindow("isabelle-raw-output"); + wm.addDockableWindow("isabelle-protocol"); diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/plugin/dockables.xml --- 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 @@ - - new isabelle.jedit.Results_Dockable(view, position); + + new isabelle.jedit.Output_Dockable(view, position); - - new isabelle.jedit.Raw_Output_Dockable(view, position); + + new isabelle.jedit.Protocol_Dockable(view, position); new isabelle.jedit.History_Dockable(view, position).peer (); diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/src/jedit/output_dockable.scala --- /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() + } +} diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/src/jedit/protocol_dockable.scala --- /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() + } +} diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/src/jedit/raw_output_dockable.scala --- 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() - } -} diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/src/jedit/results_dockable.scala --- 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() - } -} diff -r 1a79c9b9af82 -r bb5d68f7fd5e src/Tools/jEdit/src/proofdocument/theory_view.scala --- 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