# HG changeset patch # User wenzelm # Date 1569922943 -7200 # Node ID 93aed7526a94cb0b3ec4b99d0a0772357c11086d # Parent 97d3485028b675a23b17c78e8e3599a6c038313a more robust after shutdown; diff -r 97d3485028b6 -r 93aed7526a94 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Tue Oct 01 11:29:03 2019 +0200 +++ b/src/Pure/PIDE/session.scala Tue Oct 01 11:42:23 2019 +0200 @@ -671,9 +671,12 @@ def get_state(): Document.State = { - val promise = Future.promise[Document.State] - manager.send_wait(Get_State(promise)) - promise.join + if (manager.is_active) { + val promise = Future.promise[Document.State] + manager.send_wait(Get_State(promise)) + promise.join + } + else Document.State.init } def snapshot(name: Document.Node.Name = Document.Node.Name.empty,