# HG changeset patch
# User wenzelm
# Date 1350418426 -7200
# Node ID 2b82358694e62d1bff926befd37928e721ee6d95
# Parent  bd370af308f00071c8c610e1304d3e90f90bd3df
retain info dockable state via educated guess on window focus;

diff -r bd370af308f0 -r 2b82358694e6 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Tue Oct 16 21:30:52 2012 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Tue Oct 16 22:13:46 2012 +0200
@@ -16,7 +16,7 @@
 
 import java.lang.System
 import java.awt.BorderLayout
-import java.awt.event.{ComponentEvent, ComponentAdapter}
+import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
 
 import org.gjt.sp.jedit.View
 
@@ -28,17 +28,20 @@
   private var implicit_snapshot = Document.State.init.snapshot()
   private var implicit_info: XML.Body = Nil
 
-  def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
+  private def set_implicit(snapshot: Document.Snapshot, info: XML.Body)
   {
     Swing_Thread.require()
 
     implicit_snapshot = snapshot
     implicit_info = info
+  }
 
-    view.getDockableWindowManager.floatDockableWindow("isabelle-info")
+  private def reset_implicit(): Unit = set_implicit(Document.State.init.snapshot(), Nil)
 
-    implicit_snapshot = Document.State.init.snapshot()
-    implicit_info = Nil
+  def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
+  {
+    set_implicit(snapshot, info)
+    view.getDockableWindowManager.floatDockableWindow("isabelle-info")
   }
 }
 
@@ -52,13 +55,22 @@
 
   private var zoom_factor = 100
 
+  private val snapshot = Info_Dockable.implicit_snapshot
+  private val info = Info_Dockable.implicit_info
+
+  private val window_focus_listener =
+    new WindowFocusListener {
+      def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, info) }
+      def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
+    }
+
 
   /* pretty text area */
 
   private val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
-  pretty_text_area.update(Info_Dockable.implicit_snapshot, Info_Dockable.implicit_info)
+  pretty_text_area.update(snapshot, info)
 
   private def handle_resize()
   {
@@ -85,6 +97,7 @@
   {
     Swing_Thread.require()
 
+    JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
     Isabelle.session.global_options += main_actor
     handle_resize()
   }
@@ -93,6 +106,7 @@
   {
     Swing_Thread.require()
 
+    JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
     Isabelle.session.global_options -= main_actor
     delay_resize.revoke()
   }