# HG changeset patch
# User wenzelm
# Date 1285332421 -7200
# Node ID 4293ce5b07fb0431d228c8e85cff918512edd23b
# Parent  cc3452317b5f0328fb160f65a13e1dda2574faa4
persistent session-panel.selection;

diff -r cc3452317b5f -r 4293ce5b07fb src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Fri Sep 24 14:14:21 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Fri Sep 24 14:47:01 2010 +0200
@@ -12,7 +12,7 @@
 import scala.actors.Actor._
 import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane,
   Component, Swing}
-import scala.swing.event.ButtonClicked
+import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 import java.awt.BorderLayout
 
@@ -32,6 +32,17 @@
   private val tabs = new TabbedPane {
     pages += new TabbedPane.Page("README", Component.wrap(readme))
     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)