# HG changeset patch
# User wenzelm
# Date 1284812922 -7200
# Node ID 57ceabb0bb8e5949e75294a63f894a5ab9ab1d4f
# Parent  d9cf3f83331861803dfe289c50cf6b240f2a29b7
basic setup for prover session panel;

diff -r d9cf3f833318 -r 57ceabb0bb8e src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Fri Sep 17 22:42:07 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Sat Sep 18 14:28:42 2010 +0200
@@ -183,6 +183,7 @@
 insert-newline.shortcut=ENTER
 isabelle-output.dock-position=bottom
 isabelle-raw-output.dock-position=bottom
+isabelle-session.dock-position=bottom
 isabelle.activate.shortcut=CS+ENTER
 line-end.shortcut=END
 line-home.shortcut=HOME
diff -r d9cf3f833318 -r 57ceabb0bb8e src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Fri Sep 17 22:42:07 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Sat Sep 18 14:28:42 2010 +0200
@@ -1,6 +1,6 @@
 ## Isabelle plugin properties
 ##
-##:encoding=ISO-8859-1:
+##:encoding=ISO-8859-1:wrap=soft:maxLineLen=100:
 
 #identification
 plugin.isabelle.jedit.Plugin.name=Isabelle
@@ -35,13 +35,15 @@
 
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-raw-output isabelle.show-protocol
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.session-panel isabelle.show-output isabelle.show-raw-output isabelle.show-protocol
 isabelle.activate.label=Activate current buffer
+isabelle.session-panel.label=Prover session panel
 isabelle.show-output.label=Show Output
 isabelle.show-raw-output.label=Show Raw Output
 isabelle.show-protocol.label=Show Protocol
 
 #dockables
+isabelle-session.title=Session
 isabelle-output.title=Output
 isabelle-raw-output.title=Raw Output
 isabelle-protocol.title=Protocol
diff -r d9cf3f833318 -r 57ceabb0bb8e src/Tools/jEdit/plugin/actions.xml
--- a/src/Tools/jEdit/plugin/actions.xml	Fri Sep 17 22:42:07 2010 +0200
+++ b/src/Tools/jEdit/plugin/actions.xml	Sat Sep 18 14:28:42 2010 +0200
@@ -10,6 +10,11 @@
 			return isabelle.jedit.Isabelle.is_active(view);
 		</IS_SELECTED>
 	</ACTION>
+	<ACTION NAME="isabelle.session-panel">
+		<CODE>
+			wm.addDockableWindow("isabelle-session");
+		</CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.show-output">
 		<CODE>
 			wm.addDockableWindow("isabelle-output");
diff -r d9cf3f833318 -r 57ceabb0bb8e src/Tools/jEdit/plugin/dockables.xml
--- a/src/Tools/jEdit/plugin/dockables.xml	Fri Sep 17 22:42:07 2010 +0200
+++ b/src/Tools/jEdit/plugin/dockables.xml	Sat Sep 18 14:28:42 2010 +0200
@@ -2,6 +2,9 @@
 <!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
 
 <DOCKABLES>
+	<DOCKABLE NAME="isabelle-session" MOVABLE="TRUE">
+		new isabelle.jedit.Session_Dockable(view, position);
+	</DOCKABLE>
 	<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
 		new isabelle.jedit.Output_Dockable(view, position);
 	</DOCKABLE>
diff -r d9cf3f833318 -r 57ceabb0bb8e src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Sep 17 22:42:07 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 18 14:28:42 2010 +0200
@@ -170,6 +170,12 @@
 
   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
 
+  def docked_session(view: View): Option[Session_Dockable] =
+    wm(view).getDockableWindow("isabelle-session") match {
+      case dockable: Session_Dockable => Some(dockable)
+      case _ => None
+    }
+
   def docked_output(view: View): Option[Output_Dockable] =
     wm(view).getDockableWindow("isabelle-output") match {
       case dockable: Output_Dockable => Some(dockable)
diff -r d9cf3f833318 -r 57ceabb0bb8e src/Tools/jEdit/src/jedit/session_dockable.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Sat Sep 18 14:28:42 2010 +0200
@@ -0,0 +1,36 @@
+/*  Title:      Tools/jEdit/src/jedit/session_dockable.scala
+    Author:     Makarius
+
+Dockable window for prover session management.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+import scala.swing.{TextArea, ScrollPane}
+
+import org.gjt.sp.jedit.View
+
+
+class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+{
+  private val text_area = new TextArea("Isabelle session")
+  set_content(new ScrollPane(text_area))
+
+
+  /* main actor */
+
+  private val main_actor = actor {
+    loop {
+      react {
+        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  override def init() { }
+  override def exit() { }
+}