# HG changeset patch
# User wenzelm
# Date 1396642906 -7200
# Node ID 2dd33da970ea63376e719e6b4793f9393bcb93eb
# Parent  913dc982ef55ba9d8d350c1dfd231607ed923c76
more permissive Session.update_options: this is wired to jEdit PropertiesChanged, which may occur before the prover is started;

diff -r 913dc982ef55 -r 2dd33da970ea src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Apr 04 19:09:56 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Apr 04 22:21:46 2014 +0200
@@ -521,8 +521,8 @@
           receiver.cancel()
           reply(())
 
-        case Update_Options(options) if prover.isDefined =>
-          if (is_ready) {
+        case Update_Options(options) =>
+          if (prover.isDefined && is_ready) {
             prover.get.options(options)
             handle_raw_edits(Document.Blobs.empty, Nil)
           }