--- a/Admin/components/components.sha1 Fri Apr 04 16:38:16 2025 +0100
+++ b/Admin/components/components.sha1 Fri Apr 04 22:20:30 2025 +0200
@@ -263,6 +263,8 @@
011d322d4ae1f8c57112bd695f5e812e48e1d953 jedit-20250130.tar.gz
8a1a29b585240766a34784e152f769d0df007425 jedit-20250209.tar.gz
12f22ccb48a0a7dc9ad8c1b27552e8fd26d4ae0c jedit-20250215.tar.gz
+1aa375149dc5e84cfdd64bf66e7e0f68319b7db7 jedit-20250402.tar.gz
+88c9cc14f5618ad21ca17664fdb57b8f5f6f6d2e jedit-20250404.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
@@ -368,6 +370,7 @@
da83a3350cf27ca1ab3c86de6b6b60178cfda0db naproche-20250201.tar.gz
434e2a6dc6fe681f7cb7b4e348fd26dbada17e61 naproche-20250228.tar.gz
a7524802f0a12c3dc3cee594d8b22b91848eecb5 naproche-20250310.tar.gz
+66f828e98434375f244aac73101095df037055e7 naproche-20250328.tar.gz
d098dd0873b1720a77dc4e060267f9a6c93f341a naproche-2d99afe5c349.tar.gz
4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz
77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz
--- a/Admin/components/main Fri Apr 04 16:38:16 2025 +0100
+++ b/Admin/components/main Fri Apr 04 22:20:30 2025 +0200
@@ -16,7 +16,7 @@
isabelle_setup-20240327
javamail-20250122
jdk-21.0.6
-jedit-20250215
+jedit-20250404
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.18.3
--- a/NEWS Fri Apr 04 16:38:16 2025 +0100
+++ b/NEWS Fri Apr 04 22:20:30 2025 +0200
@@ -30,6 +30,13 @@
This runs Isabelle/jEdit with sequential evaluation in ML, without
affecting stored preferences of option "threads".
+* Isabelle/jEdit provides builtin navigation support, with actions
+navigate-backwards (AS-LEFT) and navigate-forwards (AS-RIGHT). These
+actions are available via arrow icons in the Search Bar, which is now
+enabled by default. The old plugins Navigator and Code2HTML are now
+longer included. The old-fashioned toolbar, with its old Navigator
+icons, is now disabled by default.
+
*** HOL ***
--- a/etc/build.props Fri Apr 04 16:38:16 2025 +0100
+++ b/etc/build.props Fri Apr 04 22:20:30 2025 +0200
@@ -303,6 +303,7 @@
src/Tools/jEdit/src/isabelle.scala \
src/Tools/jEdit/src/isabelle_encoding.scala \
src/Tools/jEdit/src/isabelle_export.scala \
+ src/Tools/jEdit/src/isabelle_navigator.scala \
src/Tools/jEdit/src/isabelle_session.scala \
src/Tools/jEdit/src/isabelle_vfs.scala \
src/Tools/jEdit/src/jedit_bibtex.scala \
--- a/src/Doc/JEdit/JEdit.thy Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Doc/JEdit/JEdit.thy Fri Apr 04 22:20:30 2025 +0200
@@ -151,11 +151,10 @@
additional plugins are bundled with Isabelle/jEdit for convenience or out of
necessity, notably \<^emph>\<open>Console\<close> with its \<^emph>\<open>Scala\<close> sub-plugin
(\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
- parsers for document tree structure (\secref{sec:sidekick}). The
- \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
- formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
- (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
- of bundled plugins, but have no particular use in Isabelle/jEdit.
+ parsers for document tree structure (\secref{sec:sidekick}). Other plugins
+ (e.g.\ \<^emph>\<open>Console\<close>, \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>SideKick\<close>) are included to saturate the
+ dependencies of bundled plugins, but have no particular use in
+ Isabelle/jEdit.
\<close>
@@ -1267,9 +1266,17 @@
\<^medskip>
A black rectangle in the text indicates a hyperlink that may be followed by
a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still
- pressed). Such jumps to other text locations are recorded by the
- \<^emph>\<open>Navigator\<close> plugin, which is bundled with Isabelle/jEdit and enabled by
- default. There are usually navigation arrows in the main jEdit toolbar.
+ pressed). Such jumps to other text locations are recorded by the builtin
+ navigator, which provides actions to move backwards or forwards, with arrow
+ icons in the \<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref
+ "quick-search"}). The following keyboard shortcuts are available:
+
+ \<^medskip>
+ \begin{tabular}[t]{l}
+ @{action_ref "navigate-backwards"} (\<^verbatim>\<open>AS+LEFT\<close>) \\
+ @{action_ref "navigate-forwards"} (\<^verbatim>\<open>AS+RIGHT\<close>) \\
+ \end{tabular}\quad
+ \<^medskip>
Note that the link target may be a file that is itself not subject to formal
document processing of the editor session and thus prevents further
--- a/src/Pure/Admin/component_jedit.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Pure/Admin/component_jedit.scala Fri Apr 04 22:20:30 2025 +0200
@@ -89,12 +89,10 @@
private val download_plugins: List[(String, String)] =
List(
- "Code2HTML" -> "0.7",
"CommonControls" -> "1.7.4",
"Console" -> "5.1.4",
"ErrorList" -> "2.4.0",
"Highlight" -> "2.5",
- "Navigator" -> "2.7",
"SideKick" -> "1.8")
private def exclude_package(name: String): Boolean =
@@ -340,6 +338,13 @@
metal.primary.fontsize=12
metal.secondary.font=Isabelle DejaVu Sans
metal.secondary.fontsize=12
+navigate-backwards.label=Navigate backwards
+navigate-backwards.shortcut=AS+LEFT
+navigate-backwards.icon=ArrowL.png
+navigate-forwards.label=Navigate forwards
+navigate-forwards.shortcut=AS+RIGHT
+navigate-forwards.icon=ArrowR.png
+navigate-toolbar=navigate-backwards navigate-forwards
navigator.showOnToolbar=true
new-file-in-mode.shortcut=
next-bracket.shortcut2=C+e C+9
@@ -358,6 +363,7 @@
recent-buffer.shortcut2=C+CIRCUMFLEX
restore.remote=false
restore=false
+search.find=Search:
search.subdirs.toggle=true
select-block.shortcut2=C+8
sidekick-tree.dock-position=right
@@ -404,7 +410,8 @@
view.gutter.selectionAreaWidth=18
view.height=850
view.middleMousePaste=true
-view.showToolbar=true
+view.showSearchbar=true
+view.showToolbar=false
view.status.memory.background=#666699
view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
view.thickCaret=true
--- a/src/Pure/General/linear_set.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Pure/General/linear_set.scala Fri Apr 04 22:20:30 2025 +0200
@@ -37,10 +37,12 @@
final class Linear_Set[A] private(
start: Option[A],
end: Option[A],
- val nexts: Map[A, A], prevs: Map[A, A])
- extends Iterable[A]
+ nexts: Map[A, A],
+ prevs: Map[A, A]
+) extends Iterable[A]
with SetOps[A, Linear_Set, Linear_Set[A]]
with IterableFactoryDefaults[A, Linear_Set] {
+
/* relative addressing */
def next(elem: A): Option[A] =
--- a/src/Pure/PIDE/text.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Pure/PIDE/text.scala Fri Apr 04 22:20:30 2025 +0200
@@ -137,8 +137,10 @@
/* editing */
object Edit {
- def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
- def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
+ def make(is_insert: Boolean, start: Offset, text: String): Edit =
+ new Edit(is_insert, start, text)
+ def insert(start: Offset, text: String): Edit = make(true, start, text)
+ def remove(start: Offset, text: String): Edit = make(false, start, text)
def inserts(start: Offset, text: String): List[Edit] =
if (text == "") Nil else List(insert(start, text))
def removes(start: Offset, text: String): List[Edit] =
--- a/src/Tools/jEdit/jedit_main/actions.xml Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Tools/jEdit/jedit_main/actions.xml Fri Apr 04 22:20:30 2025 +0200
@@ -2,6 +2,16 @@
<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
<ACTIONS>
+ <ACTION NAME="navigate-backwards">
+ <CODE>
+ isabelle.jedit.Isabelle.navigate_backwards(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="navigate-forwards">
+ <CODE>
+ isabelle.jedit.Isabelle.navigate_forwards(view);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.browser-info">
<CODE>
isabelle.jedit.Isabelle.open_browser_info(view);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/search_bar Fri Apr 04 22:20:30 2025 +0200
@@ -0,0 +1,14 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2025-04-03 11:33:23.921426197 +0200
+@@ -51,6 +51,10 @@
+ setFloatable(false);
+ add(Box.createHorizontalStrut(2));
+
++ if (!jEdit.getProperty("navigate-toolbar", "").isEmpty()) {
++ add(GUIUtilities.loadToolBar("navigate-toolbar"));
++ }
++
+ JLabel label = new JLabel(jEdit.getProperty("view.search.find"));
+ add(label);
+
--- a/src/Tools/jEdit/src/document_model.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Apr 04 22:20:30 2025 +0200
@@ -18,7 +18,7 @@
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
object Document_Model {
@@ -568,6 +568,8 @@
PIDE.editor.invoke()
}
+ val listener: BufferListener = JEdit_Lib.buffer_listener((_, e) => edit(List(e)))
+
// blob
@@ -621,31 +623,6 @@
def untyped_data: AnyRef = buffer_state.untyped_data
- /* buffer listener */
-
- private val buffer_listener: BufferListener = new BufferAdapter {
- override def contentInserted(
- buffer: JEditBuffer,
- start_line: Int,
- offset: Int,
- num_lines: Int,
- length: Int
- ): Unit = {
- buffer_state.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
- }
-
- override def preContentRemoved(
- buffer: JEditBuffer,
- start_line: Int,
- offset: Int,
- num_lines: Int,
- removed_length: Int
- ): Unit = {
- buffer_state.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
- }
- }
-
-
/* syntax */
def syntax_changed(): Unit = {
@@ -681,7 +658,7 @@
Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
}
- buffer.addBufferListener(buffer_listener)
+ buffer.addBufferListener(buffer_state.listener)
init_token_marker()
this
@@ -691,7 +668,7 @@
/* exit */
def exit(): File_Model = GUI_Thread.require {
- buffer.removeBufferListener(buffer_listener)
+ buffer.removeBufferListener(buffer_state.listener)
init_token_marker()
File_Model.init(session,
--- a/src/Tools/jEdit/src/font_info.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Tools/jEdit/src/font_info.scala Fri Apr 04 22:20:30 2025 +0200
@@ -49,7 +49,7 @@
jEdit.setIntegerProperty("view.fontsize", size)
jEdit.propertiesChanged()
jEdit.saveSettings()
- jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
+ jEdit.getActiveView.getStatus.setMessageAndClear("Text font size: " + size)
}
}
--- a/src/Tools/jEdit/src/isabelle.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Apr 04 22:20:30 2025 +0200
@@ -82,6 +82,12 @@
}
+ /* navigation */
+
+ def navigate_backwards(view: View): Unit = PIDE.plugin.navigator.backward(view)
+ def navigate_forwards(view: View): Unit = PIDE.plugin.navigator.forward(view)
+
+
/* text structure */
def indent_rule(mode: String): Option[IndentRule] =
@@ -459,8 +465,7 @@
else Symbol.cartouche(arg.get)
buffer.remove(antiq_range.start, antiq_range.length)
- text_area.moveCaretPosition(antiq_range.start)
- text_area.selectNone
+ text_area.setCaretPosition(antiq_range.start)
text_area.setSelectedText(op_text + arg_text)
}
}
@@ -563,7 +568,8 @@
val errs = rendering.errors(range).filterNot(_.range.overlaps(avoid_range))
get(errs) match {
case Some(err) =>
- PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start)
+ PIDE.editor.goto_file(
+ false, view, JEdit_Lib.buffer_name(view.getBuffer), offset = err.range.start)
case None =>
view.getStatus.setMessageAndClear("No " + which + "error in current document snapshot")
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_navigator.scala Fri Apr 04 22:20:30 2025 +0200
@@ -0,0 +1,197 @@
+/* Title: Tools/jEdit/src/isabelle_navigator.scala
+ Author: Makarius
+
+Navigate history of notable source positions.
+*/
+
+package isabelle.jedit
+
+
+import org.gjt.sp.jedit.{View, Buffer, EditPane}
+
+
+import isabelle._
+
+object Isabelle_Navigator {
+ object Pos {
+ val none: Pos = new Pos(Document_ID.none, "", 0)
+ def make(name: String, offset: Int): Pos = new Pos(Document_ID.make(), name, offset)
+
+ def apply(buffer: Buffer): Pos =
+ if (buffer == null) Pos.none else make(JEdit_Lib.buffer_name(buffer), 0)
+
+ def apply(edit_pane: EditPane): Pos =
+ if (edit_pane == null) none
+ else {
+ val buffer = edit_pane.getBuffer
+ if (buffer != null && buffer.isLoaded && !buffer.isUntitled) {
+ make(JEdit_Lib.buffer_name(buffer), edit_pane.getTextArea.getCaretPosition)
+ }
+ else none
+ }
+
+ def apply(view: View): Pos =
+ if (view == null) none else apply(view.getEditPane)
+ }
+
+ final class Pos private(
+ val id: Document_ID.Generic,
+ val name: String,
+ val offset: Int
+ ) {
+ def defined: Boolean = id != Document_ID.none
+
+ override def toString: String =
+ if (defined) "(offset " + offset + " of " + quote(name) + ")" else "Pos.none"
+
+ override def hashCode: Int = id.hashCode
+ override def equals(other: Any): Boolean =
+ other match {
+ case that: Pos => id == that.id
+ case _ => false
+ }
+
+ def equiv(that: Pos): Boolean = name == that.name && offset == that.offset
+
+ def convert(edit_name: String, edit: Text.Edit): Pos = {
+ if (name == edit_name) {
+ val offset1 = edit.convert(offset)
+ if (offset == offset1) this else Pos.make(name, offset1)
+ }
+ else this
+ }
+ }
+
+ object History {
+ val limit: Int = 500
+ val empty: History = new History(Linear_Set.empty)
+ }
+
+ class History(hist: Linear_Set[Pos]) {
+ override def toString: String =
+ size match {
+ case 0 => "History.empty"
+ case n => "History(" + n + ")"
+ }
+ def is_empty: Boolean = hist.isEmpty
+ def size: Int = hist.size
+ def iterator: Iterator[Pos] = hist.iterator
+
+ def top: Pos = if (hist.isEmpty) Pos.none else hist.head
+ def pop: History = if (hist.isEmpty) this else new History(hist.delete_after(None))
+
+ def push(pos: Pos): History =
+ if (!pos.defined || pos.equiv(top)) this
+ else {
+ val hist1 =
+ if (hist.size < History.limit) hist
+ else hist.delete_after(hist.prev(hist.last))
+ new History(hist1.insert_after(None, pos))
+ }
+
+ def convert(name: String, edit: Text.Edit): History =
+ new History(
+ hist.foldLeft(hist) {
+ case (h, pos) =>
+ val prev = h.prev(pos)
+ val pos0 = prev.getOrElse(Pos.none)
+ val pos1 = pos.convert(name, edit)
+ if (pos1.equiv(pos0)) h.delete_after(prev)
+ else if (pos1.equiv(pos)) h
+ else h.delete_after(prev).insert_after(prev, pos1)
+ }
+ )
+
+ def close(names: Set[String]): History =
+ new History(
+ hist.foldLeft(hist) {
+ case (h, pos) =>
+ val prev = h.prev(pos)
+ val pos0 = prev.getOrElse(Pos.none)
+ if (names.contains(pos.name) || pos.equiv(pos0)) h.delete_after(prev)
+ else h
+ }
+ )
+ }
+
+ final class State private[Isabelle_Navigator](view: View) {
+ }
+}
+
+class Isabelle_Navigator {
+ import Isabelle_Navigator.{Pos, History}
+
+ // owned by GUI thread
+ private var _bypass = false
+ private var _backward = History.empty
+ private var _forward = History.empty
+
+ def current: Pos = _backward.top
+ def recurrent: Pos = _forward.top
+
+ override def toString: String = {
+ val size = _backward.size + _forward.size
+ "Isabelle_Navigator(" + (if (size == 0) "" else size.toString) + ")"
+ }
+
+ private def convert(name: String, edit: Text.Edit): Unit = GUI_Thread.require {
+ _backward = _backward.convert(name, edit)
+ _forward = _forward.convert(name, edit)
+ }
+
+ private def close(names: Set[String]): Unit = GUI_Thread.require {
+ _backward = _backward.close(names)
+ _forward = _forward.close(names)
+ }
+
+ private val buffer_listener =
+ JEdit_Lib.buffer_listener((buffer, edit) => convert(JEdit_Lib.buffer_name(buffer), edit))
+
+ def exit(buffers: IterableOnce[Buffer]): Unit = GUI_Thread.require {
+ buffers.iterator.foreach(_.removeBufferListener(buffer_listener))
+ close(buffers.iterator.map(JEdit_Lib.buffer_name).toSet)
+ }
+
+ def init(buffers: IterableOnce[Buffer]): Unit = GUI_Thread.require {
+ exit(buffers)
+ buffers.iterator.foreach(_.addBufferListener(buffer_listener))
+ }
+
+ def record(pos: Pos): Unit = GUI_Thread.require {
+ if (!_bypass && pos.defined && !pos.equiv(current)) {
+ _backward = _backward.push(pos)
+ _forward = History.empty
+ }
+ }
+
+ def record(buffer: Buffer): Unit = record(Pos(buffer))
+ def record(edit_pane: EditPane): Unit = record(Pos(edit_pane))
+ def record(view: View): Unit = record(Pos(view))
+
+ def goto_current(view: View): Unit = GUI_Thread.require {
+ if (current.defined) {
+ val b = _bypass
+ try {
+ _bypass = true
+ PIDE.editor.goto_file(true, view, current.name, offset = current.offset)
+ }
+ finally { _bypass = b }
+ }
+ }
+
+ def backward(view: View): Unit = GUI_Thread.require {
+ if (!_backward.is_empty) {
+ _forward = _forward.push(current).push(Pos(view))
+ _backward = _backward.pop
+ goto_current(view)
+ }
+ }
+
+ def forward(view: View): Unit = GUI_Thread.require {
+ if (!_forward.is_empty) {
+ _backward = _backward.push(recurrent)
+ _forward = _forward.pop
+ goto_current(view)
+ }
+ }
+}
--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 04 22:20:30 2025 +0200
@@ -12,7 +12,9 @@
import org.gjt.sp.jedit.{jEdit, View, Buffer}
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] {
@@ -109,53 +111,28 @@
/* navigation */
- def push_position(view: View): Unit = {
- val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
- if (navigator != null) {
- try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
- catch { case _: NoSuchMethodException => }
- }
- }
-
- def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit = {
+ def goto_file(
+ focus: Boolean,
+ view: View,
+ name: String,
+ line: Int = -1,
+ offset: Text.Offset = -1,
+ at_target: (Buffer, Text.Offset) => Unit = (_, _) => ()
+ ): Unit = {
GUI_Thread.require {}
- push_position(view)
-
- if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
- try { view.getTextArea.moveCaretPosition(offset) }
- catch {
- case _: ArrayIndexOutOfBoundsException =>
- case _: IllegalArgumentException =>
- }
- }
+ PIDE.plugin.navigator.record(view)
- def goto_file(focus: Boolean, view: View, name: String): Unit =
- goto_file(focus, view, Line.Node_Position.offside(name))
-
- def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit = {
- GUI_Thread.require {}
-
- push_position(view)
-
- val name = pos.name
- val line = pos.line
- val column = pos.column
+ def buffer_offset(buffer: Buffer): Text.Offset =
+ ((if (line < 0) 0 else buffer.getLineStartOffset(line min buffer.getLineCount)) +
+ (if (offset < 0) 0 else offset)) min buffer.getLength
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
- val text_area = view.getTextArea
-
- try {
- val line_start = text_area.getBuffer.getLineStartOffset(line)
- text_area.moveCaretPosition(line_start)
- if (column > 0) text_area.moveCaretPosition(line_start + column)
- }
- catch {
- case _: ArrayIndexOutOfBoundsException =>
- case _: IllegalArgumentException =>
- }
+ val target = buffer_offset(buffer)
+ view.getTextArea.setCaretPosition(target)
+ at_target(buffer, target)
case None =>
val is_dir =
@@ -168,11 +145,23 @@
if (is_dir) VFSBrowser.browseDirectory(view, name)
else if (!Isabelle_System.open_external_file(name)) {
- val args =
- if (line <= 0) Array(name)
- else if (column <= 0) Array(name, "+line:" + (line + 1))
- else Array(name, "+line:" + (line + 1) + "," + (column + 1))
- jEdit.openFiles(view, null, args)
+ val buffer = jEdit.openFile(view, name)
+ if (buffer != null && (line >= 0 || offset >= 0)) {
+ AwtRunnableQueue.INSTANCE.runAfterIoTasks({ () =>
+ val target = buffer_offset(buffer)
+ if (view.getBuffer == buffer) {
+ view.getTextArea.setCaretPosition(target)
+ buffer.setIntegerProperty(Buffer.CARET, target)
+ buffer.setBooleanProperty(Buffer.CARET_POSITIONED, true)
+ at_target(buffer, target)
+ }
+ else {
+ buffer.setIntegerProperty(Buffer.CARET, target)
+ buffer.setBooleanProperty(Buffer.CARET_POSITIONED, true)
+ buffer.unsetProperty(Buffer.SCROLL_VERT)
+ }
+ })
+ }
}
}
}
@@ -209,27 +198,20 @@
override def toString: String = "URL " + quote(name)
}
- def hyperlink_file(focus: Boolean, name: String): Hyperlink =
- hyperlink_file(focus, Line.Node_Position.offside(name))
-
- def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
+ def hyperlink_file(
+ focus: Boolean,
+ name: String,
+ line: Int = -1,
+ offset: Text.Offset = -1
+ ): Hyperlink =
new Hyperlink {
- def follow(view: View): Unit = goto_file(focus, view, pos)
- override def toString: String = "file " + quote(pos.name)
- }
-
- def hyperlink_model(focus: Boolean, model: Document_Model, offset: Text.Offset): Hyperlink =
- model match {
- case file_model: File_Model =>
- val pos =
- try { file_model.node_position(offset) }
- catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) }
- hyperlink_file(focus, pos)
- case buffer_model: Buffer_Model =>
- new Hyperlink {
- def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset)
- override def toString: String = "buffer " + quote(model.node_name.node)
- }
+ def follow(view: View): Unit = {
+ import Isabelle_Navigator.Pos
+ PIDE.plugin.navigator.record(Pos(view))
+ goto_file(focus, view, name, line = line, offset = offset,
+ at_target = (buffer, target) => Pos.make(JEdit_Lib.buffer_name(buffer), target))
+ }
+ override def toString: String = "file " + quote(name)
}
def hyperlink_source_file(
@@ -240,7 +222,7 @@
) : Option[Hyperlink] = {
for (platform_path <- PIDE.resources.source_file(source_name)) yield {
def hyperlink(pos: Line.Position) =
- hyperlink_file(focus, Line.Node_Position(platform_path, pos))
+ hyperlink_file(focus, platform_path, line = pos.line, offset = pos.column)
if (offset > 0) {
PIDE.resources.get_file_content(PIDE.resources.node_name(platform_path)) match {
@@ -263,7 +245,10 @@
offset: Symbol.Offset = 0
) : Option[Hyperlink] = {
if (snapshot.is_outdated) None
- else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
+ else {
+ snapshot.find_command_position(id, offset)
+ .map(pos => hyperlink_file(focus, pos.name, line = pos.line, offset = pos.column))
+ }
}
def is_hyperlink_position(
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Apr 04 22:20:30 2025 +0200
@@ -23,7 +23,7 @@
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
-import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
+import org.gjt.sp.jedit.buffer.{BufferListener, BufferAdapter, JEditBuffer, LineManager}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection, AntiAlias}
@@ -111,7 +111,7 @@
jEdit.getViewManager().getViews().asScala.iterator
def jedit_view(view: View = null): View =
- if (view == null) jEdit.getActiveView() else view
+ if (view == null) jEdit.getActiveView else view
def jedit_edit_panes(view: View): Iterator[EditPane] =
if (view == null) Iterator.empty
@@ -403,10 +403,28 @@
}
+ /* buffer event handling */
+
+ private def buffer_edit(ins: Boolean, buf: JEditBuffer, i: Text.Offset, n: Int): Text.Edit = {
+ val try_range = Text.Range(i, i + n.max(0)).try_restrict(buffer_range(buf))
+ val edit_range = try_range.getOrElse(Text.Range.zero)
+ val edit_text = try_range.flatMap(get_text(buf, _)).getOrElse("")
+ Text.Edit.make(ins, edit_range.start, edit_text)
+ }
+
+ def buffer_listener(handle: (Buffer, Text.Edit) => Unit): BufferListener =
+ new BufferAdapter {
+ override def contentInserted(buf: JEditBuffer, line: Int, i: Int, lines: Int, n: Int): Unit =
+ handle(buf.asInstanceOf[Buffer], buffer_edit(true, buf, i, n))
+ override def preContentRemoved(buf: JEditBuffer, line: Int, i: Int, lines: Int, n: Int): Unit =
+ handle(buf.asInstanceOf[Buffer], buffer_edit(false, buf, i, n))
+ }
+
+
/* key event handling */
def request_focus_view(alt_view: View = null): Unit = {
- val view = if (alt_view != null) alt_view else jEdit.getActiveView()
+ val view = if (alt_view != null) alt_view else jEdit.getActiveView
if (view != null) {
val text_area = view.getTextArea
if (text_area != null) text_area.requestFocus()
--- a/src/Tools/jEdit/src/main_plugin.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Fri Apr 04 22:20:30 2025 +0200
@@ -16,8 +16,8 @@
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
import org.gjt.sp.jedit.textarea.JEditTextArea
import org.gjt.sp.jedit.syntax.ModeProvider
-import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged,
- ViewUpdate}
+import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, BufferChanging, PositionChanging,
+ EditPaneUpdate, PropertiesChanged, ViewUpdate}
import org.gjt.sp.util.Log
@@ -96,6 +96,7 @@
val completion_history = new Completion.History_Variable
val spell_checker = new Spell_Checker_Variable
+ val navigator = new Isabelle_Navigator
/* theory files */
@@ -301,67 +302,80 @@
if (startup_failure.isEmpty) {
message match {
case _: EditorStarted =>
+ val view = jEdit.getActiveView
+
try { resources.session_background.check_errors }
catch {
case ERROR(msg) =>
- GUI.warning_dialog(jEdit.getActiveView,
+ GUI.warning_dialog(view,
"Bad session structure: may cause problems with theory imports",
GUI.scrollable_text(msg))
}
jEdit.propertiesChanged()
- val view = jEdit.getActiveView()
- init_editor(view)
+ if (view != null) {
+ init_editor(view)
- PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
- JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
+ PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
+ JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
+ }
- case msg: ViewUpdate
- if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>
- init_title(msg.getView)
-
- case msg: BufferUpdate
- if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
- if (msg.getBuffer != null) {
- exit_models(List(msg.getBuffer))
- PIDE.editor.invoke_generated()
+ case msg: ViewUpdate =>
+ val what = msg.getWhat
+ val view = msg.getView
+ what match {
+ case ViewUpdate.CREATED if view != null => init_title(view)
+ case _ =>
}
- case msg: BufferUpdate
- if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
- if (session.is_ready) {
- delay_init.invoke()
- delay_load.invoke()
+ case msg: BufferUpdate =>
+ val what = msg.getWhat
+ val buffer = msg.getBuffer
+ val view = msg.getView
+ val view_edit_pane = if (view == null) null else view.getEditPane
+
+ what match {
+ case BufferUpdate.LOAD_STARTED | BufferUpdate.CLOSING if buffer != null =>
+ exit_models(List(buffer))
+ PIDE.editor.invoke_generated()
+ case BufferUpdate.PROPERTIES_CHANGED | BufferUpdate.LOADED if session.is_ready =>
+ delay_init.invoke()
+ delay_load.invoke()
+ case _ =>
}
- case msg: EditPaneUpdate
- if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
- msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
- msg.getWhat == EditPaneUpdate.CREATED ||
- msg.getWhat == EditPaneUpdate.DESTROYED =>
+ if (buffer != null && !buffer.isUntitled) {
+ what match {
+ case BufferUpdate.CREATED => navigator.init(Set(buffer))
+ case BufferUpdate.CLOSED => navigator.exit(Set(buffer))
+ case _ =>
+ }
+ }
+
+ case msg: EditPaneUpdate =>
+ val what = msg.getWhat
val edit_pane = msg.getEditPane
- val buffer = edit_pane.getBuffer
- val text_area = edit_pane.getTextArea
+ val buffer = if (edit_pane == null) null else edit_pane.getBuffer
+ val text_area = if (edit_pane == null) null else edit_pane.getTextArea
if (buffer != null && text_area != null) {
- if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
- msg.getWhat == EditPaneUpdate.CREATED) {
- if (session.is_ready)
- init_view(buffer, text_area)
+ if (what == EditPaneUpdate.BUFFER_CHANGED || what == EditPaneUpdate.CREATED) {
+ if (session.is_ready) init_view(buffer, text_area)
}
- else {
+
+ if (what == EditPaneUpdate.BUFFER_CHANGING || what == EditPaneUpdate.DESTROYED) {
Isabelle.dismissed_popups(text_area.getView)
exit_view(buffer, text_area)
}
- if (msg.getWhat == EditPaneUpdate.CREATED)
- Completion_Popup.Text_Area.init(text_area)
+ if (what == EditPaneUpdate.CREATED) Completion_Popup.Text_Area.init(text_area)
- if (msg.getWhat == EditPaneUpdate.DESTROYED)
- Completion_Popup.Text_Area.exit(text_area)
+ if (what == EditPaneUpdate.DESTROYED) Completion_Popup.Text_Area.exit(text_area)
}
+ if (msg.isInstanceOf[PositionChanging]) navigator.record(edit_pane)
+
case _: PropertiesChanged =>
for {
view <- JEdit_Lib.jedit_views()
@@ -428,6 +442,7 @@
spell_checker.update(options.value)
JEdit_Lib.jedit_views().foreach(init_title)
+ navigator.init(JEdit_Lib.jedit_buffers())
Syntax_Style.set_extender(Syntax_Style.Main_Extender)
init_mode_provider()
@@ -446,7 +461,7 @@
shutting_down.change(_ => false)
- val view = jEdit.getActiveView()
+ val view = jEdit.getActiveView
if (view != null) init_editor(view)
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Apr 04 16:38:16 2025 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Apr 04 22:20:30 2025 +0200
@@ -266,7 +266,7 @@
/* search */
- private val search_label: Component = new Label("Search:") {
+ private val search_label: Component = new Label(jEdit.getProperty("search.find")) {
tooltip = "Search and highlight output via regular expression"
}