separate syslog dockable -- discontinued tendency of sub-window management via tabs;
authorwenzelm
Tue, 29 May 2012 22:24:31 +0200
changeset 48021 d899be1cfe6d
parent 48020 a4f9957878ab
child 48022 e237a3fc7ba3
separate syslog dockable -- discontinued tendency of sub-window management via tabs;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/dockables.xml
src/Tools/jEdit/src/session_dockable.scala
src/Tools/jEdit/src/syslog_dockable.scala
--- 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"
--- 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
--- 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");
 		</CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.syslog-panel">
+		<CODE>
+			wm.addDockableWindow("isabelle-syslog");
+		</CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.readme-panel">
 		<CODE>
 			wm.addDockableWindow("isabelle-readme");
--- 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 @@
 	<DOCKABLE NAME="isabelle-session" MOVABLE="TRUE">
 		new isabelle.jedit.Session_Dockable(view, position);
 	</DOCKABLE>
+	<DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
+		new isabelle.jedit.Syslog_Dockable(view, position);
+	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-readme" MOVABLE="TRUE">
 		new isabelle.jedit.README_Dockable(view, position);
 	</DOCKABLE>
--- 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()
 }
--- /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
+  }
+}