# HG changeset patch
# User wenzelm
# Date 1369059476 -7200
# Node ID 573e80625c78d667a982487fcf663c88cd932947
# Parent  f852d08376f9b0be16dc3b26eb79b8d0ce08acb5
more explicit Session.update_options as source of Global_Options event;

diff -r f852d08376f9 -r 573e80625c78 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon May 20 15:42:14 2013 +0200
+++ b/src/Pure/System/session.scala	Mon May 20 16:17:56 2013 +0200
@@ -177,6 +177,7 @@
     version: Document.Version)
   private case class Messages(msgs: List[Isabelle_Process.Message])
   private case class Finished_Scala(id: String, tag: Invoke_Scala.Tag.Value, result: String)
+  private case class Update_Options(options: Options)
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
@@ -415,8 +416,10 @@
           receiver.cancel()
           reply(())
 
-        case Session.Global_Options(options) if prover.isDefined =>
+        case Update_Options(options) if prover.isDefined =>
           if (is_ready) prover.get.options(options)
+          global_options.event(Session.Global_Options(options))
+          reply(())
 
         case Cancel_Execution if prover.isDefined =>
           prover.get.cancel_execution()
@@ -470,13 +473,11 @@
 
   def start(args: List[String])
   {
-    global_options += session_actor
     session_actor ! Start(args)
   }
 
   def stop()
   {
-    global_options -= session_actor
     commands_changed_buffer !? Stop
     change_parser !? Stop
     session_actor !? Stop
@@ -487,6 +488,9 @@
   def update(edits: List[Document.Edit_Text])
   { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
 
+  def update_options(options: Options)
+  { session_actor !? Update_Options(options) }
+
   def dialog_result(id: Document.ID, serial: Long, result: String)
   { session_actor ! Session.Dialog_Result(id, serial, result) }
 }
diff -r f852d08376f9 -r 573e80625c78 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon May 20 15:42:14 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon May 20 16:17:56 2013 +0200
@@ -196,7 +196,7 @@
               }
 
             case Session.Ready =>
-              PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+              PIDE.session.update_options(PIDE.options.value)
               PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
               Swing_Thread.later { delay_load.invoke() }
 
@@ -270,7 +270,7 @@
           }
 
         case msg: PropertiesChanged =>
-          PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+          PIDE.session.update_options(PIDE.options.value)
 
         case _ =>
       }