src/Pure/System/session.scala

 object Session
 {
   /* events */
 
   //{{{
-  case object Global_Options
+  case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(edits: List[Document.Edit_Text])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 

   def reparse_limit: Int = 0
 
 
   /* pervasive event buses */
 
-  val global_options = new Event_Bus[Session.Global_Options.type]
+  val global_options = new Event_Bus[Session.Global_Options]
   val caret_focus = new Event_Bus[Session.Caret_Focus.type]
   val raw_edits = new Event_Bus[Session.Raw_Edits]
   val commands_changed = new Event_Bus[Session.Commands_Changed]
   val phase_changed = new Event_Bus[Session.Phase]
   val syslog_messages = new Event_Bus[Isabelle_Process.Output]

           }
           finished = true
           receiver.cancel()
           reply(())
 
+        case Session.Global_Options(options) if prover.isDefined =>
+          prover.get.options(options)
+
         case Cancel_Execution if prover.isDefined =>
           prover.get.cancel_execution()
 
         case raw @ Session.Raw_Edits(edits) if prover.isDefined =>
           prover.get.discontinue_execution()

 
 
   /* actions */
 
   def start(args: List[String])
-  { session_actor ! Start(args) }
-
-  def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
+  {
+    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 edit(edits: List[Document.Edit_Text])
   { session_actor !? Session.Raw_Edits(edits) }