# HG changeset patch
# User wenzelm
# Date 1598540759 -7200
# Node ID e35997591c5b7854d6241089ecfac371d4f64aa9
# Parent  0d7cd97f6c484acc925d3472de8fa08a33809f14
strict init of protocol handlers;

diff -r 0d7cd97f6c48 -r e35997591c5b src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Aug 27 15:16:56 2020 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Aug 27 17:05:59 2020 +0200
@@ -13,7 +13,9 @@
 
 val _ =
   Isabelle_Process.protocol_command "Prover.stop"
-    (fn [rc] => raise Isabelle_Process.STOP (Value.parse_int rc));
+    (fn rc :: msgs =>
+      (List.app Output.system_message msgs;
+       raise Isabelle_Process.STOP (Value.parse_int rc)));
 
 val _ =
   Isabelle_Process.protocol_command "Prover.options"
diff -r 0d7cd97f6c48 -r e35997591c5b src/Pure/PIDE/protocol_handlers.scala
--- a/src/Pure/PIDE/protocol_handlers.scala	Thu Aug 27 15:16:56 2020 +0200
+++ b/src/Pure/PIDE/protocol_handlers.scala	Thu Aug 27 17:05:59 2020 +0200
@@ -9,9 +9,8 @@
 
 object Protocol_Handlers
 {
-  private def bad_handler(exn: Throwable, name: String): Unit =
-    Output.error_message(
-      "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+  private def err_handler(exn: Throwable, name: String): Nothing =
+    error("Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
 
   sealed case class State(
     session: Session,
@@ -32,18 +31,18 @@
           copy(handlers = handlers + (name -> handler), functions = functions ++ handler.functions)
         }
       }
-      catch { case exn: Throwable => bad_handler(exn, name); this }
+      catch { case exn: Throwable => err_handler(exn, name) }
     }
 
     def init(name: String): State =
     {
-      val new_handler =
+      val handler =
         try {
-          Some(Class.forName(name).getDeclaredConstructor().newInstance()
-            .asInstanceOf[Session.Protocol_Handler])
+          Class.forName(name).getDeclaredConstructor().newInstance()
+            .asInstanceOf[Session.Protocol_Handler]
         }
-        catch { case exn: Throwable => bad_handler(exn, name); None }
-      new_handler match { case Some(handler) => init(handler) case None => this }
+        catch { case exn: Throwable => err_handler(exn, name) }
+      init(handler)
     }
 
     def invoke(msg: Prover.Protocol_Output): Boolean =
diff -r 0d7cd97f6c48 -r e35997591c5b src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Aug 27 15:16:56 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Aug 27 17:05:59 2020 +0200
@@ -544,14 +544,25 @@
               change_command(_.accumulate(state_id, output.message, xml_cache))
 
             case _ if output.is_init =>
-              Isabelle_System.make_services(classOf[Session.Protocol_Handler])
-                .foreach(init_protocol_handler)
+              val init_ok =
+                try {
+                  Isabelle_System.make_services(classOf[Session.Protocol_Handler])
+                    .foreach(init_protocol_handler)
+                  true
+                }
+                catch {
+                  case exn: Throwable =>
+                    prover.get.protocol_command("Prover.stop", "1", Exn.message(exn))
+                    false
+                }
 
-              prover.get.options(prover_options(session_options))
-              prover.get.init_session(resources)
+              if (init_ok) {
+                prover.get.options(prover_options(session_options))
+                prover.get.init_session(resources)
 
-              phase = Session.Ready
-              debugger.ready()
+                phase = Session.Ready
+                debugger.ready()
+              }
 
             case Markup.Process_Result(result) if output.is_exit =>
               if (prover.defined) protocol_handlers.exit()