--- a/Admin/isatest/isatest-makedist Wed Jun 22 15:07:03 2011 +0200
+++ b/Admin/isatest/isatest-makedist Wed Jun 22 16:35:31 2011 +0200
@@ -59,7 +59,7 @@
echo "### building distribution" >> $DISTLOG 2>&1
mkdir -p $DISTPREFIX
-$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110620" >> $DISTLOG 2>&1
+$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20110622" >> $DISTLOG 2>&1
if [ $? -ne 0 ]
then
--- a/src/Tools/jEdit/patches/extended_styles Wed Jun 22 15:07:03 2011 +0200
+++ b/src/Tools/jEdit/patches/extended_styles Wed Jun 22 16:35:31 2011 +0200
@@ -1,63 +1,74 @@
-Only in jEdit-patched: build
-diff -ru jEdit/org/gjt/sp/jedit/Buffer.java jEdit-patched/org/gjt/sp/jedit/Buffer.java
---- jEdit/org/gjt/sp/jedit/Buffer.java 2010-05-09 14:29:25.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/Buffer.java 2011-06-18 18:28:19.000000000 +0200
-@@ -2232,7 +2232,7 @@
- start = next;
- token = token.next;
- }
-- if (token.id == Token.END || token.id == Token.NULL)
-+ if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
- {
- JOptionPane.showMessageDialog(jEdit.getActiveView(),
- jEdit.getProperty("syntax-style-no-token.message"),
-diff -ru jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
---- jEdit/org/gjt/sp/jedit/syntax/Token.java 2010-05-09 14:29:24.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2011-06-18 18:28:10.000000000 +0200
+diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
+--- 4.4.1/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2011-06-21 01:28:56.000000000 +0200
++++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2011-06-22 16:07:32.000000000 +0200
+@@ -78,7 +78,7 @@
+ start = next;
+ token = token.next;
+ }
+- if (token.id == Token.END || token.id == Token.NULL)
++ if (token.id == Token.END || (token.id % Token.ID_COUNT) == Token.NULL)
+ {
+ JOptionPane.showMessageDialog(textArea.getView(),
+ jEdit.getProperty("syntax-style-no-token.message"),
+diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2011-06-21 01:29:10.000000000 +0200
++++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2011-06-22 16:02:07.000000000 +0200
+@@ -380,7 +380,7 @@
+ // this is either style.getBackgroundColor() or
+ // styles[defaultID].getBackgroundColor()
+ private Color background;
+- private String str;
++ public String str;
+ //private GlyphVector gv;
+ private List<GlyphVector> glyphs;
+ private boolean visible;
+diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+--- 4.4.1/jEdit/org/gjt/sp/jedit/syntax/Token.java 2011-06-21 01:29:10.000000000 +0200
++++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2011-06-22 16:08:47.000000000 +0200
@@ -57,7 +57,7 @@
- */
- public static String tokenToString(byte token)
- {
-- return (token == Token.END) ? "END" : TOKEN_TYPES[token];
-+ return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
- } //}}}
-
- //{{{ Token types
-diff -ru jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- jEdit/org/gjt/sp/util/SyntaxUtilities.java 2010-05-09 14:29:29.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2011-06-20 21:30:58.000000000 +0200
+ */
+ public static String tokenToString(byte token)
+ {
+- return (token == Token.END) ? "END" : TOKEN_TYPES[token];
++ return (token == Token.END) ? "END" : TOKEN_TYPES[token % ID_COUNT];
+ } //}}}
+
+ //{{{ Token types
+diff -ru 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 4.4.1/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2011-06-21 01:29:11.000000000 +0200
++++ 4.4.1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2011-06-22 16:05:28.000000000 +0200
@@ -194,6 +194,23 @@
- }
-
- /**
-+ * 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.
- * @param family The font family
+ }
+
+ /**
++ * 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.
+ * @param family The font family
@@ -222,8 +239,9 @@
- Log.log(Log.ERROR,StandardUtilities.class,e);
- }
- }
-+ styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
-
-- return styles;
-+ return _styleExtender.extendStyles(styles);
- } //}}}
-
- private SyntaxUtilities(){}
+ Log.log(Log.ERROR,StandardUtilities.class,e);
+ }
+ }
++ styles[0] = new SyntaxStyle(Color.black, null, new Font(family, 0, size));
+
+- return styles;
++ return _styleExtender.extendStyles(styles);
+ } //}}}
+
+ private SyntaxUtilities(){}
--- a/src/Tools/jEdit/patches/render_context Wed Jun 22 15:07:03 2011 +0200
+++ b/src/Tools/jEdit/patches/render_context Wed Jun 22 16:35:31 2011 +0200
@@ -1,6 +1,6 @@
-diff -ru jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
---- jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2010-05-09 14:29:17.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2011-06-21 23:00:11.000000000 +0200
+diff -ru 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- 4.4.1/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2011-06-21 01:28:56.000000000 +0200
++++ 4.4.1/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2011-06-22 16:18:43.000000000 +0200
@@ -646,7 +646,7 @@
this.font = font;
@@ -10,3 +10,4 @@
glyphs = font.createGlyphVector(fontRenderContext,text);
width = (int)glyphs.getLogicalBounds().getWidth() + 4;
//height = (int)glyphs.getLogicalBounds().getHeight();
+
--- a/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 22 15:07:03 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 22 16:35:31 2011 +0200
@@ -187,23 +187,20 @@
}
private def paint_chunk_list(
- gfx: Graphics2D, offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+ gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
{
val clip_rect = gfx.getClipBounds
val painter = text_area.getPainter
val font_context = painter.getFontRenderContext
var w = 0.0f
- var chunk_offset = offset
var chunk = head
while (chunk != null) {
- val chunk_length = if (chunk.str == null) 0 else chunk.str.length
-
+ val chunk_offset = line_start + chunk.offset
if (x + w + chunk.width > clip_rect.x &&
- x + w < clip_rect.x + clip_rect.width &&
- chunk.accessable && chunk.visible)
+ x + w < clip_rect.x + clip_rect.width && chunk.accessable)
{
- val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
+ val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
val chunk_font = chunk.style.getFont
val chunk_color = chunk.style.getForegroundColor
@@ -251,7 +248,6 @@
}
}
w += chunk.width
- chunk_offset += chunk_length
chunk = chunk.next.asInstanceOf[Chunk]
}
w