--- a/src/Tools/jEdit/lib/Tools/jedit Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Dec 01 19:51:43 2012 +0100
@@ -46,6 +46,7 @@
"src/actions.xml"
"src/dockables.xml"
"src/Isabelle.props"
+ "src/jEdit.props"
"src/services.xml"
)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit/annotation Sat Dec 01 19:51:43 2012 +0100
@@ -0,0 +1,45 @@
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/input/AbstractInputHandler.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/input/AbstractInputHandler.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/input/AbstractInputHandler.java 2012-11-17 16:41:23.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/input/AbstractInputHandler.java 2012-12-01 18:40:31.000000000 +0100
+@@ -29,8 +29,6 @@
+ import java.awt.event.KeyEvent;
+ import java.util.Hashtable;
+ import java.util.StringTokenizer;
+-import javax.annotation.Nonnull;
+-import javax.annotation.Nullable;
+
+ import org.gjt.sp.jedit.JEditAbstractEditAction;
+ import org.gjt.sp.jedit.gui.ShortcutPrefixActiveEvent;
+@@ -198,8 +196,7 @@
+ * @param keyBinding The key binding
+ * @since jEdit 3.2pre5
+ */
+- @Nullable
+- public Object getKeyBinding(@Nonnull String keyBinding)
++ public Object getKeyBinding(String keyBinding)
+ {
+ Hashtable current = bindings;
+ StringTokenizer st = new StringTokenizer(keyBinding);
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/jEdit.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/jEdit.java 2012-11-17 16:42:29.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2012-12-01 18:40:40.000000000 +0100
+@@ -35,8 +35,6 @@
+ import org.gjt.sp.jedit.View.ViewConfig;
+ import org.gjt.sp.jedit.bsh.UtilEvalError;
+
+-import javax.annotation.Nonnull;
+-import javax.annotation.Nullable;
+ import javax.swing.*;
+ import java.awt.event.*;
+ import java.io.*;
+@@ -3853,8 +3851,7 @@
+
+ } //}}}
+
+- @Nonnull
+- private static String getPLAFClassName(@Nullable String lf)
++ private static String getPLAFClassName(String lf)
+ {
+ if (lf != null && lf.length() != 0)
+ {
+
--- a/src/Tools/jEdit/patches/jedit/caret Sat Dec 01 17:23:50 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-diff -ru jEdit/org/gjt/sp/jedit/textarea/TextArea.java jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2012-06-15 22:20:05.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2012-08-13 19:11:04.000000000 +0200
-@@ -4907,7 +4907,7 @@
- /**
- * Returns true if the caret is visible, false otherwise.
- */
-- final boolean isCaretVisible()
-+ public final boolean isCaretVisible()
- {
- return blink && hasFocus();
- } //}}}
--- a/src/Tools/jEdit/patches/jedit/chunks Sat Dec 01 17:23:50 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-diff -ru jEdit/org/gjt/sp/jedit/textarea/TextArea.java jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2012-08-13 19:11:04.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2012-09-03 19:37:48.000000000 +0200
-@@ -905,6 +905,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.
-
--- a/src/Tools/jEdit/patches/jedit/extended_styles Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/patches/jedit/extended_styles Sat Dec 01 19:51:43 2012 +0100
@@ -1,7 +1,7 @@
-diff -ru jEdit/org/gjt/sp/jedit/gui/StyleEditor.java jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
---- jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2012-06-15 22:20:11.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2012-08-13 19:13:59.000000000 +0200
-@@ -78,7 +78,7 @@
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2012-11-17 16:41:58.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/gui/StyleEditor.java 2012-12-01 17:34:47.000000000 +0100
+@@ -79,7 +79,7 @@
start = next;
token = token.next;
}
@@ -10,21 +10,33 @@
{
JOptionPane.showMessageDialog(textArea.getView(),
jEdit.getProperty("syntax-style-no-token.message"),
-diff -ru jEdit/org/gjt/sp/jedit/syntax/Chunk.java jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2012-06-15 22:20:22.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2012-08-13 19:14:25.000000000 +0200
-@@ -380,7 +380,7 @@
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2012-11-17 16:42:25.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2012-12-01 18:28:35.000000000 +0100
+@@ -256,9 +256,9 @@
+ //{{{ Package private members
+
+ //{{{ Instance variables
+- SyntaxStyle style;
++ public SyntaxStyle style;
+ // set up after init()
+- float width;
++ public float width;
+ //}}}
+
+ //{{{ Chunk constructor
+@@ -506,7 +506,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 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 2012-06-15 22:20:22.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2012-08-13 19:14:44.000000000 +0200
+ private GlyphVector[] glyphs;
+ //}}}
+
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/syntax/Token.java 2012-11-17 16:42:25.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/syntax/Token.java 2012-12-01 17:37:04.000000000 +0100
@@ -57,7 +57,7 @@
*/
public static String tokenToString(byte token)
@@ -34,9 +46,9 @@
} //}}}
//{{{ 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 2012-06-15 22:20:25.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2012-08-13 19:19:20.000000000 +0200
+diff -ru 5.0.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.0.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.0.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2012-11-17 16:42:30.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2012-12-01 17:40:33.000000000 +0100
@@ -194,7 +194,24 @@
{
return loadStyles(family,size,true);
@@ -76,3 +88,19 @@
+
private SyntaxUtilities(){}
}
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2012-11-17 16:41:43.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2012-12-01 17:28:12.000000000 +0100
+@@ -906,6 +906,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.
+
--- a/src/Tools/jEdit/patches/jedit/macos Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/patches/jedit/macos Sat Dec 01 19:51:43 2012 +0100
@@ -1,9 +1,9 @@
-diff -ru jEdit/org/gjt/sp/jedit/OperatingSystem.java jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java
---- jEdit/org/gjt/sp/jedit/OperatingSystem.java 2012-06-15 22:20:24.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java 2012-08-13 19:13:06.000000000 +0200
-@@ -317,6 +317,10 @@
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/OperatingSystem.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/OperatingSystem.java 2012-11-17 16:42:29.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/OperatingSystem.java 2012-12-01 17:32:47.000000000 +0100
+@@ -318,6 +318,10 @@
{
- os = OS2;
+ os = WINDOWS_NT;
}
+ else if(osName.contains("Mac OS X"))
+ {
@@ -12,9 +12,9 @@
else if(osName.contains("VMS"))
{
os = VMS;
-diff -ru jEdit/org/gjt/sp/jedit/Debug.java jEdit-patched/org/gjt/sp/jedit/Debug.java
---- jEdit/org/gjt/sp/jedit/Debug.java 2012-06-15 22:20:24.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/Debug.java 2012-08-13 19:44:43.000000000 +0200
+diff -ru 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java
+--- 5.0.0/jEdit/org/gjt/sp/jedit/Debug.java 2012-11-17 16:42:29.000000000 +0100
++++ 5.0.0/jEdit-patched/org/gjt/sp/jedit/Debug.java 2012-12-01 17:31:24.000000000 +0100
@@ -109,7 +109,8 @@
* used to handle a modifier key press in conjunction with an alphabet
* key. <b>On by default on MacOS.</b>
--- a/src/Tools/jEdit/patches/jedit/memory Sat Dec 01 17:23:50 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-diff -ru jEdit/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java jEdit-patched/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java
---- jEdit/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java 2012-06-15 22:20:10.000000000 +0200
-+++ jEdit-patched/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java 2012-08-13 19:11:51.000000000 +0200
-@@ -222,7 +222,7 @@
- } //}}}
-
- //{{{ Private members
-- private static final String memoryTestStr = "999/999Mb";
-+ private static final String memoryTestStr = "9999/9999Mb";
-
- private final LineMetrics lm;
- private final Color progressForeground;
--- a/src/Tools/jEdit/src/Isabelle.props Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Sat Dec 01 19:51:43 2012 +0100
@@ -14,10 +14,10 @@
#dependencies
plugin.isabelle.jedit.Plugin.depend.0=jdk 1.7
-plugin.isabelle.jedit.Plugin.depend.1=jedit 04.05.02.00
-plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 4.5
-plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 1.9
-plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.3
+plugin.isabelle.jedit.Plugin.depend.1=jedit 05.00.00.00
+plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.0
+plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.0
+plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.4
#options
plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
--- a/src/Tools/jEdit/src/document_view.scala Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sat Dec 01 19:51:43 2012 +0100
@@ -69,7 +69,9 @@
def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
- val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false)
+ val rich_text_area =
+ new Rich_Text_Area(text_area.getView, text_area, get_rendering _,
+ caret_visible = true, hovering = false)
/* perspective */
--- a/src/Tools/jEdit/src/jEdit.props Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Sat Dec 01 19:51:43 2012 +0100
@@ -181,11 +181,13 @@
isabelle-output.height=174
isabelle-output.width=412
isabelle-readme.dock-position=bottom
+isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=bottom
-isabelle-symbols.dock-position=bottom
+lang.usedefaultlocale=false
+largefilemode=full
line-end.shortcut=END
line-home.shortcut=HOME
-lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
+lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
print.font=IsabelleText
restore.remote=false
restore=false
@@ -199,6 +201,7 @@
sidekick.splitter.location=721
tip.show=false
twoStageSave=false
+vfs.browser.dock-position=floating
view.antiAlias=standard
view.blockCaret=true
view.caretBlink=false
@@ -208,6 +211,7 @@
view.fontsize=18
view.fracFontMetrics=false
view.gutter.fontsize=12
+view.gutter.lineNumbers=false
view.gutter.selectionAreaWidth=18
view.height=787
view.middleMousePaste=true
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Dec 01 19:51:43 2012 +0100
@@ -66,7 +66,9 @@
Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
- private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering, true)
+ private val rich_text_area =
+ new Rich_Text_Area(view, text_area, () => current_rendering,
+ caret_visible = false, hovering = true)
def refresh()
{
@@ -144,8 +146,6 @@
/* init */
- override def isCaretVisible: Boolean = false
-
getPainter.setStructureHighlightEnabled(false)
getPainter.setLineHighlightEnabled(false)
--- a/src/Tools/jEdit/src/rich_text_area.scala Sat Dec 01 17:23:50 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Dec 01 19:51:43 2012 +0100
@@ -27,6 +27,7 @@
view: View,
text_area: TextArea,
get_rendering: () => Rendering,
+ caret_visible: Boolean,
hovering: Boolean)
{
private val buffer = text_area.getBuffer
@@ -304,7 +305,7 @@
while (chunk != null) {
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)
+ x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
{
val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
@@ -316,7 +317,7 @@
else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
val caret_range =
- if (text_area.isCaretVisible)
+ if (caret_visible && text_area.isCaretVisible)
JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
else Text.Range(-1)
@@ -479,7 +480,7 @@
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
robust_rendering { _ =>
- if (text_area.isCaretVisible) {
+ if (caret_visible && text_area.isCaretVisible) {
val caret = text_area.getCaretPosition
if (start <= caret && caret == end - 1) {
val painter = text_area.getPainter