src/Pure/System/session.scala

     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     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)
   {
     val this_actor = self
 

           }
           finished = true
           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()
 
         case raw @ Session.Raw_Edits(edits) if prover.isDefined =>

 
   /* actions */
 
   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
   }
 
   def cancel_execution() { session_actor ! Cancel_Execution }
 
   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) }
 }