more accurate patch: change jEdit source directory and copy to installation directory;
authorwenzelm
Sat, 15 Feb 2025 14:17:38 +0100
changeset 82180 1fad64843239
parent 82179 bff32e50fe14
child 82181 a0d1d772ccab
more accurate patch: change jEdit source directory and copy to installation directory;
src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Sat Feb 15 14:00:24 2025 +0100
+++ b/src/Pure/Admin/component_jedit.scala	Sat Feb 15 14:17:38 2025 +0100
@@ -121,6 +121,7 @@
 
     val jedit_dir = Isabelle_System.make_directory(component_path + Path.basic(jedit))
     val jedit_patched_dir = component_path + Path.basic(jedit_patched)
+    val source_dir = jedit_patched_dir + Path.basic("jEdit")
 
     def download_jedit(dir: Path, name: String, target_name: String = ""): Path = {
       val jedit_name = jedit + name
@@ -149,7 +150,6 @@
 
       Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir)
 
-      val source_dir = jedit_patched_dir + Path.basic("jEdit")
       val source_org_dir = source_dir + Path.basic("org")
       val tmp_source_dir = tmp_dir + Path.basic("jEdit")
 
@@ -216,7 +216,7 @@
     val drop_encodings =
       Charset.availableCharsets().keySet().asScala.toList.sorted.filterNot(keep_encodings.contains)
 
-    File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"),
+    File.write(source_dir + Path.explode("properties/jEdit.props"),
 """#jEdit properties
 autoReloadDialog=false
 buffer.deepIndent=false
@@ -412,7 +412,7 @@
 xml-insert-closing-tag.shortcut=
 """)
 
-    val modes_dir = jedit_patched_dir + Path.basic("modes")
+    val modes_dir = source_dir + Path.basic("modes")
 
     Mode.list.foreach(_.write(modes_dir))
 
@@ -443,6 +443,12 @@
       else List(line))
     }
 
+    for (name <- List("keymaps", "macros", "modes", "properties", "startup")) {
+      val path = Path.explode(name)
+      Isabelle_System.rm_tree(jedit_patched_dir + path)
+      Isabelle_System.copy_dir(source_dir + path, jedit_patched_dir)
+    }
+
 
     /* doc */