more permissive Session.update_options: this is wired to jEdit PropertiesChanged, which may occur before the prover is started;
authorwenzelm
Fri Apr 04 22:21:46 2014 +0200 (2014-04-04 ago)
changeset 564122dd33da970ea
parent 56411 913dc982ef55
child 56413 2d4d9a5f68ff
more permissive Session.update_options: this is wired to jEdit PropertiesChanged, which may occur before the prover is started;
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Fri Apr 04 19:09:56 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Fri Apr 04 22:21:46 2014 +0200
     1.3 @@ -521,8 +521,8 @@
     1.4            receiver.cancel()
     1.5            reply(())
     1.6  
     1.7 -        case Update_Options(options) if prover.isDefined =>
     1.8 -          if (is_ready) {
     1.9 +        case Update_Options(options) =>
    1.10 +          if (prover.isDefined && is_ready) {
    1.11              prover.get.options(options)
    1.12              handle_raw_edits(Document.Blobs.empty, Nil)
    1.13            }