src/Tools/jEdit/patches/vfs_marker
changeset 71932 65fd0f032a75
parent 69838 4419d4d675c3
child 72247 c06260b7152c
equal deleted inserted replaced
71931:0c8a9c028304 71932:65fd0f032a75
     1 diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
     1 diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
     2 --- 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java	2018-04-09 01:57:42.000000000 +0200
     2 --- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-05-20 11:10:12.000000000 +0200
     3 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2019-02-24 12:23:42.403199825 +0100
     3 +++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-06-10 15:37:37.310005209 +0200
     4 @@ -1204,6 +1204,7 @@
     4 @@ -1194,6 +1194,7 @@
     5  		VFSFile[] selectedFiles = browserView.getSelectedFiles();
     5  		VFSFile[] selectedFiles = browserView.getSelectedFiles();
     6  
     6  
     7  		Buffer buffer = null;
     7  		Buffer buffer = null;
     8 +		String bufferMarker = null;
     8 +		String bufferMarker = null;
     9  
     9  
    10  check_selected:
    10  check_selected:
    11  		for (VFSFile file : selectedFiles)
    11  		for (VFSFile file : selectedFiles)
    12 @@ -1253,7 +1254,10 @@
    12 @@ -1243,7 +1244,10 @@
    13  				}
    13  				}
    14  
    14  
    15  				if (_buffer != null)
    15  				if (_buffer != null)
    16 +				{
    16 +				{
    17  					buffer = _buffer;
    17  					buffer = _buffer;
    18 +					bufferMarker = file.getPathMarker();
    18 +					bufferMarker = file.getPathMarker();
    19 +				}
    19 +				}
    20  			}
    20  			}
    21  			// otherwise if a file is selected in OPEN_DIALOG or
    21  			// otherwise if a file is selected in OPEN_DIALOG or
    22  			// SAVE_DIALOG mode, just let the listener(s)
    22  			// SAVE_DIALOG mode, just let the listener(s)
    23 @@ -1262,21 +1266,30 @@
    23 @@ -1252,21 +1256,30 @@
    24  
    24  
    25  		if(buffer != null)
    25  		if(buffer != null)
    26  		{
    26  		{
    27 +			View gotoView = null;
    27 +			View gotoView = null;
    28 +
    28 +
    51 +				jEdit.gotoMarker(gotoView, buffer, bufferMarker);
    51 +				jEdit.gotoMarker(gotoView, buffer, bufferMarker);
    52 +			}
    52 +			}
    53  		}
    53  		}
    54  
    54  
    55  		Object[] listeners = listenerList.getListenerList();
    55  		Object[] listeners = listenerList.getListenerList();
    56 diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
    56 diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
    57 --- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java	2018-04-09 01:57:13.000000000 +0200
    57 --- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java	2020-05-20 11:10:11.000000000 +0200
    58 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2019-02-24 12:23:42.403199825 +0100
    58 +++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2020-06-10 15:37:37.314005109 +0200
    59 @@ -297,6 +297,12 @@
    59 @@ -302,6 +302,12 @@
    60  		}
    60  		}
    61  	} //}}}
    61  	} //}}}
    62  
    62  
    63 +	//{{{ getPathMarker() method (for jEdit.gotoMarker)
    63 +	//{{{ getPathMarker() method (for jEdit.gotoMarker)
    64 +	public String getPathMarker()
    64 +	public String getPathMarker()
    67 +	} //}}}
    67 +	} //}}}
    68 +
    68 +
    69  	//{{{ getPath() method
    69  	//{{{ getPath() method
    70  	public String getPath()
    70  	public String getPath()
    71  	{
    71  	{
    72 diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/jEdit.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
    72 diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java
    73 --- 5.5.0/jEdit/org/gjt/sp/jedit/jEdit.java	2018-04-09 01:56:22.000000000 +0200
    73 --- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java	2020-05-26 16:55:37.000000000 +0200
    74 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java	2019-02-24 12:23:42.403199825 +0100
    74 +++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java	2020-06-10 15:37:37.314005109 +0200
    75 @@ -4479,7 +4479,7 @@
    75 @@ -4242,7 +4242,7 @@
    76  	} //}}}
    76  	} //}}}
    77  
    77  
    78  	//{{{ gotoMarker() method
    78  	//{{{ gotoMarker() method
    79 -	private static void gotoMarker(final View view, final Buffer buffer,
    79 -	private static void gotoMarker(final View view, final Buffer buffer,
    80 +	public static void gotoMarker(final View view, final Buffer buffer,
    80 +	public static void gotoMarker(final View view, final Buffer buffer,