# HG changeset patch
# User wenzelm
# Date 1743759447 -7200
# Node ID 1c646ad68bd8af129777ec988666a0674027a20e
# Parent  144168941ca415c5da8292a42aa3f6e62b28ad5e
eliminated patch: imitate jEdit.gotoMarker more directly;

diff -r 144168941ca4 -r 1c646ad68bd8 src/Tools/jEdit/patches/vfs_marker
--- a/src/Tools/jEdit/patches/vfs_marker	Fri Apr 04 11:21:01 2025 +0200
+++ b/src/Tools/jEdit/patches/vfs_marker	Fri Apr 04 11:37:27 2025 +0200
@@ -71,16 +71,7 @@
  	{
 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java	2024-08-03 19:53:14.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java	2025-04-02 21:46:10.377166514 +0200
-@@ -1553,7 +1553,7 @@
- 		{
- 			if (arg == null)
- 				continue;
--			else if (arg.startsWith("+line:") || arg.startsWith("+marker:"))
-+			else if (arg.startsWith("+offset:") || arg.startsWith("+line:") || arg.startsWith("+marker:"))
- 			{
- 				if (lastBuffer != null)
- 					gotoMarker(view, lastBuffer, arg);
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java	2024-10-29 11:50:54.062016616 +0100
 @@ -4233,7 +4233,7 @@
  	} //}}}
  
@@ -90,32 +81,3 @@
  		final String marker)
  	{
  		AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable()
-@@ -4243,8 +4243,27 @@
- 			{
- 				int pos;
- 
-+				// Handle offset
-+				if(marker.startsWith("+offset:"))
-+				{
-+					try
-+					{
-+						String arg = marker.substring(8);
-+						int offset = parseInt(arg);
-+						if (0 <= offset && offset <= buffer.getLength()) {
-+							pos = offset;
-+						}
-+						else {
-+							return;
-+						}
-+					}
-+					catch(Exception e)
-+					{
-+						return;
-+					}
-+				}
- 				// Handle line number
--				if(marker.startsWith("+line:"))
-+				else if(marker.startsWith("+line:"))
- 				{
- 					try
- 					{
diff -r 144168941ca4 -r 1c646ad68bd8 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 11:21:01 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 11:37:27 2025 +0200
@@ -14,6 +14,7 @@
 import org.gjt.sp.jedit.browser.VFSBrowser
 import org.gjt.sp.jedit.textarea.TextArea
 import org.gjt.sp.jedit.io.{VFSManager, VFSFile}
+import org.gjt.sp.util.AwtRunnableQueue
 
 
 class JEdit_Editor extends Editor[View] {
@@ -151,13 +152,30 @@
 
         if (is_dir) VFSBrowser.browseDirectory(view, name)
         else if (!Isabelle_System.open_external_file(name)) {
-          val marker =
-            if (offset >= 0) "+offset:" + offset
-            else if (line <= 0) ""
-            else if (column <= 0) "+line:" + (line + 1)
-            else "+line:" + (line + 1) + "," + (column + 1)
           val buffer = jEdit.openFile(view, name)
-          if (buffer != null && marker.nonEmpty) jEdit.gotoMarker(view, buffer, marker)
+          if (buffer != null) {
+            if (offset < 0) {
+              val marker =
+                if (line <= 0) ""
+                else if (column <= 0) "+line:" + (line + 1)
+                else "+line:" + (line + 1) + "," + (column + 1)
+              if (marker.nonEmpty) jEdit.gotoMarker(view, buffer, marker)
+            }
+            else {
+              AwtRunnableQueue.INSTANCE.runAfterIoTasks(() =>
+                if (view.getBuffer == buffer) {
+                  view.getTextArea.setCaretPosition(offset)
+                  buffer.setIntegerProperty(Buffer.CARET, offset)
+                  buffer.setBooleanProperty(Buffer.CARET_POSITIONED, true)
+                }
+                else {
+                  buffer.setIntegerProperty(Buffer.CARET, offset)
+                  buffer.setBooleanProperty(Buffer.CARET_POSITIONED, true)
+                  buffer.unsetProperty(Buffer.SCROLL_VERT)
+                }
+              )
+            }
+          }
         }
     }
   }