# HG changeset patch
# User wenzelm
# Date 1620677892 -7200
# Node ID ff716ecb08053b1a9fd6045eb1c45afd333f7e44
# Parent  af82097b4adc2926471e281a119d074b6728a96b
put more resources into jedit_build component;

diff -r af82097b4adc -r ff716ecb0805 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon May 10 20:09:47 2021 +0200
+++ b/Admin/components/components.sha1	Mon May 10 22:18:12 2021 +0200
@@ -205,6 +205,7 @@
 533b1ee6459f59bcbe4f09e214ad2cb990fb6952  jedit_build-20200908.tar.gz
 f9966b5ed26740bb5b8bddbfe947fcefaea43d4d  jedit_build-20201223.tar.gz
 0bdbd36eda5992396e9c6b66aa24259d4dd7559c  jedit_build-20210201.tar.gz
+a0744f1948abdde4bfb51dd4769b619e7444baf1  jedit_build-20210510-1.tar.gz
 837d6c8f72ecb21ad59a2544c69aadc9f05684c6  jedit_build-20210510.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
diff -r af82097b4adc -r ff716ecb0805 Admin/components/main
--- a/Admin/components/main	Mon May 10 20:09:47 2021 +0200
+++ b/Admin/components/main	Mon May 10 22:18:12 2021 +0200
@@ -9,7 +9,7 @@
 idea-icons-20210508
 isabelle_fonts-20210322
 jdk-15.0.2+7
-jedit_build-20210510
+jedit_build-20210510-1
 jfreechart-1.5.1
 jortho-1.0-2
 kodkodi-1.5.6-1
diff -r af82097b4adc -r ff716ecb0805 src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Mon May 10 20:09:47 2021 +0200
+++ b/src/Pure/Admin/build_jedit.scala	Mon May 10 22:18:12 2021 +0200
@@ -9,6 +9,77 @@
 
 object Build_JEdit
 {
+  /* modes */
+
+  object Mode
+  {
+    val empty: Mode = new Mode("", "", Nil)
+
+    val init: Mode =
+      empty +
+        ("noWordSep" -> """_'?⇩\^<>""") +
+        ("unalignedOpenBrackets" -> "{[(«‹⟨⌈⌊⦇⟦⦃⦉") +
+        ("unalignedCloseBrackets" -> "⦊⦄⟧⦈⌋⌉⟩›»)]}") +
+        ("tabSize" -> "2") +
+        ("indentSize" -> "2")
+
+    val list: List[Mode] =
+    {
+      val isabelle_news: Mode = init.define("isabelle-news", "Isabelle NEWS")
+
+      val isabelle: Mode =
+        init.define("isabelle", "Isabelle theory") +
+          ("commentStart" -> "(*") +
+          ("commentEnd" -> "*)")
+
+      val isabelle_ml: Mode = isabelle.define("isabelle-ml", "Isabelle/ML")
+
+      val isabelle_root: Mode = isabelle.define("isabelle-root", "Isabelle session root")
+
+      val isabelle_options: Mode = isabelle.define("isabelle-options", "Isabelle options")
+
+      val sml: Mode =
+        init.define("sml", "Standard ML") +
+          ("commentStart" -> "(*") +
+          ("commentEnd" -> "*)") +
+          ("noWordSep" -> "_'")
+
+      List(isabelle_news, isabelle, isabelle_ml, isabelle_root, isabelle_options, sml)
+    }
+  }
+
+  final case class Mode private(name: String, description: String, rev_props: Properties.T)
+  {
+    override def toString: String = name
+
+    def define(a: String, b: String): Mode = new Mode(a, b, rev_props)
+
+    def + (entry: Properties.Entry): Mode =
+      new Mode(name, description, Properties.put(rev_props, entry))
+
+    def write(dir: Path): Unit =
+    {
+      require(name.nonEmpty && description.nonEmpty, "Bad Isabelle/jEdit mode content")
+
+      val properties =
+        rev_props.reverse.map(p =>
+          Symbol.spaces(4) +
+          XML.string_of_tree(XML.elem(Markup("PROPERTY", List("NAME" -> p._1, "VALUE" -> p._2)))))
+
+      File.write(dir + Path.basic(name).xml,
+"""<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+
+<!-- """ + XML.text(description) + """ mode -->
+<MODE>
+  <PROPS>""" + properties.mkString("\n", "\n", "\n") + """
+  </PROPS>
+</MODE>
+""")
+    }
+  }
+
+
   /* build jEdit component */
 
   private val download_jars: List[(String, String)] =
@@ -48,13 +119,13 @@
     val jedit_dir = Isabelle_System.make_directory(component_dir + Path.basic(jedit))
     val jedit_patched_dir = component_dir + Path.basic(jedit_patched)
 
-    def download_jedit(dir: Path, name: String): Path =
+    def download_jedit(dir: Path, name: String, target_name: String = ""): Path =
     {
       val jedit_name = jedit + name
       val url =
         "https://sourceforge.net/projects/jedit/files/jedit/" +
           version + "/" + jedit_name + "/download"
-      val path = dir + Path.basic(jedit_name)
+      val path = dir + Path.basic(proper_string(target_name) getOrElse jedit_name)
       Isabelle_System.download_file(url, path, progress = progress)
       path
     }
@@ -90,6 +161,12 @@
           cwd = source_dir.file, echo = true).check
       }
 
+      for { theme <- List("classic", "tango") } {
+        val path = Path.explode("org/gjt/sp/jedit/icons/themes/" + theme + "/32x32/apps/isabelle.gif")
+        Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle_transparent-32.gif"),
+          source_dir + path)
+      }
+
       progress.echo("Building jEdit ...")
       Isabelle_System.copy_dir(source_dir, tmp_source_dir)
       progress.bash("env JAVA_HOME=" + File.bash_platform_path(java_home) + " ant",
@@ -118,6 +195,407 @@
     }
 
 
+    /* resources */
+
+    File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"),
+"""#jEdit properties
+autoReloadDialog=false
+buffer.deepIndent=false
+buffer.encoding=UTF-8-Isabelle
+buffer.indentSize=2
+buffer.lineSeparator=\n
+buffer.maxLineLen=100
+buffer.noTabs=true
+buffer.sidekick.keystroke-parse=false
+buffer.tabSize=2
+buffer.undoCount=1000
+close-docking-area.shortcut2=C+e C+CIRCUMFLEX
+complete-word.shortcut=
+console.dock-position=floating
+console.encoding=UTF-8
+console.font=Isabelle DejaVu Sans Mono
+console.fontsize=14
+delete-line.shortcut=A+d
+delete.shortcut2=C+d
+encoding.opt-out.Big5-HKSCS=true
+encoding.opt-out.Big5=true
+encoding.opt-out.COMPOUND_TEXT=true
+encoding.opt-out.EUC-JP=true
+encoding.opt-out.EUC-KR=true
+encoding.opt-out.GB2312=true
+encoding.opt-out.GB18030=true
+encoding.opt-out.GBK=true
+encoding.opt-out.IBM-Thai=true
+encoding.opt-out.IBM00858=true
+encoding.opt-out.IBM037=true
+encoding.opt-out.IBM01140=true
+encoding.opt-out.IBM01141=true
+encoding.opt-out.IBM01142=true
+encoding.opt-out.IBM01143=true
+encoding.opt-out.IBM01144=true
+encoding.opt-out.IBM01145=true
+encoding.opt-out.IBM01146=true
+encoding.opt-out.IBM01147=true
+encoding.opt-out.IBM01148=true
+encoding.opt-out.IBM01149=true
+encoding.opt-out.IBM273=true
+encoding.opt-out.IBM277=true
+encoding.opt-out.IBM278=true
+encoding.opt-out.IBM280=true
+encoding.opt-out.IBM284=true
+encoding.opt-out.IBM285=true
+encoding.opt-out.IBM297=true
+encoding.opt-out.IBM420=true
+encoding.opt-out.IBM424=true
+encoding.opt-out.IBM437=true
+encoding.opt-out.IBM500=true
+encoding.opt-out.IBM775=true
+encoding.opt-out.IBM850=true
+encoding.opt-out.IBM852=true
+encoding.opt-out.IBM855=true
+encoding.opt-out.IBM857=true
+encoding.opt-out.IBM860=true
+encoding.opt-out.IBM861=true
+encoding.opt-out.IBM862=true
+encoding.opt-out.IBM863=true
+encoding.opt-out.IBM864=true
+encoding.opt-out.IBM865=true
+encoding.opt-out.IBM866=true
+encoding.opt-out.IBM868=true
+encoding.opt-out.IBM869=true
+encoding.opt-out.IBM870=true
+encoding.opt-out.IBM871=true
+encoding.opt-out.IBM918=true
+encoding.opt-out.IBM1026=true
+encoding.opt-out.IBM1047=true
+encoding.opt-out.ISO-2022-CN=true
+encoding.opt-out.ISO-2022-JP-2=true
+encoding.opt-out.ISO-2022-JP=true
+encoding.opt-out.ISO-2022-KR=true
+encoding.opt-out.ISO-8859-2=true
+encoding.opt-out.ISO-8859-3=true
+encoding.opt-out.ISO-8859-4=true
+encoding.opt-out.ISO-8859-5=true
+encoding.opt-out.ISO-8859-6=true
+encoding.opt-out.ISO-8859-7=true
+encoding.opt-out.ISO-8859-8=true
+encoding.opt-out.ISO-8859-9=true
+encoding.opt-out.ISO-8859-13=true
+encoding.opt-out.JIS_X0201=true
+encoding.opt-out.JIS_X0212-1990=true
+encoding.opt-out.KOI8-R=true
+encoding.opt-out.KOI8-U=true
+encoding.opt-out.Shift_JIS=true
+encoding.opt-out.TIS-620=true
+encoding.opt-out.UTF-16=true
+encoding.opt-out.UTF-16BE=true
+encoding.opt-out.UTF-16LE=true
+encoding.opt-out.UTF-32=true
+encoding.opt-out.UTF-32BE=true
+encoding.opt-out.UTF-32LE=true
+encoding.opt-out.X-UTF-32BE-BOM=true
+encoding.opt-out.X-UTF-32LE-BOM=true
+encoding.opt-out.windows-31j=true
+encoding.opt-out.windows-1250=true
+encoding.opt-out.windows-1251=true
+encoding.opt-out.windows-1253=true
+encoding.opt-out.windows-1254=true
+encoding.opt-out.windows-1255=true
+encoding.opt-out.windows-1256=true
+encoding.opt-out.windows-1257=true
+encoding.opt-out.windows-1258=true
+encoding.opt-out.x-Big5-Solaris=true
+encoding.opt-out.x-EUC-TW=true
+encoding.opt-out.x-IBM737=true
+encoding.opt-out.x-IBM834=true
+encoding.opt-out.x-IBM856=true
+encoding.opt-out.x-IBM874=true
+encoding.opt-out.x-IBM875=true
+encoding.opt-out.x-IBM921=true
+encoding.opt-out.x-IBM922=true
+encoding.opt-out.x-IBM930=true
+encoding.opt-out.x-IBM933=true
+encoding.opt-out.x-IBM935=true
+encoding.opt-out.x-IBM937=true
+encoding.opt-out.x-IBM939=true
+encoding.opt-out.x-IBM942=true
+encoding.opt-out.x-IBM942C=true
+encoding.opt-out.x-IBM943=true
+encoding.opt-out.x-IBM943C=true
+encoding.opt-out.x-IBM948=true
+encoding.opt-out.x-IBM949=true
+encoding.opt-out.x-IBM949C=true
+encoding.opt-out.x-IBM950=true
+encoding.opt-out.x-IBM964=true
+encoding.opt-out.x-IBM970=true
+encoding.opt-out.x-IBM1006=true
+encoding.opt-out.x-IBM1025=true
+encoding.opt-out.x-IBM1046=true
+encoding.opt-out.x-IBM1097=true
+encoding.opt-out.x-IBM1098=true
+encoding.opt-out.x-IBM1112=true
+encoding.opt-out.x-IBM1122=true
+encoding.opt-out.x-IBM1123=true
+encoding.opt-out.x-IBM1124=true
+encoding.opt-out.x-IBM1381=true
+encoding.opt-out.x-IBM1383=true
+encoding.opt-out.x-IBM33722=true
+encoding.opt-out.x-ISCII91=true
+encoding.opt-out.x-ISO-2022-CN-CNS=true
+encoding.opt-out.x-ISO-2022-CN-GB=true
+encoding.opt-out.x-JIS0208=true
+encoding.opt-out.x-JISAutoDetect=true
+encoding.opt-out.x-Johab=true
+encoding.opt-out.x-MS932_0213=true
+encoding.opt-out.x-MS950-HKSCS=true
+encoding.opt-out.x-MacArabic=true
+encoding.opt-out.x-MacCentralEurope=true
+encoding.opt-out.x-MacCroatian=true
+encoding.opt-out.x-MacCyrillic=true
+encoding.opt-out.x-MacDingbat=true
+encoding.opt-out.x-MacGreek=true
+encoding.opt-out.x-MacHebrew=true
+encoding.opt-out.x-MacIceland=true
+encoding.opt-out.x-MacRoman=true
+encoding.opt-out.x-MacRomania=true
+encoding.opt-out.x-MacSymbol=true
+encoding.opt-out.x-MacThai=true
+encoding.opt-out.x-MacTurkish=true
+encoding.opt-out.x-MacUkraine=true
+encoding.opt-out.x-PCK=true
+encoding.opt-out.x-SJIS_0213=true
+encoding.opt-out.x-UTF-16LE-BOM=true
+encoding.opt-out.x-euc-jp-linux=true
+encoding.opt-out.x-eucJP-Open=true
+encoding.opt-out.x-iso-8859-11=true
+encoding.opt-out.x-mswin-936=true
+encoding.opt-out.x-windows-874=true
+encoding.opt-out.x-windows-949=true
+encoding.opt-out.x-windows-950=true
+encoding.opt-out.x-windows-50220=true
+encoding.opt-out.x-windows-50221=true
+encoding.opt-out.x-windows-iso2022jp=true
+encodingDetectors=BOM XML-PI buffer-local-property
+end.shortcut=
+expand-abbrev.shortcut2=CA+SPACE
+expand-folds.shortcut=
+fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
+firstTime=false
+focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
+foldPainter=Circle
+gatchan.highlight.overview=false
+helpviewer.font=Isabelle DejaVu Serif
+helpviewer.fontsize=12
+home.shortcut=
+hypersearch-results.dock-position=right
+insert-newline-indent.shortcut=
+insert-newline.shortcut=
+isabelle-debugger.dock-position=floating
+isabelle-documentation.dock-position=left
+isabelle-export-browser.label=Browse theory exports
+isabelle-output.dock-position=bottom
+isabelle-output.height=174
+isabelle-output.width=412
+isabelle-query.dock-position=bottom
+isabelle-session-browser.label=Browse session information
+isabelle-simplifier-trace.dock-position=floating
+isabelle-sledgehammer.dock-position=bottom
+isabelle-state.dock-position=right
+isabelle-symbols.dock-position=bottom
+isabelle-theories.dock-position=right
+isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
+isabelle.complete-word.label=Complete word
+isabelle.complete.label=Complete Isabelle text
+isabelle.complete.shortcut2=C+b
+isabelle.control-bold.label=Control bold
+isabelle.control-bold.shortcut=C+e RIGHT
+isabelle.control-emph.label=Control emphasized
+isabelle.control-emph.shortcut=C+e LEFT
+isabelle.control-reset.label=Control reset
+isabelle.control-reset.shortcut=C+e BACK_SPACE
+isabelle.control-sub.label=Control subscript
+isabelle.control-sub.shortcut=C+e DOWN
+isabelle.control-sup.label=Control superscript
+isabelle.control-sup.shortcut=C+e UP
+isabelle.decrease-font-size.label=Decrease font size
+isabelle.decrease-font-size.shortcut2=C+SUBTRACT
+isabelle.decrease-font-size.shortcut=C+MINUS
+isabelle.decrease-font-size2.label=Decrease font size (clone)
+isabelle.draft.label=Show draft in browser
+isabelle.exclude-word-permanently.label=Exclude word permanently
+isabelle.exclude-word.label=Exclude word
+isabelle.first-error.label=Go to first error
+isabelle.first-error.shortcut=CS+a
+isabelle.goto-entity.label=Go to definition of formal entity at caret
+isabelle.goto-entity.shortcut=CS+d
+isabelle.include-word-permanently.label=Include word permanently
+isabelle.include-word.label=Include word
+isabelle.increase-font-size.label=Increase font size
+isabelle.increase-font-size.shortcut2=C+ADD
+isabelle.increase-font-size.shortcut=C+PLUS
+isabelle.increase-font-size2.label=Increase font size (clone)
+isabelle.increase-font-size2.shortcut=C+EQUALS
+isabelle.java-monitor.label=Java/VM monitor
+isabelle.last-error.label=Go to last error
+isabelle.last-error.shortcut=CS+z
+isabelle.message.label=Show message
+isabelle.message.shortcut=CS+m
+isabelle.newline.label=Newline with indentation of Isabelle keywords
+isabelle.newline.shortcut=ENTER
+isabelle.next-error.label=Go to next error
+isabelle.next-error.shortcut=CS+n
+isabelle.options.label=Isabelle options
+isabelle.prev-error.label=Go to previous error
+isabelle.prev-error.shortcut=CS+p
+isabelle.preview.label=Show preview in browser
+isabelle.reset-continuous-checking.label=Reset continuous checking
+isabelle.reset-font-size.label=Reset font size
+isabelle.reset-node-required.label=Reset node required
+isabelle.reset-words.label=Reset non-permanent words
+isabelle.select-entity.label=Select all occurences of formal entity at caret
+isabelle.select-entity.shortcut=CS+ENTER
+isabelle.set-continuous-checking.label=Set continuous checking
+isabelle.set-node-required.label=Set node required
+isabelle.toggle-breakpoint.label=Toggle Breakpoint
+isabelle.toggle-continuous-checking.label=Toggle continuous checking
+isabelle.toggle-continuous-checking.shortcut=C+e ENTER
+isabelle.toggle-node-required.label=Toggle node required
+isabelle.toggle-node-required.shortcut=C+e SPACE
+isabelle.tooltip.label=Show tooltip
+isabelle.tooltip.shortcut=CS+b
+isabelle.update-state.label=Update state output
+isabelle.update-state.shortcut=S+ENTER
+lang.usedefaultlocale=false
+largefilemode=full
+line-end.shortcut=END
+line-home.shortcut=HOME
+logo.icon.medium=32x32/apps/isabelle.gif
+lookAndFeel=com.formdev.flatlaf.FlatLightLaf
+match-bracket.shortcut2=C+9
+metal.primary.font=Isabelle DejaVu Sans
+metal.primary.fontsize=12
+metal.secondary.font=Isabelle DejaVu Sans
+metal.secondary.fontsize=12
+navigator.showOnToolbar=true
+new-file-in-mode.shortcut=
+next-bracket.shortcut2=C+e C+9
+options.shortcuts.deletekeymap.label=Delete
+options.shortcuts.duplicatekeymap.dialog.title=Keymap name
+options.shortcuts.duplicatekeymap.label=Duplicate
+options.shortcuts.resetkeymap.dialog.title=Reset keymap
+options.shortcuts.resetkeymap.label=Reset
+options.textarea.lineSpacing=1
+plugin-blacklist.MacOSX.jar=true
+plugin.MacOSXPlugin.altDispatcher=false
+plugin.MacOSXPlugin.disableOption=true
+prev-bracket.shortcut2=C+e C+8
+print.font=Isabelle DejaVu Sans Mono
+print.glyphVector=true
+recent-buffer.shortcut2=C+CIRCUMFLEX
+restore.remote=false
+restore=false
+search.subdirs.toggle=true
+select-block.shortcut2=C+8
+sidekick-tree.dock-position=right
+sidekick.auto-complete-popup-get-focus=true
+sidekick.buffer-save-parse=true
+sidekick.complete-delay=0
+sidekick.complete-instant.toggle=false
+sidekick.complete-popup.accept-characters=\\t
+sidekick.complete-popup.insert-characters=
+sidekick.persistentFilter=true
+sidekick.showFilter=true
+sidekick.splitter.location=721
+systrayicon=false
+tip.show=false
+toggle-full-screen.shortcut2=S+F11
+toggle-multi-select.shortcut2=C+NUMBER_SIGN
+toggle-rect-select.shortcut2=A+NUMBER_SIGN
+twoStageSave=false
+vfs.browser.dock-position=left
+vfs.favorite.0.type=1
+vfs.favorite.0=$ISABELLE_HOME
+vfs.favorite.1.type=1
+vfs.favorite.1=$ISABELLE_HOME_USER
+vfs.favorite.2.type=1
+vfs.favorite.2=$JEDIT_HOME
+vfs.favorite.3.type=1
+vfs.favorite.3=$JEDIT_SETTINGS
+vfs.favorite.4.type=1
+vfs.favorite.4=isabelle-export:
+vfs.favorite.5.type=1
+vfs.favorite.5=isabelle-session:
+view.antiAlias=subpixel HRGB
+view.blockCaret=true
+view.caretBlink=false
+view.docking.framework=PIDE
+view.eolMarkers=false
+view.extendedState=0
+view.font=Isabelle DejaVu Sans Mono
+view.fontsize=18
+view.fracFontMetrics=false
+view.gutter.font=Isabelle DejaVu Sans Mono
+view.gutter.fontsize=12
+view.gutter.lineNumbers=false
+view.gutter.selectionAreaWidth=18
+view.height=850
+view.middleMousePaste=true
+view.showToolbar=true
+view.status.memory.background=#666699
+view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
+view.thickCaret=true
+view.width=1200
+xml-insert-closing-tag.shortcut=
+""")
+
+    val modes_dir = jedit_patched_dir + Path.basic("modes")
+
+    Mode.list.foreach(_.write(modes_dir))
+
+    File.change_lines(modes_dir + Path.basic("catalog"),
+      _.flatMap(line =>
+          if (line.containsSlice("FILE=\"ml.xml\"") ||
+            line.containsSlice("FILE_NAME_GLOB=\"*.{sml,ml}\"") ||
+            line.containsSlice("FILE_NAME_GLOB=\"*.ftl\"")) Nil
+          else if (line.containsSlice("NAME=\"jamon\"")) {
+            List(
+              """<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>""",
+              "",
+              """<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>""",
+              "",
+              """<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>""",
+              "",
+              """<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>""",
+              "",
+              """<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>""",
+              "",
+              line)
+          }
+          else if (line.containsSlice("NAME=\"sqr\"")) {
+            List(
+              """<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>""",
+              "",
+              line)
+          }
+          else List(line)))
+
+
+    /* doc */
+
+    val doc_dir = jedit_patched_dir + Path.basic("doc")
+
+    download_jedit(doc_dir, "manual-a4.pdf", target_name = "jedit-manual.pdf")
+
+    Isabelle_System.copy_file(
+      doc_dir + Path.basic("CHANGES.txt"), doc_dir + Path.basic("jedit-changes"))
+
+    File.write(doc_dir + Path.basic("Contents"),
+"""Original jEdit Documentation
+  jedit-manual    jEdit User's Guide
+  jedit-changes   jEdit Version History
+
+""")
+
 
     /* diff */
 
@@ -129,14 +607,6 @@
     if (!original) Isabelle_System.rm_tree(jedit_dir)
 
 
-    /* doc */
-
-    val doc_dir = Isabelle_System.make_directory(component_dir + Path.explode("doc"))
-
-    download_jedit(doc_dir, "manual-a4.pdf")
-    download_jedit(doc_dir, "manual-letter.pdf")
-
-
     /* etc */
 
     val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
diff -r af82097b4adc -r ff716ecb0805 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon May 10 20:09:47 2021 +0200
+++ b/src/Pure/General/file.scala	Mon May 10 22:18:12 2021 +0200
@@ -286,7 +286,11 @@
     if (x != y) write(file, y)
   }
 
+  def change_lines(file: JFile, f: List[String] => List[String]): Unit =
+    change(file, text => cat_lines(f(split_lines(text))))
+
   def change(path: Path, f: String => String): Unit = change(path.file, f)
+  def change_lines(path: Path, f: List[String] => List[String]): Unit = change_lines(path.file, f)
 
 
   /* append */
diff -r af82097b4adc -r ff716ecb0805 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon May 10 20:09:47 2021 +0200
+++ b/src/Pure/General/path.scala	Mon May 10 22:18:12 2021 +0200
@@ -213,6 +213,7 @@
     }
 
   def xz: Path = ext("xz")
+  def xml: Path = ext("xml")
   def html: Path = ext("html")
   def tex: Path = ext("tex")
   def pdf: Path = ext("pdf")
diff -r af82097b4adc -r ff716ecb0805 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon May 10 20:09:47 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon May 10 22:18:12 2021 +0200
@@ -4,7 +4,6 @@
 #
 # DESCRIPTION: Isabelle/jEdit interface wrapper
 
-
 ## sources
 
 declare -a SOURCES0=(
@@ -80,14 +79,7 @@
   "src/Tools/jEdit/src/actions.xml"
   "src/Tools/jEdit/src/dockables.xml"
   "src/Tools/jEdit/src/Isabelle.props"
-  "src/Tools/jEdit/src/jEdit.props"
   "src/Tools/jEdit/src/services.xml"
-  "src/Tools/jEdit/src/modes/isabelle-ml.xml"
-  "src/Tools/jEdit/src/modes/isabelle-news.xml"
-  "src/Tools/jEdit/src/modes/isabelle-options.xml"
-  "src/Tools/jEdit/src/modes/isabelle-root.xml"
-  "src/Tools/jEdit/src/modes/isabelle.xml"
-  "src/Tools/jEdit/src/modes/sml.xml"
 )
 
 
@@ -334,51 +326,10 @@
   classpath "$TARGET_JAR0"
 
   init_resources "${RESOURCES[@]}"
-  cp src/Tools/jEdit/src/jEdit.props "$TARGET_DIR/properties/."
-  cp -p -R -f "src/Tools/jEdit/src/modes/." "$TARGET_DIR/modes/."
-
-  perl -i -e 'while (<>) {
-    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/ or m/FILE_NAME_GLOB="..ftl"/) { }
-    elsif (m/NAME="javacc"/) {
-      print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!;
-      print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!;
-      print qq!<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n!;
-      print qq!<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n!;
-      print qq!<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n!;
-      print;
-    }
-    elsif (m/NAME="sqr"/) {
-      print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!;
-      print;
-    }
-    else { print; }
-  }' "$TARGET_DIR/modes/catalog"
-
-  (
-    cd "$TARGET_DIR"
-    isabelle_jdk jar -x -f jedit.jar
-    cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
-      "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
-    cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
-      "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
-    isabelle_jdk jar -c -f jedit.jar -e org.gjt.sp.jedit.jEdit org || failed
-    rm -rf META-INF org
-  )
-
   compile_sources "${SOURCES[@]}"
   make_jar "$TARGET_JAR"
 
   target_shasum > "$TARGET_SHASUM"
-
-  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6.0manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf"
-  cp "$TARGET_DIR/doc/CHANGES.txt" "$TARGET_DIR/doc/jedit-changes"
-  cat > "$TARGET_DIR/doc/Contents" <<EOF
-Original jEdit Documentation
-  jedit-manual    jEdit 5.6 User's Guide
-  jedit-changes   jEdit 5.6 Version History
-
-EOF
-
 fi
 
 
diff -r af82097b4adc -r ff716ecb0805 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Mon May 10 20:09:47 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,348 +0,0 @@
-#jEdit properties
-autoReloadDialog=false
-buffer.deepIndent=false
-buffer.encoding=UTF-8-Isabelle
-buffer.indentSize=2
-buffer.lineSeparator=\n
-buffer.maxLineLen=100
-buffer.noTabs=true
-buffer.sidekick.keystroke-parse=false
-buffer.tabSize=2
-buffer.undoCount=1000
-close-docking-area.shortcut2=C+e C+CIRCUMFLEX
-complete-word.shortcut=
-console.dock-position=floating
-console.encoding=UTF-8
-console.font=Isabelle DejaVu Sans Mono
-console.fontsize=14
-delete-line.shortcut=A+d
-delete.shortcut2=C+d
-encoding.opt-out.Big5-HKSCS=true
-encoding.opt-out.Big5=true
-encoding.opt-out.COMPOUND_TEXT=true
-encoding.opt-out.EUC-JP=true
-encoding.opt-out.EUC-KR=true
-encoding.opt-out.GB2312=true
-encoding.opt-out.GB18030=true
-encoding.opt-out.GBK=true
-encoding.opt-out.IBM-Thai=true
-encoding.opt-out.IBM00858=true
-encoding.opt-out.IBM037=true
-encoding.opt-out.IBM01140=true
-encoding.opt-out.IBM01141=true
-encoding.opt-out.IBM01142=true
-encoding.opt-out.IBM01143=true
-encoding.opt-out.IBM01144=true
-encoding.opt-out.IBM01145=true
-encoding.opt-out.IBM01146=true
-encoding.opt-out.IBM01147=true
-encoding.opt-out.IBM01148=true
-encoding.opt-out.IBM01149=true
-encoding.opt-out.IBM273=true
-encoding.opt-out.IBM277=true
-encoding.opt-out.IBM278=true
-encoding.opt-out.IBM280=true
-encoding.opt-out.IBM284=true
-encoding.opt-out.IBM285=true
-encoding.opt-out.IBM297=true
-encoding.opt-out.IBM420=true
-encoding.opt-out.IBM424=true
-encoding.opt-out.IBM437=true
-encoding.opt-out.IBM500=true
-encoding.opt-out.IBM775=true
-encoding.opt-out.IBM850=true
-encoding.opt-out.IBM852=true
-encoding.opt-out.IBM855=true
-encoding.opt-out.IBM857=true
-encoding.opt-out.IBM860=true
-encoding.opt-out.IBM861=true
-encoding.opt-out.IBM862=true
-encoding.opt-out.IBM863=true
-encoding.opt-out.IBM864=true
-encoding.opt-out.IBM865=true
-encoding.opt-out.IBM866=true
-encoding.opt-out.IBM868=true
-encoding.opt-out.IBM869=true
-encoding.opt-out.IBM870=true
-encoding.opt-out.IBM871=true
-encoding.opt-out.IBM918=true
-encoding.opt-out.IBM1026=true
-encoding.opt-out.IBM1047=true
-encoding.opt-out.ISO-2022-CN=true
-encoding.opt-out.ISO-2022-JP-2=true
-encoding.opt-out.ISO-2022-JP=true
-encoding.opt-out.ISO-2022-KR=true
-encoding.opt-out.ISO-8859-2=true
-encoding.opt-out.ISO-8859-3=true
-encoding.opt-out.ISO-8859-4=true
-encoding.opt-out.ISO-8859-5=true
-encoding.opt-out.ISO-8859-6=true
-encoding.opt-out.ISO-8859-7=true
-encoding.opt-out.ISO-8859-8=true
-encoding.opt-out.ISO-8859-9=true
-encoding.opt-out.ISO-8859-13=true
-encoding.opt-out.JIS_X0201=true
-encoding.opt-out.JIS_X0212-1990=true
-encoding.opt-out.KOI8-R=true
-encoding.opt-out.KOI8-U=true
-encoding.opt-out.Shift_JIS=true
-encoding.opt-out.TIS-620=true
-encoding.opt-out.UTF-16=true
-encoding.opt-out.UTF-16BE=true
-encoding.opt-out.UTF-16LE=true
-encoding.opt-out.UTF-32=true
-encoding.opt-out.UTF-32BE=true
-encoding.opt-out.UTF-32LE=true
-encoding.opt-out.X-UTF-32BE-BOM=true
-encoding.opt-out.X-UTF-32LE-BOM=true
-encoding.opt-out.windows-31j=true
-encoding.opt-out.windows-1250=true
-encoding.opt-out.windows-1251=true
-encoding.opt-out.windows-1253=true
-encoding.opt-out.windows-1254=true
-encoding.opt-out.windows-1255=true
-encoding.opt-out.windows-1256=true
-encoding.opt-out.windows-1257=true
-encoding.opt-out.windows-1258=true
-encoding.opt-out.x-Big5-Solaris=true
-encoding.opt-out.x-EUC-TW=true
-encoding.opt-out.x-IBM737=true
-encoding.opt-out.x-IBM834=true
-encoding.opt-out.x-IBM856=true
-encoding.opt-out.x-IBM874=true
-encoding.opt-out.x-IBM875=true
-encoding.opt-out.x-IBM921=true
-encoding.opt-out.x-IBM922=true
-encoding.opt-out.x-IBM930=true
-encoding.opt-out.x-IBM933=true
-encoding.opt-out.x-IBM935=true
-encoding.opt-out.x-IBM937=true
-encoding.opt-out.x-IBM939=true
-encoding.opt-out.x-IBM942=true
-encoding.opt-out.x-IBM942C=true
-encoding.opt-out.x-IBM943=true
-encoding.opt-out.x-IBM943C=true
-encoding.opt-out.x-IBM948=true
-encoding.opt-out.x-IBM949=true
-encoding.opt-out.x-IBM949C=true
-encoding.opt-out.x-IBM950=true
-encoding.opt-out.x-IBM964=true
-encoding.opt-out.x-IBM970=true
-encoding.opt-out.x-IBM1006=true
-encoding.opt-out.x-IBM1025=true
-encoding.opt-out.x-IBM1046=true
-encoding.opt-out.x-IBM1097=true
-encoding.opt-out.x-IBM1098=true
-encoding.opt-out.x-IBM1112=true
-encoding.opt-out.x-IBM1122=true
-encoding.opt-out.x-IBM1123=true
-encoding.opt-out.x-IBM1124=true
-encoding.opt-out.x-IBM1381=true
-encoding.opt-out.x-IBM1383=true
-encoding.opt-out.x-IBM33722=true
-encoding.opt-out.x-ISCII91=true
-encoding.opt-out.x-ISO-2022-CN-CNS=true
-encoding.opt-out.x-ISO-2022-CN-GB=true
-encoding.opt-out.x-JIS0208=true
-encoding.opt-out.x-JISAutoDetect=true
-encoding.opt-out.x-Johab=true
-encoding.opt-out.x-MS932_0213=true
-encoding.opt-out.x-MS950-HKSCS=true
-encoding.opt-out.x-MacArabic=true
-encoding.opt-out.x-MacCentralEurope=true
-encoding.opt-out.x-MacCroatian=true
-encoding.opt-out.x-MacCyrillic=true
-encoding.opt-out.x-MacDingbat=true
-encoding.opt-out.x-MacGreek=true
-encoding.opt-out.x-MacHebrew=true
-encoding.opt-out.x-MacIceland=true
-encoding.opt-out.x-MacRoman=true
-encoding.opt-out.x-MacRomania=true
-encoding.opt-out.x-MacSymbol=true
-encoding.opt-out.x-MacThai=true
-encoding.opt-out.x-MacTurkish=true
-encoding.opt-out.x-MacUkraine=true
-encoding.opt-out.x-PCK=true
-encoding.opt-out.x-SJIS_0213=true
-encoding.opt-out.x-UTF-16LE-BOM=true
-encoding.opt-out.x-euc-jp-linux=true
-encoding.opt-out.x-eucJP-Open=true
-encoding.opt-out.x-iso-8859-11=true
-encoding.opt-out.x-mswin-936=true
-encoding.opt-out.x-windows-874=true
-encoding.opt-out.x-windows-949=true
-encoding.opt-out.x-windows-950=true
-encoding.opt-out.x-windows-50220=true
-encoding.opt-out.x-windows-50221=true
-encoding.opt-out.x-windows-iso2022jp=true
-encodingDetectors=BOM XML-PI buffer-local-property
-end.shortcut=
-expand-abbrev.shortcut2=CA+SPACE
-expand-folds.shortcut=
-fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
-firstTime=false
-focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
-foldPainter=Circle
-gatchan.highlight.overview=false
-helpviewer.font=Isabelle DejaVu Serif
-helpviewer.fontsize=12
-home.shortcut=
-hypersearch-results.dock-position=right
-insert-newline-indent.shortcut=
-insert-newline.shortcut=
-isabelle-debugger.dock-position=floating
-isabelle-documentation.dock-position=left
-isabelle-export-browser.label=Browse theory exports
-isabelle-output.dock-position=bottom
-isabelle-output.height=174
-isabelle-output.width=412
-isabelle-query.dock-position=bottom
-isabelle-session-browser.label=Browse session information
-isabelle-simplifier-trace.dock-position=floating
-isabelle-sledgehammer.dock-position=bottom
-isabelle-state.dock-position=right
-isabelle-symbols.dock-position=bottom
-isabelle-theories.dock-position=right
-isabelle.antiquoted_cartouche.label=Make antiquoted cartouche
-isabelle.complete-word.label=Complete word
-isabelle.complete.label=Complete Isabelle text
-isabelle.complete.shortcut2=C+b
-isabelle.control-bold.label=Control bold
-isabelle.control-bold.shortcut=C+e RIGHT
-isabelle.control-emph.label=Control emphasized
-isabelle.control-emph.shortcut=C+e LEFT
-isabelle.control-reset.label=Control reset
-isabelle.control-reset.shortcut=C+e BACK_SPACE
-isabelle.control-sub.label=Control subscript
-isabelle.control-sub.shortcut=C+e DOWN
-isabelle.control-sup.label=Control superscript
-isabelle.control-sup.shortcut=C+e UP
-isabelle.decrease-font-size.label=Decrease font size
-isabelle.decrease-font-size.shortcut2=C+SUBTRACT
-isabelle.decrease-font-size.shortcut=C+MINUS
-isabelle.decrease-font-size2.label=Decrease font size (clone)
-isabelle.draft.label=Show draft in browser
-isabelle.exclude-word-permanently.label=Exclude word permanently
-isabelle.exclude-word.label=Exclude word
-isabelle.first-error.label=Go to first error
-isabelle.first-error.shortcut=CS+a
-isabelle.goto-entity.label=Go to definition of formal entity at caret
-isabelle.goto-entity.shortcut=CS+d
-isabelle.include-word-permanently.label=Include word permanently
-isabelle.include-word.label=Include word
-isabelle.increase-font-size.label=Increase font size
-isabelle.increase-font-size.shortcut2=C+ADD
-isabelle.increase-font-size.shortcut=C+PLUS
-isabelle.increase-font-size2.label=Increase font size (clone)
-isabelle.increase-font-size2.shortcut=C+EQUALS
-isabelle.java-monitor.label=Java/VM monitor
-isabelle.last-error.label=Go to last error
-isabelle.last-error.shortcut=CS+z
-isabelle.message.label=Show message
-isabelle.message.shortcut=CS+m
-isabelle.newline.label=Newline with indentation of Isabelle keywords
-isabelle.newline.shortcut=ENTER
-isabelle.next-error.label=Go to next error
-isabelle.next-error.shortcut=CS+n
-isabelle.options.label=Isabelle options
-isabelle.prev-error.label=Go to previous error
-isabelle.prev-error.shortcut=CS+p
-isabelle.preview.label=Show preview in browser
-isabelle.reset-continuous-checking.label=Reset continuous checking
-isabelle.reset-font-size.label=Reset font size
-isabelle.reset-node-required.label=Reset node required
-isabelle.reset-words.label=Reset non-permanent words
-isabelle.select-entity.label=Select all occurences of formal entity at caret
-isabelle.select-entity.shortcut=CS+ENTER
-isabelle.set-continuous-checking.label=Set continuous checking
-isabelle.set-node-required.label=Set node required
-isabelle.toggle-breakpoint.label=Toggle Breakpoint
-isabelle.toggle-continuous-checking.label=Toggle continuous checking
-isabelle.toggle-continuous-checking.shortcut=C+e ENTER
-isabelle.toggle-node-required.label=Toggle node required
-isabelle.toggle-node-required.shortcut=C+e SPACE
-isabelle.tooltip.label=Show tooltip
-isabelle.tooltip.shortcut=CS+b
-isabelle.update-state.label=Update state output
-isabelle.update-state.shortcut=S+ENTER
-lang.usedefaultlocale=false
-largefilemode=full
-line-end.shortcut=END
-line-home.shortcut=HOME
-logo.icon.medium=32x32/apps/isabelle.gif
-lookAndFeel=com.formdev.flatlaf.FlatLightLaf
-match-bracket.shortcut2=C+9
-metal.primary.font=Isabelle DejaVu Sans
-metal.primary.fontsize=12
-metal.secondary.font=Isabelle DejaVu Sans
-metal.secondary.fontsize=12
-navigator.showOnToolbar=true
-new-file-in-mode.shortcut=
-next-bracket.shortcut2=C+e C+9
-options.shortcuts.deletekeymap.label=Delete
-options.shortcuts.duplicatekeymap.dialog.title=Keymap name
-options.shortcuts.duplicatekeymap.label=Duplicate
-options.shortcuts.resetkeymap.dialog.title=Reset keymap
-options.shortcuts.resetkeymap.label=Reset
-options.textarea.lineSpacing=1
-plugin-blacklist.MacOSX.jar=true
-plugin.MacOSXPlugin.altDispatcher=false
-plugin.MacOSXPlugin.disableOption=true
-prev-bracket.shortcut2=C+e C+8
-print.font=Isabelle DejaVu Sans Mono
-print.glyphVector=true
-recent-buffer.shortcut2=C+CIRCUMFLEX
-restore.remote=false
-restore=false
-search.subdirs.toggle=true
-select-block.shortcut2=C+8
-sidekick-tree.dock-position=right
-sidekick.auto-complete-popup-get-focus=true
-sidekick.buffer-save-parse=true
-sidekick.complete-delay=0
-sidekick.complete-instant.toggle=false
-sidekick.complete-popup.accept-characters=\\t
-sidekick.complete-popup.insert-characters=
-sidekick.persistentFilter=true
-sidekick.showFilter=true
-sidekick.splitter.location=721
-systrayicon=false
-tip.show=false
-toggle-full-screen.shortcut2=S+F11
-toggle-multi-select.shortcut2=C+NUMBER_SIGN
-toggle-rect-select.shortcut2=A+NUMBER_SIGN
-twoStageSave=false
-vfs.browser.dock-position=left
-vfs.favorite.0.type=1
-vfs.favorite.0=$ISABELLE_HOME
-vfs.favorite.1.type=1
-vfs.favorite.1=$ISABELLE_HOME_USER
-vfs.favorite.2.type=1
-vfs.favorite.2=$JEDIT_HOME
-vfs.favorite.3.type=1
-vfs.favorite.3=$JEDIT_SETTINGS
-vfs.favorite.4.type=1
-vfs.favorite.4=isabelle-export:
-vfs.favorite.5.type=1
-vfs.favorite.5=isabelle-session:
-view.antiAlias=subpixel HRGB
-view.blockCaret=true
-view.caretBlink=false
-view.docking.framework=PIDE
-view.eolMarkers=false
-view.extendedState=0
-view.font=Isabelle DejaVu Sans Mono
-view.fontsize=18
-view.fracFontMetrics=false
-view.gutter.font=Isabelle DejaVu Sans Mono
-view.gutter.fontsize=12
-view.gutter.lineNumbers=false
-view.gutter.selectionAreaWidth=18
-view.height=850
-view.middleMousePaste=true
-view.showToolbar=true
-view.status.memory.background=#666699
-view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
-view.thickCaret=true
-view.width=1200
-xml-insert-closing-tag.shortcut=
diff -r af82097b4adc -r ff716ecb0805 src/Tools/jEdit/src/modes/isabelle-ml.xml
--- a/src/Tools/jEdit/src/modes/isabelle-ml.xml	Mon May 10 20:09:47 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-
-<!-- Isabelle/ML mode -->
-<MODE>
-  <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'?⇩\^&lt;&gt;"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃⦉" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦊⦄⟧⦈⌋⌉⟩›»)]}" />
-    <PROPERTY NAME="tabSize" VALUE="2" />
-    <PROPERTY NAME="indentSize" VALUE="2" />
-  </PROPS>
-</MODE>
diff -r af82097b4adc -r ff716ecb0805 src/Tools/jEdit/src/modes/isabelle-news.xml
--- a/src/Tools/jEdit/src/modes/isabelle-news.xml	Mon May 10 20:09:47 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-
-<!-- Isabelle NEWS mode -->
-<MODE>
-  <PROPS>
-    <PROPERTY NAME="noWordSep" VALUE="_'?⇩\^&lt;&gt;"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃⦉" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦊⦄⟧⦈⌋⌉⟩›»)]}" />
-    <PROPERTY NAME="tabSize" VALUE="2" />
-    <PROPERTY NAME="indentSize" VALUE="2" />
-  </PROPS>
-</MODE>
diff -r af82097b4adc -r ff716ecb0805 src/Tools/jEdit/src/modes/isabelle-options.xml
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml	Mon May 10 20:09:47 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-
-<!-- Isabelle options mode -->
-<MODE>
-  <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'?⇩\^&lt;&gt;"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃⦉" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦊⦄⟧⦈⌋⌉⟩›»)]}" />
-    <PROPERTY NAME="tabSize" VALUE="2" />
-    <PROPERTY NAME="indentSize" VALUE="2" />
-  </PROPS>
-</MODE>
diff -r af82097b4adc -r ff716ecb0805 src/Tools/jEdit/src/modes/isabelle-root.xml
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml	Mon May 10 20:09:47 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-
-<!-- Isabelle session root mode -->
-<MODE>
-  <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'?⇩\^&lt;&gt;"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃⦉" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦊⦄⟧⦈⌋⌉⟩›»)]}" />
-    <PROPERTY NAME="tabSize" VALUE="2" />
-    <PROPERTY NAME="indentSize" VALUE="2" />
-  </PROPS>
-</MODE>
diff -r af82097b4adc -r ff716ecb0805 src/Tools/jEdit/src/modes/isabelle.xml
--- a/src/Tools/jEdit/src/modes/isabelle.xml	Mon May 10 20:09:47 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-
-<!-- Isabelle theory mode -->
-<MODE>
-  <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'?⇩\^&lt;&gt;"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃⦉" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦊⦄⟧⦈⌋⌉⟩›»)]}" />
-    <PROPERTY NAME="tabSize" VALUE="2" />
-    <PROPERTY NAME="indentSize" VALUE="2" />
-  </PROPS>
-</MODE>
diff -r af82097b4adc -r ff716ecb0805 src/Tools/jEdit/src/modes/sml.xml
--- a/src/Tools/jEdit/src/modes/sml.xml	Mon May 10 20:09:47 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-
-<!-- Standard ML mode -->
-<MODE>
-  <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
-    <PROPERTY NAME="noWordSep" VALUE="_'"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃⦉" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦊⦄⟧⦈⌋⌉⟩›»)]}" />
-    <PROPERTY NAME="tabSize" VALUE="2" />
-    <PROPERTY NAME="indentSize" VALUE="2" />
-  </PROPS>
-</MODE>