init options on startup as well;
authorwenzelm
Mon, 19 Nov 2012 20:47:13 +0100
changeset 50127 ff0b52a6d72f
parent 50126 3dec88149176
child 50128 599c935aac82
init options on startup as well;
src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Nov 19 20:23:47 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Nov 19 20:47:13 2012 +0100
@@ -231,6 +231,7 @@
               }
 
             case Session.Ready =>
+              Isabelle.session.global_options.event(Session.Global_Options(Isabelle.options.value))
               JEdit_Lib.jedit_buffers.foreach(Isabelle.init_model)
               Swing_Thread.later { delay_load.invoke() }