clarified signature;
authorwenzelm
Wed, 14 Sep 2022 10:46:47 +0200
changeset 76146 a64f3496d93a
parent 76145 a6bdf4b889ca
child 76147 75f0fc965539
clarified signature;
src/Pure/System/bash.scala
src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/bash.scala	Tue Sep 13 23:06:52 2022 +0200
+++ b/src/Pure/System/bash.scala	Wed Sep 14 10:46:47 2022 +0200
@@ -146,19 +146,13 @@
     }
 
 
-    // JVM shutdown hook
-
-    private val shutdown_hook = Isabelle_Thread.create(() => terminate())
-
-    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
-    catch { case _: IllegalStateException => }
-
-
     // cleanup
 
+    private val shutdown_hook =
+      Isabelle_System.create_shutdown_hook { terminate() }
+
     private def do_cleanup(): Unit = {
-      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
-      catch { case _: IllegalStateException => }
+      Isabelle_System.remove_shutdown_hook(shutdown_hook)
 
       script_file.delete()
       winpid_file.foreach(_.delete())
--- a/src/Pure/System/isabelle_system.scala	Tue Sep 13 23:06:52 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Sep 14 10:46:47 2022 +0200
@@ -360,6 +360,23 @@
   }
 
 
+  /* JVM shutdown hook */
+
+  def create_shutdown_hook(body: => Unit): Thread = {
+    val shutdown_hook = Isabelle_Thread.create(new Runnable { def run: Unit = body })
+
+    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
+    catch { case _: IllegalStateException => }
+
+    shutdown_hook
+  }
+
+  def remove_shutdown_hook(shutdown_hook: Thread): Unit =
+    try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
+    catch { case _: IllegalStateException => }
+
+
+
   /** external processes **/
 
   /* GNU bash */