updated to jedit-5.5.0;
authorwenzelm
Tue Apr 17 14:48:55 2018 +0200 (16 months ago)
changeset 67992752a4e6d760c
parent 67991 53ab458395a8
child 67993 271e2d84e7a3
updated to jedit-5.5.0;
discontinued jedit_build/contrib/jEdit-patched.tar.gz -- its content is in directory jedit_build/contrib/jedit-5.5.0-patched/jEdit;
Admin/components/components.sha1
Admin/components/main
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/patches/docking
src/Tools/jEdit/patches/extended_styles
src/Tools/jEdit/patches/folding
src/Tools/jEdit/patches/props
     1.1 --- a/Admin/components/components.sha1	Tue Apr 17 10:22:42 2018 +0100
     1.2 +++ b/Admin/components/components.sha1	Tue Apr 17 14:48:55 2018 +0200
     1.3 @@ -124,6 +124,7 @@
     1.4  c70c5a6c565d435a09a8639f8afd3de360708e1c  jedit_build-20160330.tar.gz
     1.5  d4e1496c257659cf15458d718f4663cdd95a404e  jedit_build-20161024.tar.gz
     1.6  d806c1c26b571b5b4ef05ea11e8b9cf936518e06  jedit_build-20170319.tar.gz
     1.7 +7bcb202e13358dd750e964b2f747664428b5d8b3  jedit_build-20180417.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	Tue Apr 17 10:22:42 2018 +0100
     2.2 +++ b/Admin/components/main	Tue Apr 17 14:48:55 2018 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  e-2.0-1
     2.5  isabelle_fonts-20180113
     2.6  jdk-8u162
     2.7 -jedit_build-20170319
     2.8 +jedit_build-20180417
     2.9  jfreechart-1.0.14-1
    2.10  jortho-1.0-2
    2.11  kodkodi-1.5.2
     3.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Apr 17 10:22:42 2018 +0100
     3.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Apr 17 14:48:55 2018 +0200
     3.3 @@ -411,12 +411,12 @@
     3.4    compile_sources "${SOURCES[@]}"
     3.5    make_jar "$TARGET"
     3.6  
     3.7 -  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.4.0manual-a4.pdf" dist/doc/jedit-manual.pdf
     3.8 +  cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.5.0manual-a4.pdf" dist/doc/jedit-manual.pdf
     3.9    cp dist/doc/CHANGES.txt dist/doc/jedit-changes
    3.10    cat > dist/doc/Contents <<EOF
    3.11  Original jEdit Documentation
    3.12 -  jedit-manual    jEdit 5.4 User's Guide
    3.13 -  jedit-changes   jEdit 5.4 Version History
    3.14 +  jedit-manual    jEdit 5.5 User's Guide
    3.15 +  jedit-changes   jEdit 5.5 Version History
    3.16  
    3.17  EOF
    3.18  
     4.1 --- a/src/Tools/jEdit/patches/docking	Tue Apr 17 10:22:42 2018 +0100
     4.2 +++ b/src/Tools/jEdit/patches/docking	Tue Apr 17 14:48:55 2018 +0200
     4.3 @@ -1,6 +1,6 @@
     4.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
     4.5 ---- 5.4.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2017-03-18 14:30:25.000000000 +0100
     4.6 -+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2017-03-19 19:27:45.730945687 +0100
     4.7 +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
     4.8 +--- 5.5.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2018-04-09 01:56:46.000000000 +0200
     4.9 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2018-04-17 13:57:40.320348370 +0200
    4.10  @@ -35,7 +35,7 @@
    4.11   import javax.swing.Box;
    4.12   import javax.swing.BoxLayout;
     5.1 --- a/src/Tools/jEdit/patches/extended_styles	Tue Apr 17 10:22:42 2018 +0100
     5.2 +++ b/src/Tools/jEdit/patches/extended_styles	Tue Apr 17 14:48:55 2018 +0200
     5.3 @@ -1,7 +1,7 @@
     5.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
     5.5 ---- 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java	2017-03-18 14:30:28.000000000 +0100
     5.6 -+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2017-03-19 19:27:45.730945687 +0100
     5.7 -@@ -259,9 +259,9 @@
     5.8 +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
     5.9 +--- 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2018-04-09 01:57:24.000000000 +0200
    5.10 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2018-04-17 13:58:12.912465088 +0200
    5.11 +@@ -322,9 +322,9 @@
    5.12   	//{{{ Package private members
    5.13   
    5.14   	//{{{ Instance variables
    5.15 @@ -13,7 +13,7 @@
    5.16   	//}}}
    5.17   
    5.18   	//{{{ Chunk constructor
    5.19 -@@ -509,7 +509,7 @@
    5.20 +@@ -572,7 +572,7 @@
    5.21   	// this is either style.getBackgroundColor() or
    5.22   	// styles[defaultID].getBackgroundColor()
    5.23   	private Color background;
    5.24 @@ -22,9 +22,9 @@
    5.25   	private GlyphVector[] glyphs;
    5.26   	//}}}
    5.27   
    5.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
    5.29 ---- 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java	2017-03-18 14:30:28.000000000 +0100
    5.30 -+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2017-03-19 19:27:45.734945702 +0100
    5.31 +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
    5.32 +--- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2018-04-09 01:58:01.000000000 +0200
    5.33 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2018-04-17 13:58:12.912465088 +0200
    5.34  @@ -917,6 +917,11 @@
    5.35   		return chunkCache.getLineInfo(screenLine).physicalLine;
    5.36   	} //}}}
    5.37 @@ -37,10 +37,9 @@
    5.38   	//{{{ getScreenLineOfOffset() method
    5.39   	/**
    5.40   	 * Returns the screen (wrapped) line containing the specified offset.
    5.41 -Only in 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea: TextArea.java.orig
    5.42 -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.43 ---- 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2017-03-18 14:30:34.000000000 +0100
    5.44 -+++ 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2017-03-19 19:27:45.734945702 +0100
    5.45 +diff -ru 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    5.46 +--- 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2018-04-09 01:58:37.000000000 +0200
    5.47 ++++ 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2018-04-17 13:58:12.912465088 +0200
    5.48  @@ -200,7 +200,24 @@
    5.49   	{
    5.50   		return loadStyles(family,size,true);
     6.1 --- a/src/Tools/jEdit/patches/folding	Tue Apr 17 10:22:42 2018 +0100
     6.2 +++ b/src/Tools/jEdit/patches/folding	Tue Apr 17 14:48:55 2018 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4 -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
     6.5 ---- 5.4.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java	2017-03-18 14:30:28.000000000 +0100
     6.6 -+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2017-03-19 19:27:45.734945702 +0100
     6.7 -@@ -1950,29 +1950,23 @@
     6.8 +diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
     6.9 +--- 5.5.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java	2018-04-09 01:57:06.000000000 +0200
    6.10 ++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java	2018-04-17 13:58:42.984572359 +0200
    6.11 +@@ -1961,29 +1961,23 @@
    6.12   			{
    6.13   				Segment seg = new Segment();
    6.14   				newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
     7.1 --- a/src/Tools/jEdit/patches/props	Tue Apr 17 10:22:42 2018 +0100
     7.2 +++ b/src/Tools/jEdit/patches/props	Tue Apr 17 14:48:55 2018 +0200
     7.3 @@ -1,7 +1,7 @@
     7.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
     7.5 ---- 5.4.0/jEdit-orig/org/jedit/localization/jedit_en.props	2017-03-18 14:30:24.000000000 +0100
     7.6 -+++ 5.4.0/jEdit-patched/org/jedit/localization/jedit_en.props	2017-03-19 19:35:49.728895954 +0100
     7.7 -@@ -1262,8 +1262,7 @@
     7.8 +diff -ru 5.5.0/jEdit/org/jedit/localization/jedit_en.props 5.5.0/jEdit-patched/org/jedit/localization/jedit_en.props
     7.9 +--- 5.5.0/jEdit/org/jedit/localization/jedit_en.props	2018-04-09 01:58:42.000000000 +0200
    7.10 ++++ 5.5.0/jEdit-patched/org/jedit/localization/jedit_en.props	2018-04-17 13:59:10.688670850 +0200
    7.11 +@@ -1270,8 +1270,7 @@
    7.12   	The most likely reason is that the JAR file is corrupt; try\n\
    7.13   	reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
    7.14   	for a full stack trace.