# HG changeset patch
# User wenzelm
# Date 1373727922 -7200
# Node ID f45ab3e8211b884a00586e8b588f38bd48a2948f
# Parent  b1ae4306f29f5499460361fe2e5aaf5e9f8f7534
update_options with full update, e.g. required for re-assignment of Command.prints;

diff -r b1ae4306f29f -r f45ab3e8211b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 13 16:45:47 2013 +0200
+++ b/src/Pure/System/session.scala	Sat Jul 13 17:05:22 2013 +0200
@@ -335,6 +335,23 @@
     }
 
 
+    /* raw edits */
+
+    def handle_raw_edits(edits: List[Document.Edit_Text])
+    //{{{
+    {
+      prover.get.discontinue_execution()
+
+      val previous = global_state().history.tip.version
+      val version = Future.promise[Document.Version]
+      val change = global_state >>> (_.continue_history(previous, edits, version))
+
+      raw_edits.event(Session.Raw_Edits(edits))
+      change_parser ! Text_Edits(previous, edits, version)
+    }
+    //}}}
+
+
     /* resulting changes */
 
     def handle_change(change: Change)
@@ -480,22 +497,18 @@
           reply(())
 
         case Update_Options(options) if prover.isDefined =>
-          if (is_ready) prover.get.options(options)
+          if (is_ready) {
+            prover.get.options(options)
+            handle_raw_edits(Nil)
+          }
           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 =>
-          prover.get.discontinue_execution()
-
-          val previous = global_state().history.tip.version
-          val version = Future.promise[Document.Version]
-          val change = global_state >>> (_.continue_history(previous, edits, version))
-          raw_edits.event(raw)
-          change_parser ! Text_Edits(previous, edits, version)
-
+        case Session.Raw_Edits(edits) if prover.isDefined =>
+          handle_raw_edits(edits)
           reply(())
 
         case Session.Dialog_Result(id, serial, result) if prover.isDefined =>