src/Tools/jEdit/patches/vfs_marker
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (2 months ago ago)
changeset 70019 4419d4d675c3
parent 69781 c5778547ed03
permissions -rw-r--r--
formal update of patches -- no change of content;
     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
     2 --- 5.5.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java	2018-04-09 01:57:42.000000000 +0200
     3 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java	2019-02-24 12:23:42.403199825 +0100
     4 @@ -1204,6 +1204,7 @@
     5  		VFSFile[] selectedFiles = browserView.getSelectedFiles();
     6  
     7  		Buffer buffer = null;
     8 +		String bufferMarker = null;
     9  
    10  check_selected:
    11  		for (VFSFile file : selectedFiles)
    12 @@ -1253,7 +1254,10 @@
    13  				}
    14  
    15  				if (_buffer != null)
    16 +				{
    17  					buffer = _buffer;
    18 +					bufferMarker = file.getPathMarker();
    19 +				}
    20  			}
    21  			// otherwise if a file is selected in OPEN_DIALOG or
    22  			// SAVE_DIALOG mode, just let the listener(s)
    23 @@ -1262,21 +1266,30 @@
    24  
    25  		if(buffer != null)
    26  		{
    27 +			View gotoView = null;
    28 +
    29  			switch(mode)
    30  			{
    31  			case M_OPEN:
    32  				view.setBuffer(buffer);
    33 +				gotoView = view;
    34  				break;
    35  			case M_OPEN_NEW_VIEW:
    36 -				jEdit.newView(view,buffer,false);
    37 +				gotoView = jEdit.newView(view,buffer,false);
    38  				break;
    39  			case M_OPEN_NEW_PLAIN_VIEW:
    40 -				jEdit.newView(view,buffer,true);
    41 +				gotoView = jEdit.newView(view,buffer,true);
    42  				break;
    43  			case M_OPEN_NEW_SPLIT:
    44  				view.splitHorizontally().setBuffer(buffer);
    45 +				gotoView = view;
    46  				break;
    47  			}
    48 +
    49 +			if (gotoView != null && bufferMarker != null)
    50 +			{
    51 +				jEdit.gotoMarker(gotoView, buffer, bufferMarker);
    52 +			}
    53  		}
    54  
    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
    57 --- 5.5.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java	2018-04-09 01:57:13.000000000 +0200
    58 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java	2019-02-24 12:23:42.403199825 +0100
    59 @@ -297,6 +297,12 @@
    60  		}
    61  	} //}}}
    62  
    63 +	//{{{ getPathMarker() method (for jEdit.gotoMarker)
    64 +	public String getPathMarker()
    65 +	{
    66 +		return null;
    67 +	} //}}}
    68 +
    69  	//{{{ getPath() method
    70  	public String getPath()
    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
    73 --- 5.5.0/jEdit/org/gjt/sp/jedit/jEdit.java	2018-04-09 01:56:22.000000000 +0200
    74 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java	2019-02-24 12:23:42.403199825 +0100
    75 @@ -4479,7 +4479,7 @@
    76  	} //}}}
    77  
    78  	//{{{ gotoMarker() method
    79 -	private static void gotoMarker(final View view, final Buffer buffer,
    80 +	public static void gotoMarker(final View view, final Buffer buffer,
    81  		final String marker)
    82  	{
    83  		AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable()