# HG changeset patch
# User wenzelm
# Date 1420464630 -3600
# Node ID b1086f3e4590bae8aa97de292a50fb2da98c2507
# Parent  9d4728e0092533d729f423553d4fbc6e7f1da26b
apply layout on change of options;

diff -r 9d4728e00925 -r b1086f3e4590 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 14:17:17 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jan 05 14:30:30 2015 +0100
@@ -88,13 +88,30 @@
     }
   set_content(graphview)
 
+
+  /* main */
+
+  private val main =
+    Session.Consumer[Session.Global_Options](getClass.getName) {
+      case _: Session.Global_Options =>
+        GUI_Thread.later {
+          graphview match {
+            case main_panel: isabelle.graphview.Main_Panel =>
+              main_panel.graph_panel.apply_layout()
+            case _ =>
+          }
+        }
+    }
+
   override def init()
   {
     GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    PIDE.session.global_options += main
   }
 
   override def exit()
   {
     GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    PIDE.session.global_options -= main
   }
 }