# HG changeset patch # User wenzelm # Date 1489951701 -3600 # Node ID 4f3da52cec02481db9b0219363012a6ea96f33c7 # Parent 2510b0ce28da384e04c7e57fac0fbd049491bbfc updated to jedit-5.4.0; diff -r 2510b0ce28da -r 4f3da52cec02 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sun Mar 19 18:28:32 2017 +0100 +++ b/Admin/components/components.sha1 Sun Mar 19 20:28:21 2017 +0100 @@ -106,6 +106,7 @@ 8ba7b6791be788f316427cdcd805daeaa6935190 jedit_build-20151124.tar.gz c70c5a6c565d435a09a8639f8afd3de360708e1c jedit_build-20160330.tar.gz d4e1496c257659cf15458d718f4663cdd95a404e jedit_build-20161024.tar.gz +d806c1c26b571b5b4ef05ea11e8b9cf936518e06 jedit_build-20170319.tar.gz 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz diff -r 2510b0ce28da -r 4f3da52cec02 Admin/components/main --- a/Admin/components/main Sun Mar 19 18:28:32 2017 +0100 +++ b/Admin/components/main Sun Mar 19 20:28:21 2017 +0100 @@ -5,7 +5,7 @@ e-1.8 isabelle_fonts-20160830 jdk-8u121 -jedit_build-20161024 +jedit_build-20170319 jfreechart-1.0.14-1 jortho-1.0-2 kodkodi-1.5.2 diff -r 2510b0ce28da -r 4f3da52cec02 NEWS --- a/NEWS Sun Mar 19 18:28:32 2017 +0100 +++ b/NEWS Sun Mar 19 20:28:21 2017 +0100 @@ -45,6 +45,8 @@ the document model to theories that are required for open editor buffers. +* Update to jedit-5.4.0. + *** HOL *** diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sun Mar 19 18:28:32 2017 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Mar 19 20:28:21 2017 +0100 @@ -353,12 +353,12 @@ cd ../.. rm -rf dist/classes - cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.3.0manual-a4.pdf" dist/doc/jedit-manual.pdf + cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.4.0manual-a4.pdf" dist/doc/jedit-manual.pdf cp dist/doc/CHANGES.txt dist/doc/jedit-changes cat > dist/doc/Contents <'; - 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 '‹'; -+ 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 '⌈'; -+ 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 '⦇'; -+ 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'; - } - } //}}} -diff -ru 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java ---- 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2015-10-20 19:56:08.000000000 +0200 -+++ 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2015-11-24 22:14:56.935661997 +0100 -@@ -194,7 +194,24 @@ - { - return loadStyles(family,size,true); - } -- -+ -+ /** -+ * Extended styles derived from the user-specified style array. -+ */ -+ -+ public static class StyleExtender -+ { -+ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) -+ { -+ return styles; -+ } -+ } -+ volatile private static StyleExtender _styleExtender = new StyleExtender(); -+ public static void setStyleExtender(StyleExtender ext) -+ { -+ _styleExtender = ext; -+ } -+ - /** - * Loads the syntax styles from the properties, giving them the specified - * base font family and size. -@@ -224,9 +241,11 @@ - Log.log(Log.ERROR,StandardUtilities.class,e); - } - } -- -- return styles; -+ styles[0] = -+ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK), -+ null, new Font(family, 0, size)); -+ return _styleExtender.extendStyles(styles); - } //}}} -- -+ - private SyntaxUtilities(){} - } diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/patches/docking --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/docking Sun Mar 19 20:28:21 2017 +0100 @@ -0,0 +1,52 @@ +diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java +--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2017-03-18 14:30:25.000000000 +0100 ++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2017-03-19 19:27:45.730945687 +0100 +@@ -35,7 +35,7 @@ + import javax.swing.Box; + import javax.swing.BoxLayout; + import javax.swing.JButton; +-import javax.swing.JFrame; ++import javax.swing.JDialog; + import javax.swing.JPopupMenu; + import javax.swing.JSeparator; + import javax.swing.SwingUtilities; +@@ -51,7 +51,7 @@ + * @version $Id: FloatingWindowContainer.java 24411 2016-06-19 11:02:53Z kerik-sf $ + * @since jEdit 4.0pre1 + */ +-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, ++public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, + PropertyChangeListener + { + String dockableName = null; +@@ -59,6 +59,8 @@ + public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager, + boolean clone) + { ++ super(dockableWindowManager.getView()); ++ + this.dockableWindowManager = dockableWindowManager; + + dockableWindowManager.addPropertyChangeListener(this); +@@ -94,7 +96,6 @@ + pack(); + Container parent = dockableWindowManager.getView(); + GUIUtilities.loadGeometry(this, parent, dockableName); +- GUIUtilities.addSizeSaver(this, parent, dockableName); + KeyListener listener = dockableWindowManager.closeListener(dockableName); + addKeyListener(listener); + getContentPane().addKeyListener(listener); +@@ -161,8 +162,11 @@ + @Override + public void dispose() + { +- entry.container = null; +- entry.win = null; ++ GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName); ++ if (entry != null) { ++ entry.container = null; ++ entry.win = null; ++ } + super.dispose(); + } //}}} + diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/patches/extended_styles --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/extended_styles Sun Mar 19 20:28:21 2017 +0100 @@ -0,0 +1,84 @@ +diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java +--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 2017-03-18 14:30:28.000000000 +0100 ++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2017-03-19 19:27:45.730945687 +0100 +@@ -259,9 +259,9 @@ + //{{{ Package private members + + //{{{ Instance variables +- SyntaxStyle style; ++ public SyntaxStyle style; + // set up after init() +- float width; ++ public float width; + //}}} + + //{{{ Chunk constructor +@@ -509,7 +509,7 @@ + // this is either style.getBackgroundColor() or + // styles[defaultID].getBackgroundColor() + private Color background; +- private String str; ++ public String str; + private GlyphVector[] glyphs; + //}}} + +diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java +--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 2017-03-18 14:30:28.000000000 +0100 ++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2017-03-19 19:27:45.734945702 +0100 +@@ -917,6 +917,11 @@ + return chunkCache.getLineInfo(screenLine).physicalLine; + } //}}} + ++ public Chunk getChunksOfScreenLine(int screenLine) ++ { ++ return chunkCache.getLineInfo(screenLine).chunks; ++ } ++ + //{{{ getScreenLineOfOffset() method + /** + * Returns the screen (wrapped) line containing the specified offset. +Only in 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea: TextArea.java.orig +diff -ru 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java +--- 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2017-03-18 14:30:34.000000000 +0100 ++++ 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2017-03-19 19:27:45.734945702 +0100 +@@ -200,7 +200,24 @@ + { + return loadStyles(family,size,true); + } +- ++ ++ /** ++ * Extended styles derived from the user-specified style array. ++ */ ++ ++ public static class StyleExtender ++ { ++ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) ++ { ++ return styles; ++ } ++ } ++ volatile private static StyleExtender _styleExtender = new StyleExtender(); ++ public static void setStyleExtender(StyleExtender ext) ++ { ++ _styleExtender = ext; ++ } ++ + /** + * Loads the syntax styles from the properties, giving them the specified + * base font family and size. +@@ -230,9 +247,11 @@ + Log.log(Log.ERROR,StandardUtilities.class,e); + } + } +- +- return styles; ++ styles[0] = ++ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK), ++ null, new Font(family, 0, size)); ++ return _styleExtender.extendStyles(styles); + } //}}} +- ++ + private SyntaxUtilities(){} + } diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/patches/file_completion --- a/src/Tools/jEdit/patches/file_completion Sun Mar 19 18:28:32 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java ---- 5.3.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2015-10-20 19:56:08.000000000 +0200 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2015-10-23 20:06:27.874803025 +0200 -@@ -82,16 +82,7 @@ - } - else if(matchAgainst.regionMatches(true,0,str,0,strLen)) - { -- /* Keep the first match with exact length but different case. -- * If the first match is not same length, prefer longest match */ -- if(iPotentialMatch == -1 -- || (potentialMatchGTStr -- && (matchAgainst.length() > potentialMatchLen))) -- { -- potentialMatchLen = matchAgainst.length(); -- iPotentialMatch = i; -- potentialMatchGTStr = potentialMatchLen > strLen; -- } -+ return i; - } - } - diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/patches/folding --- a/src/Tools/jEdit/patches/folding Sun Mar 19 18:28:32 2017 +0100 +++ b/src/Tools/jEdit/patches/folding Sun Mar 19 20:28:21 2017 +0100 @@ -1,7 +1,7 @@ -diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java ---- 5.3.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-10-20 19:56:02.000000000 +0200 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2015-10-23 20:02:38.897330618 +0200 -@@ -1956,29 +1956,23 @@ +diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java +--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 2017-03-18 14:30:28.000000000 +0100 ++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2017-03-19 19:27:45.734945702 +0100 +@@ -1950,29 +1950,23 @@ { Segment seg = new Segment(); newFoldLevel = foldHandler.getFoldLevel(this,i,seg); diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/patches/gutter --- a/src/Tools/jEdit/patches/gutter Sun Mar 19 18:28:32 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -diff -ru 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java ---- 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java 2015-10-20 19:56:03.000000000 +0200 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java 2015-11-24 21:58:47.686343684 +0100 -@@ -185,8 +185,6 @@ - } - - int y = clip.y - clip.y % lineHeight; -- if (y == 0) -- y = textArea.getPainter().getLineExtraSpacing(); - - extensionMgr.paintScreenLineRange(textArea,gfx, - firstLine,lastLine,y,lineHeight); -@@ -725,7 +723,7 @@ - - FontMetrics textAreaFm = textArea.getPainter().getFontMetrics(); - int lineHeight = textArea.getPainter().getLineHeight(); -- int baseline = textAreaFm.getAscent(); -+ int baseline = lineHeight - (textAreaFm.getLeading()+1) - textAreaFm.getDescent(); - - ChunkCache.LineInfo info = textArea.chunkCache.getLineInfo(line); - int physicalLine = info.physicalLine; diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/patches/props --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/props Sun Mar 19 20:28:21 2017 +0100 @@ -0,0 +1,13 @@ +diff -ru 5.4.0/jEdit-orig/org/jedit/localization/jedit_en.props 5.4.0/jEdit-patched/org/jedit/localization/jedit_en.props +--- 5.4.0/jEdit-orig/org/jedit/localization/jedit_en.props 2017-03-18 14:30:24.000000000 +0100 ++++ 5.4.0/jEdit-patched/org/jedit/localization/jedit_en.props 2017-03-19 19:35:49.728895954 +0100 +@@ -1262,8 +1262,7 @@ + The most likely reason is that the JAR file is corrupt; try\n\ + reinstalling it. See Utilities->Troubleshooting->Activity Log\n\ + for a full stack trace. +-plugin-error.start-error=Cannot start: {0}\n\ +- Try updating to a newer version of the plugin. ++plugin-error.start-error=Cannot start: {0} + plugin-error.already-loaded=Two copies installed. Please remove one of the \ + two copies. + plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}. diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Sun Mar 19 18:28:32 2017 +0100 +++ b/src/Tools/jEdit/src/Isabelle.props Sun Mar 19 20:28:21 2017 +0100 @@ -14,7 +14,7 @@ #dependencies plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8 -plugin.isabelle.jedit.Plugin.depend.1=jedit 05.03.00.00 +plugin.isabelle.jedit.Plugin.depend.1=jedit 05.04.00.00 plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4 plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3 plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8 diff -r 2510b0ce28da -r 4f3da52cec02 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sun Mar 19 18:28:32 2017 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Sun Mar 19 20:28:21 2017 +0100 @@ -412,17 +412,11 @@ /* strict initialization */ - // adhoc patch of confusing message - val orig_plugin_error = jEdit.getProperty("plugin-error.start-error") - jEdit.setProperty("plugin-error.start-error", "Cannot start plugin: {0}") - init_options() init_resources() init_session() PIDE._plugin = this - jEdit.setProperty("plugin-error.start-error", orig_plugin_error) - /* non-strict initialization */