# HG changeset patch
# User wenzelm
# Date 1338323071 -7200
# Node ID d899be1cfe6dc3cd705200ec8c33c8c10a2a14b4
# Parent a4f9957878ab637729dcd2f52226e56717793f99
separate syslog dockable -- discontinued tendency of sub-window management via tabs;
diff -r a4f9957878ab -r d899be1cfe6d src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Tue May 29 21:48:05 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue May 29 22:24:31 2012 +0200
@@ -25,6 +25,7 @@
"src/readme_dockable.scala"
"src/scala_console.scala"
"src/session_dockable.scala"
+ "src/syslog_dockable.scala"
"src/text_area_painter.scala"
"src/text_overview.scala"
"src/token_markup.scala"
diff -r a4f9957878ab -r d899be1cfe6d src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Tue May 29 21:48:05 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Tue May 29 22:24:31 2012 +0200
@@ -50,12 +50,13 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel
+plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
isabelle.session-panel.label=Prover Session panel
isabelle.output-panel.label=Output panel
isabelle.raw-output-panel.label=Raw Output panel
isabelle.protocol-panel.label=Protocol panel
isabelle.readme-panel.label=README panel
+isabelle.syslog-panel.label=Syslog panel
#dockables
isabelle-session.title=Prover Session
@@ -63,6 +64,7 @@
isabelle-raw-output.title=Raw Output
isabelle-protocol.title=Protocol
isabelle-readme.title=README
+isabelle-syslog.title=Syslog
#SideKick
sidekick.parser.isabelle.label=Isabelle
diff -r a4f9957878ab -r d899be1cfe6d src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml Tue May 29 21:48:05 2012 +0200
+++ b/src/Tools/jEdit/src/actions.xml Tue May 29 22:24:31 2012 +0200
@@ -7,6 +7,11 @@
wm.addDockableWindow("isabelle-session");
+
+
+ wm.addDockableWindow("isabelle-syslog");
+
+
wm.addDockableWindow("isabelle-readme");
diff -r a4f9957878ab -r d899be1cfe6d src/Tools/jEdit/src/dockables.xml
--- a/src/Tools/jEdit/src/dockables.xml Tue May 29 21:48:05 2012 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Tue May 29 22:24:31 2012 +0200
@@ -5,6 +5,9 @@
new isabelle.jedit.Session_Dockable(view, position);
+
+ new isabelle.jedit.Syslog_Dockable(view, position);
+
new isabelle.jedit.README_Dockable(view, position);
diff -r a4f9957878ab -r d899be1cfe6d src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala Tue May 29 21:48:05 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Tue May 29 22:24:31 2012 +0200
@@ -10,8 +10,7 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
- ScrollPane, TabbedPane, Component, Swing}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, Component}
import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
import java.lang.System
@@ -24,9 +23,9 @@
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
{
- /* main tabs */
+ /* status */
- val status = new ListView(Nil: List[Document.Node.Name]) {
+ private val status = new ListView(Nil: List[Document.Node.Name]) {
listenTo(mouse.clicks)
reactions += {
case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
@@ -37,30 +36,12 @@
status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
status.selection.intervalMode = ListView.IntervalMode.Single
- private val syslog = new TextArea(Isabelle.session.current_syslog())
-
- private val tabs = new TabbedPane {
- pages += new TabbedPane.Page("Theory Status", new ScrollPane(status))
- pages += new TabbedPane.Page("System Log", new ScrollPane(syslog))
-
- selection.index =
- {
- val index = Isabelle.Int_Property("session-panel.selection", 0)
- if (index >= pages.length) 0 else index
- }
- listenTo(selection)
- reactions += {
- case SelectionChanged(_) =>
- Isabelle.Int_Property("session-panel.selection") = selection.index
- }
- }
-
- set_content(tabs)
+ set_content(status)
/* controls */
- val session_phase = new Label(Isabelle.session.phase.toString)
+ private val session_phase = new Label(Isabelle.session.phase.toString)
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Prover status"
@@ -171,13 +152,6 @@
private val main_actor = actor {
loop {
react {
- case output: Isabelle_Process.Output =>
- if (output.is_syslog)
- Swing_Thread.later {
- val text = Isabelle.session.current_syslog()
- if (text != syslog.text) syslog.text = text
- }
-
case phase: Session.Phase => handle_phase(phase)
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
@@ -189,20 +163,13 @@
override def init()
{
- Isabelle.session.syslog_messages += main_actor
- Isabelle.session.phase_changed += main_actor
- handle_phase(Isabelle.session.phase)
- Isabelle.session.commands_changed += main_actor
- handle_update()
+ Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
+ Isabelle.session.commands_changed += main_actor; handle_update()
}
override def exit()
{
- Isabelle.session.syslog_messages -= main_actor
Isabelle.session.phase_changed -= main_actor
Isabelle.session.commands_changed -= main_actor
}
-
- handle_phase(Isabelle.session.phase)
- handle_update()
}
diff -r a4f9957878ab -r d899be1cfe6d src/Tools/jEdit/src/syslog_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Tue May 29 22:24:31 2012 +0200
@@ -0,0 +1,60 @@
+/* Title: Tools/jEdit/src/syslog_dockable.scala
+ Author: Makarius
+
+Dockable window for syslog.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+import scala.swing.TextArea
+
+import java.lang.System
+
+import org.gjt.sp.jedit.View
+
+
+class Syslog_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+{
+ /* GUI components */
+
+ private val syslog = new TextArea()
+
+ private def update_syslog()
+ {
+ Swing_Thread.later {
+ val text = Isabelle.session.current_syslog()
+ if (text != syslog.text) syslog.text = text
+ }
+ }
+
+ set_content(syslog)
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case output: Isabelle_Process.Output =>
+ if (output.is_syslog) update_syslog()
+
+ case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Isabelle.session.syslog_messages += main_actor
+ update_syslog()
+ }
+
+ override def exit()
+ {
+ Isabelle.session.syslog_messages -= main_actor
+ }
+}