src/Pure/PIDE/session.scala
changeset 77243 629dce95bb5c
parent 77199 7d7786585ab0
child 80300 152d6c58adb3
--- a/src/Pure/PIDE/session.scala	Sat Feb 11 14:24:20 2023 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Feb 11 16:38:29 2023 +0100
@@ -727,7 +727,7 @@
         {
           case Session.Startup | Session.Shutdown => None
           case Session.Terminated(_) => Some((false, phase))
-          case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
+          case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result.ok))))
           case Session.Ready => Some((true, post_phase(Session.Shutdown)))
         })
     if (was_ready) manager.send(Stop)