more direct access to jEdit jar resources, without unzip;

--- a/etc/build.props	Thu Dec 01 11:36:45 2022 +0100
+++ b/etc/build.props	Sun Dec 04 14:15:12 2022 +0100
@@ -264,6 +264,7 @@
   src/Tools/jEdit/src/isabelle_vfs.scala \
   src/Tools/jEdit/src/jedit_bibtex.scala \
   src/Tools/jEdit/src/jedit_editor.scala \
+  src/Tools/jEdit/src/jedit_jar.scala \
   src/Tools/jEdit/src/jedit_lib.scala \
   src/Tools/jEdit/src/jedit_main.scala \
   src/Tools/jEdit/src/jedit_options.scala \
@@ -317,6 +318,7 @@
   isabelle.Tools \
   isabelle.jedit.JEdit_Plugin0 \
   isabelle.jedit.JEdit_Plugin1 \
+  isabelle.jedit.JEdit_JAR$Scala_Functions \
   isabelle.nitpick.Kodkod$Handler \
   isabelle.nitpick.Scala_Functions \
   isabelle.spark.SPARK$Load_Command1 \

--- a/src/Pure/Tools/jedit.ML	Thu Dec 01 11:36:45 2022 +0100
+++ b/src/Pure/Tools/jedit.ML	Sun Dec 04 14:15:12 2022 +0100
@@ -30,29 +30,17 @@
   | parse_dockables _ = [];
 
 
-(* XML resources *)
-
-val xml_file = XML.parse o File.read;
+(* actions *)
 
-fun xml_resource name =
-  let
-    val res =
-      Isabelle_System.bash_process (Bash.script ("unzip -p \"$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;
-
-
-(* actions *)
+fun parse_resources [actions, dockables] =
+  parse_actions (XML.parse actions) @ parse_dockables (XML.parse dockables);
 
 val lazy_actions =
   Lazy.lazy (fn () =>
-    (parse_actions (xml_file \<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>) @
-      parse_dockables (xml_file \<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>) @
-      parse_actions (xml_resource "org/gjt/sp/jedit/actions.xml") @
-      parse_dockables (xml_resource "org/gjt/sp/jedit/dockables.xml"))
+    (parse_resources o map File.read)
+      [\<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>,
+       \<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>] @
+    (parse_resources o \<^scala>\<open>jEdit.resources\<close>) ["actions.xml", "dockables.xml"]
     |> sort_strings);
 
 fun get_actions () = Lazy.force lazy_actions;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_jar.scala	Sun Dec 04 14:15:12 2022 +0100
@@ -0,0 +1,28 @@
+/*  Title:      Tools/jEdit/src/jedit_jar.scala
+    Author:     Makarius
+
+Offline access to jEdit jar resources.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+object JEdit_JAR {
+  /* jEdit jar resources */
+
+  def get_resource(name: String): String = {
+    val s = classOf[org.gjt.sp.jedit.jEdit].getResourceAsStream(name)
+    if (s == null) error("Bad jEdit resource: " + quote(name))
+    else using(s)(File.read_stream)
+  }
+
+  object JEdit_Resources extends Scala.Fun_Strings("jEdit.resources") {
+    val here = Scala_Project.here
+    def apply(args: List[String]): List[String] = args.map(get_resource)
+  }
+
+  class Scala_Functions extends Scala.Functions(JEdit_Resources)
+}