# 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,