diff -r bff32e50fe14 -r 1fad64843239 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 */