prefer Exn.result: avoid accidental capture of interrupts, similar to ML;

--- a/src/Pure/Admin/build_log.scala	Thu Oct 12 20:58:15 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu Oct 12 21:11:59 2023 +0200
@@ -820,7 +820,7 @@
   class Store private[Build_Log](val options: Options, val cache: XML.Cache) {
     override def toString: String = {
       val s =
-        Exn.capture { open_database() } match {
+        Exn.result { open_database() } match {
           case Exn.Res(db) =>
             val db_name = db.toString
             db.close()
@@ -1036,7 +1036,7 @@
       for (file_group <- file_groups) {
         val log_files =
           Par_List.map[JFile, Exn.Result[Log_File]](
-            file => Exn.capture { Log_File(file) }, file_group)
+            file => Exn.result { Log_File(file) }, file_group)
         db.transaction {
           for (case Exn.Res(log_file) <- log_files) {
             progress.echo("Log " + quote(log_file.name), verbose = true)

--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 12 20:58:15 2023 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 12 21:11:59 2023 +0200
@@ -481,7 +481,7 @@
 
     def run_task(start_date: Date, task: Logger_Task): Unit = {
       val logger = start_logger(start_date, task.name)
-      val res = Exn.capture { task.body(logger) }
+      val res = Exn.result { task.body(logger) }
       val end_date = Date.now()
       val err =
         res match {

--- a/src/Pure/General/http.scala	Thu Oct 12 20:58:15 2023 +0200
+++ b/src/Pure/General/http.scala	Thu Oct 12 21:11:59 2023 +0200
@@ -243,7 +243,7 @@
       val input = using(http.getRequestBody)(Bytes.read_stream(_))
       if (http.getRequestMethod == method) {
         val request = new Request(server_name, name, uri, input)
-        Exn.capture(apply(request)) match {
+        Exn.result(apply(request)) match {
           case Exn.Res(Some(response)) =>
             response.write(http, 200)
           case Exn.Res(None) =>

--- a/src/Pure/General/mercurial.scala	Thu Oct 12 20:58:15 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Thu Oct 12 21:11:59 2023 +0200
@@ -29,7 +29,7 @@
       val server_root = Future.promise[String]
       Isabelle_Thread.fork("hg") {
         val process =
-          Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
+          Exn.result { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
         server_process.fulfill_result(process)
         Exn.release(process).result(progress_stdout =
           line => if (!server_root.is_finished) {