# HG changeset patch # User wenzelm # Date 1563393392 -7200 # Node ID 2e8af171887fe43152e1fb72fe2677c8922da827 # Parent 2b4c40722f0bb5d156da1614f3fed7f8125e2802 updated to jedit_build-20190717: support more brackets; diff -r 2b4c40722f0b -r 2e8af171887f Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed Jul 17 21:32:03 2019 +0200 +++ b/Admin/components/components.sha1 Wed Jul 17 21:56:32 2019 +0200 @@ -161,6 +161,7 @@ 58b9f03e5ec0b85f8123c31f5d8092dae5803773 jedit_build-20190130.tar.gz ec0aded5f2655e2de8bc4427106729e797584f2f jedit_build-20190224.tar.gz 1e53598a02ec8d8736b15f480cbe2c84767a7827 jedit_build-20190508.tar.gz +b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz diff -r 2b4c40722f0b -r 2e8af171887f Admin/components/main --- a/Admin/components/main Wed Jul 17 21:32:03 2019 +0200 +++ b/Admin/components/main Wed Jul 17 21:56:32 2019 +0200 @@ -6,7 +6,7 @@ e-2.0-2 isabelle_fonts-20190717 jdk-11.0.3+7 -jedit_build-20190508 +jedit_build-20190717 jfreechart-1.5.0 jortho-1.0-2 kodkodi-1.5.2-1 diff -r 2b4c40722f0b -r 2e8af171887f src/Tools/jEdit/patches/brackets --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/brackets Wed Jul 17 21:56:32 2019 +0200 @@ -0,0 +1,25 @@ +--- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2018-04-09 01:58:01.000000000 +0200 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2019-07-17 21:36:43.985183582 +0200 +@@ -1625,8 +1630,8 @@ + } + + // Scan backwards, trying to find a bracket +- String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃"; +- String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄"; ++ String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪"; ++ String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"; + int count = 1; + char openBracket = '\0'; + char closeBracket = '\0'; +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java +--- 5.5.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2018-04-09 01:58:07.000000000 +0200 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2019-07-17 21:44:15.545431576 +0200 +@@ -113,6 +113,8 @@ + case '⟧': if (direction != null) direction[0] = false; return '⟦'; + case '⦃': if (direction != null) direction[0] = true; return '⦄'; + case '⦄': if (direction != null) direction[0] = false; return '⦃'; ++ case '⟪': if (direction != null) direction[0] = true; return '⟫'; ++ case '⟫': if (direction != null) direction[0] = false; return '⟪'; + default: return '\0'; + } + } //}}}