src/Pure/PIDE/session.scala
changeset 56412 2dd33da970ea
parent 56394 bbf4d512f395
child 56671 06853449cf0a
equal deleted inserted replaced
56411:913dc982ef55 56412:2dd33da970ea
   519           }
   519           }
   520           finished = true
   520           finished = true
   521           receiver.cancel()
   521           receiver.cancel()
   522           reply(())
   522           reply(())
   523 
   523 
   524         case Update_Options(options) if prover.isDefined =>
   524         case Update_Options(options) =>
   525           if (is_ready) {
   525           if (prover.isDefined && is_ready) {
   526             prover.get.options(options)
   526             prover.get.options(options)
   527             handle_raw_edits(Document.Blobs.empty, Nil)
   527             handle_raw_edits(Document.Blobs.empty, Nil)
   528           }
   528           }
   529           global_options.event(Session.Global_Options(options))
   529           global_options.event(Session.Global_Options(options))
   530           reply(())
   530           reply(())