Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/vfs_marker
author wenzelm
Sat, 03 Oct 2020 19:56:02 +0200
changeset 72370 e25c0a6cc335
parent 72247 c06260b7152c
child 73653 d9823224fcfe
permissions -rw-r--r--
detect/guess arm32 platform (unsupported);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72247
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
     1
 
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
     2
 
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-09-03 05:31:04.000000000 +0200
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
     3
 
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-09-08 20:13:45.348505646 +0200
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset 
     4
 
@@ -1194,6 +1194,7 @@
69765
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
     5
 
 		VFSFile[] selectedFiles = browserView.getSelectedFiles();
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
     6
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
     7
 
 		Buffer buffer = null;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
     8
 
+		String bufferMarker = null;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
     9
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    10
 
 check_selected:
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    11
 
 		for (VFSFile file : selectedFiles)
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset 
    12
 
@@ -1243,7 +1244,10 @@
69765
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    13
 
 				}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    14
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    15
 
 				if (_buffer != null)
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    16
 
+				{
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    17
 
 					buffer = _buffer;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    18
 
+					bufferMarker = file.getPathMarker();
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    19
 
+				}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    20
 
 			}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    21
 
 			// otherwise if a file is selected in OPEN_DIALOG or
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    22
 
 			// SAVE_DIALOG mode, just let the listener(s)
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset 
    23
 
@@ -1252,21 +1256,30 @@
69765
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    24
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    25
 
 		if(buffer != null)
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    26
 
 		{
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    27
 
+			View gotoView = null;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    28
 
+
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    29
 
 			switch(mode)
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    30
 
 			{
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    31
 
 			case M_OPEN:
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    32
 
 				view.setBuffer(buffer);
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    33
 
+				gotoView = view;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    34
 
 				break;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    35
 
 			case M_OPEN_NEW_VIEW:
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    36
 
-				jEdit.newView(view,buffer,false);
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    37
 
+				gotoView = jEdit.newView(view,buffer,false);
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    38
 
 				break;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    39
 
 			case M_OPEN_NEW_PLAIN_VIEW:
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    40
 
-				jEdit.newView(view,buffer,true);
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    41
 
+				gotoView = jEdit.newView(view,buffer,true);
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    42
 
 				break;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    43
 
 			case M_OPEN_NEW_SPLIT:
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    44
 
 				view.splitHorizontally().setBuffer(buffer);
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    45
 
+				gotoView = view;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    46
 
 				break;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    47
 
 			}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    48
 
+
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    49
 
+			if (gotoView != null && bufferMarker != null)
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    50
 
+			{
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    51
 
+				jEdit.gotoMarker(gotoView, buffer, bufferMarker);
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    52
 
+			}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    53
 
 		}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    54
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    55
 
 		Object[] listeners = listenerList.getListenerList();
72247
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
    56
 
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
    57
 
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java	2020-09-03 05:31:03.000000000 +0200
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
    58
 
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2020-09-08 20:13:45.348505646 +0200
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset 
    59
 
@@ -302,6 +302,12 @@
69765
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    60
 
 		}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    61
 
 	} //}}}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    62
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    63
 
+	//{{{ getPathMarker() method (for jEdit.gotoMarker)
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    64
 
+	public String getPathMarker()
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    65
 
+	{
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    66
 
+		return null;
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    67
 
+	} //}}}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    68
 
+
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    69
 
 	//{{{ getPath() method
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    70
 
 	public String getPath()
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    71
 
 	{
72247
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
    72
 
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
    73
 
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java	2020-09-03 05:31:01.000000000 +0200
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset 
    74
 
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java	2020-09-08 20:13:45.348505646 +0200
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset 
    75
 
@@ -4242,7 +4242,7 @@
69765
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    76
 
 	} //}}}
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    77
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    78
 
 	//{{{ gotoMarker() method
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    79
 
-	private static void gotoMarker(final View view, final Buffer buffer,
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    80
 
+	public static void gotoMarker(final View view, final Buffer buffer,
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    81
 
 		final String marker)
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    82
 
 	{
c5778547ed03 more accurate file position;
wenzelm
parents:
diff changeset 
    83
 
 		AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable()
isabelle