--- a/Admin/components/components.sha1 Wed Jan 30 21:18:26 2019 +0100
+++ b/Admin/components/components.sha1 Wed Jan 30 22:39:58 2019 +0100
@@ -146,6 +146,7 @@
cfa65bf8720b9b798ffa0986bafbc8437f44f758 jedit_build-20181026.tar.gz
847492b75b38468268f9ea424d27d53f2d95cef4 jedit_build-20181203.tar.gz
536a38ed527115b4bf2545a2137ec57b6ffad718 jedit_build-20190120.tar.gz
+58b9f03e5ec0b85f8123c31f5d8092dae5803773 jedit_build-20190130.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
--- a/Admin/components/main Wed Jan 30 21:18:26 2019 +0100
+++ b/Admin/components/main Wed Jan 30 22:39:58 2019 +0100
@@ -6,7 +6,7 @@
e-2.0-2
isabelle_fonts-20181129
jdk-11.0.2+9
-jedit_build-20190120
+jedit_build-20190130
jfreechart-1.5.0
jortho-1.0-2
kodkodi-1.5.2-1
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/vfs_marker Wed Jan 30 22:39:58 2019 +0100
@@ -0,0 +1,83 @@
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
+--- jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2018-04-09 01:57:42.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java 2019-01-30 22:18:22.534820468 +0100
+@@ -1204,6 +1204,7 @@
+ VFSFile[] selectedFiles = browserView.getSelectedFiles();
+
+ Buffer buffer = null;
++ String bufferMarker = null;
+
+ check_selected:
+ for (VFSFile file : selectedFiles)
+@@ -1253,7 +1254,10 @@
+ }
+
+ if (_buffer != null)
++ {
+ buffer = _buffer;
++ bufferMarker = file.getPathMarker();
++ }
+ }
+ // otherwise if a file is selected in OPEN_DIALOG or
+ // SAVE_DIALOG mode, just let the listener(s)
+@@ -1262,21 +1266,30 @@
+
+ if(buffer != null)
+ {
++ View gotoView = null;
++
+ switch(mode)
+ {
+ case M_OPEN:
+ view.setBuffer(buffer);
++ gotoView = view;
+ break;
+ case M_OPEN_NEW_VIEW:
+- jEdit.newView(view,buffer,false);
++ gotoView = jEdit.newView(view,buffer,false);
+ break;
+ case M_OPEN_NEW_PLAIN_VIEW:
+- jEdit.newView(view,buffer,true);
++ gotoView = jEdit.newView(view,buffer,true);
+ break;
+ case M_OPEN_NEW_SPLIT:
+ view.splitHorizontally().setBuffer(buffer);
++ gotoView = view;
+ break;
+ }
++
++ if (gotoView != null && bufferMarker != null)
++ {
++ jEdit.gotoMarker(gotoView, buffer, bufferMarker);
++ }
+ }
+
+ Object[] listeners = listenerList.getListenerList();
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
+--- jEdit/org/gjt/sp/jedit/io/VFSFile.java 2018-04-09 01:57:13.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2019-01-30 21:55:19.531911500 +0100
+@@ -297,6 +297,12 @@
+ }
+ } //}}}
+
++ //{{{ getPathMarker() method (for jEdit.gotoMarker)
++ public String getPathMarker()
++ {
++ return null;
++ } //}}}
++
+ //{{{ getPath() method
+ public String getPath()
+ {
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/jEdit.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
+--- jEdit/org/gjt/sp/jedit/jEdit.java 2018-04-09 01:56:22.000000000 +0200
++++ jEdit-patched/org/gjt/sp/jedit/jEdit.java 2019-01-30 21:56:00.171827173 +0100
+@@ -4479,7 +4479,7 @@
+ } //}}}
+
+ //{{{ gotoMarker() method
+- private static void gotoMarker(final View view, final Buffer buffer,
++ public static void gotoMarker(final View view, final Buffer buffer,
+ final String marker)
+ {
+ AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable()
--- a/src/Tools/jEdit/src/isabelle_session.scala Wed Jan 30 21:18:26 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_session.scala Wed Jan 30 22:39:58 2019 +0100
@@ -29,9 +29,11 @@
val vfs_prefix = "isabelle-session:"
- class Session_Entry(name: String, path: String)
+ class Session_Entry(name: String, path: String, marker: String)
extends VFSFile(name, path, null, VFSFile.FILE, 0L, false)
{
+ override def getPathMarker: String = marker
+
override def getExtendedAttribute(att: String): String =
if (att == JEdit_VFS.EA_SIZE) null
else super.getExtendedAttribute(att)
@@ -61,7 +63,12 @@
case Some(path) => File.platform_path(path)
case None => null
}
- new Session_Entry(name, path)
+ val marker =
+ Position.Line.unapply(info.pos) match {
+ case Some(line) => "+line:" + line
+ case None => null
+ }
+ new Session_Entry(name, path, marker)
}).toArray
}
case _ => null