# HG changeset patch
# User wenzelm
# Date 1671200049 -3600
# Node ID 90abc28523d735276854f6d4c5830eae6008ded0
# Parent  f8826fc8c4191cafa8cc8100596bddba7bafc62e
tuned names: avoid overlap with instances of class Resources;

diff -r f8826fc8c419 -r 90abc28523d7 src/Pure/Tools/jedit.ML
--- a/src/Pure/Tools/jedit.ML	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Pure/Tools/jedit.ML	Fri Dec 16 15:14:09 2022 +0100
@@ -40,7 +40,7 @@
     (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"]
+    (parse_resources o \<^scala>\<open>jEdit.resource\<close>) ["actions.xml", "dockables.xml"]
     |> sort_strings);
 
 fun get_actions () = Lazy.force lazy_actions;
diff -r f8826fc8c419 -r 90abc28523d7 src/Tools/jEdit/src/jedit_jar.scala
--- a/src/Tools/jEdit/src/jedit_jar.scala	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_jar.scala	Fri Dec 16 15:14:09 2022 +0100
@@ -19,10 +19,10 @@
     else using(s)(File.read_stream)
   }
 
-  object JEdit_Resources extends Scala.Fun_Strings("jEdit.resources") {
+  object JEdit_Resource extends Scala.Fun_Strings("jEdit.resource") {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = args.map(get_resource)
   }
 
-  class Scala_Functions extends Scala.Functions(JEdit_Resources)
+  class Scala_Functions extends Scala.Functions(JEdit_Resource)
 }