updated to jedit-5.4.0;
authorwenzelm
Sun Mar 19 20:28:21 2017 +0100 (2017-03-19)
changeset 653294f3da52cec02
parent 65328 2510b0ce28da
child 65330 d83f709b7580
child 65331 999864cdf96c
updated to jedit-5.4.0;
Admin/components/components.sha1
Admin/components/main
NEWS
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/patches/brackets_extended_styles
src/Tools/jEdit/patches/docking
src/Tools/jEdit/patches/extended_styles
src/Tools/jEdit/patches/file_completion
src/Tools/jEdit/patches/folding
src/Tools/jEdit/patches/gutter
src/Tools/jEdit/patches/props
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/Admin/components/components.sha1	Sun Mar 19 18:28:32 2017 +0100
     1.2 +++ b/Admin/components/components.sha1	Sun Mar 19 20:28:21 2017 +0100
     1.3 @@ -106,6 +106,7 @@
     1.4  8ba7b6791be788f316427cdcd805daeaa6935190  jedit_build-20151124.tar.gz
     1.5  c70c5a6c565d435a09a8639f8afd3de360708e1c  jedit_build-20160330.tar.gz
     1.6  d4e1496c257659cf15458d718f4663cdd95a404e  jedit_build-20161024.tar.gz
     1.7 +d806c1c26b571b5b4ef05ea11e8b9cf936518e06  jedit_build-20170319.tar.gz
     1.8  0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
     1.9  8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
    1.10  c8a19a36adf6cefa779d85f22ded2f4654e68ea5  jortho-1.0-1.tar.gz
     2.1 --- a/Admin/components/main	Sun Mar 19 18:28:32 2017 +0100
     2.2 +++ b/Admin/components/main	Sun Mar 19 20:28:21 2017 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  e-1.8
     2.5  isabelle_fonts-20160830
     2.6  jdk-8u121
     2.7 -jedit_build-20161024
     2.8 +jedit_build-20170319
     2.9  jfreechart-1.0.14-1
    2.10  jortho-1.0-2
    2.11  kodkodi-1.5.2
     3.1 --- a/NEWS	Sun Mar 19 18:28:32 2017 +0100
     3.2 +++ b/NEWS	Sun Mar 19 20:28:21 2017 +0100
     3.3 @@ -45,6 +45,8 @@
     3.4  the document model to theories that are required for open editor
     3.5  buffers.
     3.6  
     3.7 +* Update to jedit-5.4.0.
     3.8 +
     3.9  
    3.10  *** HOL ***
    3.11  
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Mar 19 18:28:32 2017 +0100
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Mar 19 20:28:21 2017 +0100
     4.3 @@ -353,12 +353,12 @@
     4.4    cd ../..
     4.5    rm -rf dist/classes
     4.6  
     4.7 -  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.3.0manual-a4.pdf" dist/doc/jedit-manual.pdf
     4.8 +  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.4.0manual-a4.pdf" dist/doc/jedit-manual.pdf
     4.9    cp dist/doc/CHANGES.txt dist/doc/jedit-changes
    4.10    cat > dist/doc/Contents <<EOF
    4.11  Original jEdit Documentation
    4.12 -  jedit-manual    jEdit 5.3 User's Guide
    4.13 -  jedit-changes   jEdit 5.3 Version History
    4.14 +  jedit-manual    jEdit 5.4 User's Guide
    4.15 +  jedit-changes   jEdit 5.4 Version History
    4.16  
    4.17  EOF
    4.18  
     5.1 --- a/src/Tools/jEdit/patches/brackets_extended_styles	Sun Mar 19 18:28:32 2017 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,144 +0,0 @@
     5.4 -diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
     5.5 ---- 5.3.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java	2015-10-20 19:56:05.000000000 +0200
     5.6 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java	2015-10-23 20:02:22.161225360 +0200
     5.7 -@@ -79,7 +79,7 @@
     5.8 - 			start = next;
     5.9 - 			token = token.next;
    5.10 - 		}
    5.11 --		if (token.id == Token.END || token.id == Token.NULL)
    5.12 -+		if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
    5.13 - 		{
    5.14 - 			JOptionPane.showMessageDialog(textArea.getView(),
    5.15 - 				jEdit.getProperty("syntax-style-no-token.message"),
    5.16 -diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
    5.17 ---- 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2015-10-20 19:56:07.000000000 +0200
    5.18 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2015-10-23 20:02:22.161225360 +0200
    5.19 -@@ -259,9 +259,9 @@
    5.20 - 	//{{{ Package private members
    5.21 - 
    5.22 - 	//{{{ Instance variables
    5.23 --	SyntaxStyle style;
    5.24 -+	public SyntaxStyle style;
    5.25 - 	// set up after init()
    5.26 --	float width;
    5.27 -+	public float width;
    5.28 - 	//}}}
    5.29 - 
    5.30 - 	//{{{ Chunk constructor
    5.31 -@@ -509,7 +509,7 @@
    5.32 - 	// this is either style.getBackgroundColor() or
    5.33 - 	// styles[defaultID].getBackgroundColor()
    5.34 - 	private Color background;
    5.35 --	private String str;
    5.36 -+	public String str;
    5.37 - 	private GlyphVector[] glyphs;
    5.38 - 	//}}}
    5.39 - 
    5.40 -diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
    5.41 ---- 5.3.0/jEdit/org/gjt/sp/jedit/syntax/Token.java	2015-10-20 19:56:07.000000000 +0200
    5.42 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java	2015-10-23 20:02:22.161225360 +0200
    5.43 -@@ -57,7 +57,7 @@
    5.44 - 	 */
    5.45 - 	public static String tokenToString(byte token)
    5.46 - 	{
    5.47 --		return (token == Token.END) ? "END" : TOKEN_TYPES[token];
    5.48 -+		return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
    5.49 - 	} //}}}
    5.50 - 
    5.51 - 	//{{{ Token types
    5.52 -diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
    5.53 ---- 5.3.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2015-10-20 19:56:03.000000000 +0200
    5.54 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2015-10-23 20:02:22.161225360 +0200
    5.55 -@@ -910,6 +910,11 @@
    5.56 - 		return chunkCache.getLineInfo(screenLine).physicalLine;
    5.57 - 	} //}}}
    5.58 - 
    5.59 -+        public Chunk getChunksOfScreenLine(int screenLine)
    5.60 -+        {
    5.61 -+                return chunkCache.getLineInfo(screenLine).chunks;
    5.62 -+        }
    5.63 -+
    5.64 - 	//{{{ getScreenLineOfOffset() method
    5.65 - 	/**
    5.66 - 	 * Returns the screen (wrapped) line containing the specified offset.
    5.67 -@@ -1618,8 +1623,8 @@
    5.68 - 		}
    5.69 - 
    5.70 - 		// Scan backwards, trying to find a bracket
    5.71 --		String openBrackets = "([{";
    5.72 --		String closeBrackets = ")]}";
    5.73 -+		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
    5.74 -+		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄'";
    5.75 - 		int count = 1;
    5.76 - 		char openBracket = '\0';
    5.77 - 		char closeBracket = '\0';
    5.78 -diff -ru 5.3.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.3.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
    5.79 ---- 5.3.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2015-10-20 19:56:00.000000000 +0200
    5.80 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java	2015-10-23 19:46:33.728522904 +0200
    5.81 -@@ -97,6 +97,22 @@
    5.82 - 		case '}': if (direction != null) direction[0] = false; return '{';
    5.83 - 		case '<': if (direction != null) direction[0] = true;  return '>';
    5.84 - 		case '>': if (direction != null) direction[0] = false; return '<';
    5.85 -+		case '«': if (direction != null) direction[0] = true;  return '»';
    5.86 -+		case '»': if (direction != null) direction[0] = false; return '«';
    5.87 -+		case '‹': if (direction != null) direction[0] = true;  return '›';
    5.88 -+		case '›': if (direction != null) direction[0] = false; return '‹';
    5.89 -+		case '⟨': if (direction != null) direction[0] = true;  return '⟩';
    5.90 -+		case '⟩': if (direction != null) direction[0] = false; return '⟨';
    5.91 -+		case '⌈': if (direction != null) direction[0] = true;  return '⌉';
    5.92 -+		case '⌉': if (direction != null) direction[0] = false; return '⌈';
    5.93 -+		case '⌊': if (direction != null) direction[0] = true;  return '⌋';
    5.94 -+		case '⌋': if (direction != null) direction[0] = false; return '⌊';
    5.95 -+		case '⦇': if (direction != null) direction[0] = true;  return '⦈';
    5.96 -+		case '⦈': if (direction != null) direction[0] = false; return '⦇';
    5.97 -+		case '⟦': if (direction != null) direction[0] = true;  return '⟧';
    5.98 -+		case '⟧': if (direction != null) direction[0] = false; return '⟦';
    5.99 -+		case '⦃': if (direction != null) direction[0] = true;  return '⦄';
   5.100 -+		case '⦄': if (direction != null) direction[0] = false; return '⦃';
   5.101 - 		default:  return '\0';
   5.102 - 		}
   5.103 - 	} //}}}
   5.104 -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.105 ---- 5.3.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2015-10-20 19:56:08.000000000 +0200
   5.106 -+++ 5.3.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2015-11-24 22:14:56.935661997 +0100
   5.107 -@@ -194,7 +194,24 @@
   5.108 - 	{
   5.109 - 		return loadStyles(family,size,true);
   5.110 - 	}
   5.111 --	
   5.112 -+
   5.113 -+	/**
   5.114 -+	 * Extended styles derived from the user-specified style array.
   5.115 -+	 */
   5.116 -+
   5.117 -+	public static class StyleExtender
   5.118 -+	{
   5.119 -+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
   5.120 -+		{
   5.121 -+			return styles;
   5.122 -+		}
   5.123 -+	}
   5.124 -+	volatile private static StyleExtender _styleExtender = new StyleExtender();
   5.125 -+	public static void setStyleExtender(StyleExtender ext)
   5.126 -+	{
   5.127 -+		_styleExtender = ext;
   5.128 -+	}
   5.129 -+
   5.130 - 	/**
   5.131 - 	 * Loads the syntax styles from the properties, giving them the specified
   5.132 - 	 * base font family and size.
   5.133 -@@ -224,9 +241,11 @@
   5.134 - 				Log.log(Log.ERROR,StandardUtilities.class,e);
   5.135 - 			}
   5.136 - 		}
   5.137 --
   5.138 --		return styles;
   5.139 -+		styles[0] =
   5.140 -+			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
   5.141 -+				null, new Font(family, 0, size));
   5.142 -+		return _styleExtender.extendStyles(styles);
   5.143 - 	} //}}}
   5.144 --	
   5.145 -+
   5.146 - 	private SyntaxUtilities(){}
   5.147 - }
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/jEdit/patches/docking	Sun Mar 19 20:28:21 2017 +0100
     6.3 @@ -0,0 +1,52 @@
     6.4 +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
     6.5 +--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2017-03-18 14:30:25.000000000 +0100
     6.6 ++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2017-03-19 19:27:45.730945687 +0100
     6.7 +@@ -35,7 +35,7 @@
     6.8 + import javax.swing.Box;
     6.9 + import javax.swing.BoxLayout;
    6.10 + import javax.swing.JButton;
    6.11 +-import javax.swing.JFrame;
    6.12 ++import javax.swing.JDialog;
    6.13 + import javax.swing.JPopupMenu;
    6.14 + import javax.swing.JSeparator;
    6.15 + import javax.swing.SwingUtilities;
    6.16 +@@ -51,7 +51,7 @@
    6.17 +  * @version $Id: FloatingWindowContainer.java 24411 2016-06-19 11:02:53Z kerik-sf $
    6.18 +  * @since jEdit 4.0pre1
    6.19 +  */
    6.20 +-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer,
    6.21 ++public class FloatingWindowContainer extends JDialog implements DockableWindowContainer,
    6.22 + 	PropertyChangeListener
    6.23 + {
    6.24 + 	String dockableName = null;
    6.25 +@@ -59,6 +59,8 @@
    6.26 + 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
    6.27 + 		boolean clone)
    6.28 + 	{
    6.29 ++		super(dockableWindowManager.getView());
    6.30 ++
    6.31 + 		this.dockableWindowManager = dockableWindowManager;
    6.32 + 
    6.33 + 		dockableWindowManager.addPropertyChangeListener(this);
    6.34 +@@ -94,7 +96,6 @@
    6.35 + 		pack();
    6.36 + 		Container parent = dockableWindowManager.getView();
    6.37 + 		GUIUtilities.loadGeometry(this, parent, dockableName);
    6.38 +-		GUIUtilities.addSizeSaver(this, parent, dockableName);
    6.39 + 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
    6.40 + 		addKeyListener(listener);
    6.41 + 		getContentPane().addKeyListener(listener);
    6.42 +@@ -161,8 +162,11 @@
    6.43 + 	@Override
    6.44 + 	public void dispose()
    6.45 + 	{
    6.46 +-		entry.container = null;
    6.47 +-		entry.win = null;
    6.48 ++		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
    6.49 ++		if (entry != null) {
    6.50 ++			entry.container = null;
    6.51 ++			entry.win = null;
    6.52 ++		}
    6.53 + 		super.dispose();
    6.54 + 	} //}}}
    6.55 + 
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/jEdit/patches/extended_styles	Sun Mar 19 20:28:21 2017 +0100
     7.3 @@ -0,0 +1,84 @@
     7.4 +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
     7.5 +--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java	2017-03-18 14:30:28.000000000 +0100
     7.6 ++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2017-03-19 19:27:45.730945687 +0100
     7.7 +@@ -259,9 +259,9 @@
     7.8 + 	//{{{ Package private members
     7.9 + 
    7.10 + 	//{{{ Instance variables
    7.11 +-	SyntaxStyle style;
    7.12 ++	public SyntaxStyle style;
    7.13 + 	// set up after init()
    7.14 +-	float width;
    7.15 ++	public float width;
    7.16 + 	//}}}
    7.17 + 
    7.18 + 	//{{{ Chunk constructor
    7.19 +@@ -509,7 +509,7 @@
    7.20 + 	// this is either style.getBackgroundColor() or
    7.21 + 	// styles[defaultID].getBackgroundColor()
    7.22 + 	private Color background;
    7.23 +-	private String str;
    7.24 ++	public String str;
    7.25 + 	private GlyphVector[] glyphs;
    7.26 + 	//}}}
    7.27 + 
    7.28 +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
    7.29 +--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java	2017-03-18 14:30:28.000000000 +0100
    7.30 ++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2017-03-19 19:27:45.734945702 +0100
    7.31 +@@ -917,6 +917,11 @@
    7.32 + 		return chunkCache.getLineInfo(screenLine).physicalLine;
    7.33 + 	} //}}}
    7.34 + 
    7.35 ++        public Chunk getChunksOfScreenLine(int screenLine)
    7.36 ++        {
    7.37 ++                return chunkCache.getLineInfo(screenLine).chunks;
    7.38 ++        }
    7.39 ++
    7.40 + 	//{{{ getScreenLineOfOffset() method
    7.41 + 	/**
    7.42 + 	 * Returns the screen (wrapped) line containing the specified offset.
    7.43 +Only in 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea: TextArea.java.orig
    7.44 +diff -ru 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    7.45 +--- 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2017-03-18 14:30:34.000000000 +0100
    7.46 ++++ 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2017-03-19 19:27:45.734945702 +0100
    7.47 +@@ -200,7 +200,24 @@
    7.48 + 	{
    7.49 + 		return loadStyles(family,size,true);
    7.50 + 	}
    7.51 +-	
    7.52 ++
    7.53 ++	/**
    7.54 ++	 * Extended styles derived from the user-specified style array.
    7.55 ++	 */
    7.56 ++
    7.57 ++	public static class StyleExtender
    7.58 ++	{
    7.59 ++		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
    7.60 ++		{
    7.61 ++			return styles;
    7.62 ++		}
    7.63 ++	}
    7.64 ++	volatile private static StyleExtender _styleExtender = new StyleExtender();
    7.65 ++	public static void setStyleExtender(StyleExtender ext)
    7.66 ++	{
    7.67 ++		_styleExtender = ext;
    7.68 ++	}
    7.69 ++
    7.70 + 	/**
    7.71 + 	 * Loads the syntax styles from the properties, giving them the specified
    7.72 + 	 * base font family and size.
    7.73 +@@ -230,9 +247,11 @@
    7.74 + 				Log.log(Log.ERROR,StandardUtilities.class,e);
    7.75 + 			}
    7.76 + 		}
    7.77 +-
    7.78 +-		return styles;
    7.79 ++		styles[0] =
    7.80 ++			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
    7.81 ++				null, new Font(family, 0, size));
    7.82 ++		return _styleExtender.extendStyles(styles);
    7.83 + 	} //}}}
    7.84 +-	
    7.85 ++
    7.86 + 	private SyntaxUtilities(){}
    7.87 + }
     8.1 --- a/src/Tools/jEdit/patches/file_completion	Sun Mar 19 18:28:32 2017 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,21 +0,0 @@
     8.4 -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
     8.5 ---- 5.3.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java	2015-10-20 19:56:08.000000000 +0200
     8.6 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2015-10-23 20:06:27.874803025 +0200
     8.7 -@@ -82,16 +82,7 @@
     8.8 - 			}
     8.9 - 			else if(matchAgainst.regionMatches(true,0,str,0,strLen))
    8.10 - 			{
    8.11 --				/* Keep the first match with exact length but different case.
    8.12 --				 * If the first match is not same length, prefer longest match */
    8.13 --				if(iPotentialMatch == -1
    8.14 --						|| (potentialMatchGTStr
    8.15 --							&& (matchAgainst.length() > potentialMatchLen)))
    8.16 --				{
    8.17 --					potentialMatchLen = matchAgainst.length();
    8.18 --					iPotentialMatch = i;
    8.19 --					potentialMatchGTStr = potentialMatchLen > strLen;
    8.20 --				}
    8.21 -+                            return i;
    8.22 - 			}
    8.23 - 		}
    8.24 - 
     9.1 --- a/src/Tools/jEdit/patches/folding	Sun Mar 19 18:28:32 2017 +0100
     9.2 +++ b/src/Tools/jEdit/patches/folding	Sun Mar 19 20:28:21 2017 +0100
     9.3 @@ -1,7 +1,7 @@
     9.4 -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
     9.5 ---- 5.3.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java	2015-10-20 19:56:02.000000000 +0200
     9.6 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2015-10-23 20:02:38.897330618 +0200
     9.7 -@@ -1956,29 +1956,23 @@
     9.8 +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
     9.9 +--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java	2017-03-18 14:30:28.000000000 +0100
    9.10 ++++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2017-03-19 19:27:45.734945702 +0100
    9.11 +@@ -1950,29 +1950,23 @@
    9.12   			{
    9.13   				Segment seg = new Segment();
    9.14   				newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
    10.1 --- a/src/Tools/jEdit/patches/gutter	Sun Mar 19 18:28:32 2017 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,21 +0,0 @@
    10.4 -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
    10.5 ---- 5.3.0/jEdit-orig/org/gjt/sp/jedit/textarea/Gutter.java	2015-10-20 19:56:03.000000000 +0200
    10.6 -+++ 5.3.0/jEdit-patched/org/gjt/sp/jedit/textarea/Gutter.java	2015-11-24 21:58:47.686343684 +0100
    10.7 -@@ -185,8 +185,6 @@
    10.8 - 		}
    10.9 - 	
   10.10 - 		int y = clip.y - clip.y % lineHeight;
   10.11 --		if (y == 0)
   10.12 --			y = textArea.getPainter().getLineExtraSpacing();
   10.13 - 
   10.14 - 		extensionMgr.paintScreenLineRange(textArea,gfx,
   10.15 - 			firstLine,lastLine,y,lineHeight);
   10.16 -@@ -725,7 +723,7 @@
   10.17 - 
   10.18 - 		FontMetrics textAreaFm = textArea.getPainter().getFontMetrics();
   10.19 - 		int lineHeight = textArea.getPainter().getLineHeight();
   10.20 --		int baseline = textAreaFm.getAscent();
   10.21 -+		int baseline = lineHeight - (textAreaFm.getLeading()+1) - textAreaFm.getDescent();
   10.22 - 
   10.23 - 		ChunkCache.LineInfo info = textArea.chunkCache.getLineInfo(line);
   10.24 - 		int physicalLine = info.physicalLine;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/jEdit/patches/props	Sun Mar 19 20:28:21 2017 +0100
    11.3 @@ -0,0 +1,13 @@
    11.4 +diff -ru 5.4.0/jEdit-orig/org/jedit/localization/jedit_en.props 5.4.0/jEdit-patched/org/jedit/localization/jedit_en.props
    11.5 +--- 5.4.0/jEdit-orig/org/jedit/localization/jedit_en.props	2017-03-18 14:30:24.000000000 +0100
    11.6 ++++ 5.4.0/jEdit-patched/org/jedit/localization/jedit_en.props	2017-03-19 19:35:49.728895954 +0100
    11.7 +@@ -1262,8 +1262,7 @@
    11.8 + 	The most likely reason is that the JAR file is corrupt; try\n\
    11.9 + 	reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
   11.10 + 	for a full stack trace.
   11.11 +-plugin-error.start-error=Cannot start: {0}\n\
   11.12 +-	Try updating to a newer version of the plugin.
   11.13 ++plugin-error.start-error=Cannot start: {0}
   11.14 + plugin-error.already-loaded=Two copies installed. Please remove one of the \
   11.15 + 	two copies.
   11.16 + plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}.
    12.1 --- a/src/Tools/jEdit/src/Isabelle.props	Sun Mar 19 18:28:32 2017 +0100
    12.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Sun Mar 19 20:28:21 2017 +0100
    12.3 @@ -14,7 +14,7 @@
    12.4  
    12.5  #dependencies
    12.6  plugin.isabelle.jedit.Plugin.depend.0=jdk 1.8
    12.7 -plugin.isabelle.jedit.Plugin.depend.1=jedit 05.03.00.00
    12.8 +plugin.isabelle.jedit.Plugin.depend.1=jedit 05.04.00.00
    12.9  plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
   12.10  plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
   12.11  plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8
    13.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Mar 19 18:28:32 2017 +0100
    13.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Mar 19 20:28:21 2017 +0100
    13.3 @@ -412,17 +412,11 @@
    13.4  
    13.5      /* strict initialization */
    13.6  
    13.7 -    // adhoc patch of confusing message
    13.8 -    val orig_plugin_error = jEdit.getProperty("plugin-error.start-error")
    13.9 -    jEdit.setProperty("plugin-error.start-error", "Cannot start plugin: {0}")
   13.10 -
   13.11      init_options()
   13.12      init_resources()
   13.13      init_session()
   13.14      PIDE._plugin = this
   13.15  
   13.16 -    jEdit.setProperty("plugin-error.start-error", orig_plugin_error)
   13.17 -
   13.18  
   13.19      /* non-strict initialization */
   13.20