# HG changeset patch
# User wenzelm
# Date 1614010745 -3600
# Node ID dcadb3243cfa97fc54bb6f2541fb0d73d2037176
# Parent  22417b6314539a67b3c06606b9093ac19378a07a
tuned;

diff -r 22417b631453 -r dcadb3243cfa src/Pure/Tools/jedit.ML
--- a/src/Pure/Tools/jedit.ML	Mon Feb 22 17:17:30 2021 +0100
+++ b/src/Pure/Tools/jedit.ML	Mon Feb 22 17:19:05 2021 +0100
@@ -35,10 +35,13 @@
 val xml_file = XML.parse o File.read;
 
 fun xml_resource name =
-  let val script = "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name in
-    (case Isabelle_System.bash_output script of
-      (txt, 0) => XML.parse txt
-    | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc))
+  let
+    val res =
+      Isabelle_System.bash_process ("unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name);
+    val rc = Process_Result.rc res;
+  in
+    res |> Process_Result.check |> Process_Result.out |> XML.parse
+      handle ERROR _ => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)
   end;