# HG changeset patch # User wenzelm # Date 1354387903 -3600 # Node ID b655d2d0406d9d92dc2e335b4937d1cc2b8c170a # Parent 8290dc6c8d7f4d0d98449b7a9de7125b65fb88ce updated to jedit-5.0.0; diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/lib/Tools/jedit --- 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" ) diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/patches/jedit/annotation --- /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) + { + diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/patches/jedit/caret --- 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(); - } //}}} diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/patches/jedit/chunks --- 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. - diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/patches/jedit/extended_styles --- 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 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. + diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/patches/jedit/macos --- 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. On by default on MacOS. diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/patches/jedit/memory --- 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; diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/src/Isabelle.props --- 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 diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/src/document_view.scala --- 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 */ diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/src/jEdit.props --- 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 diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/src/pretty_text_area.scala --- 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) diff -r 8290dc6c8d7f -r b655d2d0406d src/Tools/jEdit/src/rich_text_area.scala --- 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