# HG changeset patch
# User wenzelm
# Date 1503254317 -7200
# Node ID 0b55fbc51f76870c4d5b2493162dc7bfe3273dc5
# Parent  f7b0d6fb417a15db847765f7385989fc0d8272c7
reinit the manager thread, e.g. after restart of the Isabelle/jEdit plugin;

diff -r f7b0d6fb417a -r 0b55fbc51f76 src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Sun Aug 20 20:05:36 2017 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Sun Aug 20 20:38:37 2017 +0200
@@ -140,7 +140,7 @@
   def send_reply(session: Session, serial: Long, answer: Answer) =
     manager.send(Reply(session, serial, answer))
 
-  private lazy val manager: Consumer_Thread[Any] =
+  def make_manager: Consumer_Thread[Any] =
   {
     var contexts = Map.empty[Document_ID.Command, Context]
 
@@ -283,17 +283,27 @@
     )
   }
 
+  private val manager_variable = Synchronized[Option[Consumer_Thread[Any]]](None)
+
+  def manager: Consumer_Thread[Any] =
+    manager_variable.value match {
+      case Some(thread) if thread.is_active => thread
+      case _ => error("Bad Simplifier_Trace.manager thread")
+    }
+
 
   /* protocol handler */
 
   class Handler extends Session.Protocol_Handler
   {
-    assert(manager.is_active)
+    try { manager }
+    catch { case ERROR(_) => manager_variable.change(_ => Some(make_manager)) }
 
     override def exit() =
     {
       manager.send(Clear_Memory)
       manager.shutdown()
+      manager_variable.change(_ => None)
     }
 
     private def cancel(msg: Prover.Protocol_Output): Boolean =