# HG changeset patch # User wenzelm # Date 1743798030 -7200 # Node ID 8f6dc8483b1a78e679549dbe798b1faa419887b5 # Parent 13a185b64ffff8bd49fe8e811244008ae7f978b9# Parent 8b5dd705dfef4981380edfde154a79f0916b7e4e merged diff -r 13a185b64fff -r 8f6dc8483b1a Admin/components/components.sha1 --- 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 diff -r 13a185b64fff -r 8f6dc8483b1a Admin/components/main --- 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 diff -r 13a185b64fff -r 8f6dc8483b1a NEWS --- 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 *** diff -r 13a185b64fff -r 8f6dc8483b1a etc/build.props --- 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 \ diff -r 13a185b64fff -r 8f6dc8483b1a src/Doc/JEdit/JEdit.thy --- 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>\Console\ with its \<^emph>\Scala\ sub-plugin (\secref{sec:scala-console}) and \<^emph>\SideKick\ with some Isabelle-specific - parsers for document tree structure (\secref{sec:sidekick}). The - \<^emph>\Navigator\ plugin is particularly important for hyperlinks within the - formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins - (e.g.\ \<^emph>\ErrorList\, \<^emph>\Code2HTML\) 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>\Console\, \<^emph>\ErrorList\, \<^emph>\SideKick\) are included to saturate the + dependencies of bundled plugins, but have no particular use in + Isabelle/jEdit. \ @@ -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>\CONTROL\ or \<^verbatim>\COMMAND\ modifier key is still - pressed). Such jumps to other text locations are recorded by the - \<^emph>\Navigator\ 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>\Incremental Search Bar\ (action @{action_ref + "quick-search"}). The following keyboard shortcuts are available: + + \<^medskip> + \begin{tabular}[t]{l} + @{action_ref "navigate-backwards"} (\<^verbatim>\AS+LEFT\) \\ + @{action_ref "navigate-forwards"} (\<^verbatim>\AS+RIGHT\) \\ + \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 diff -r 13a185b64fff -r 8f6dc8483b1a src/Pure/Admin/component_jedit.scala --- 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 diff -r 13a185b64fff -r 8f6dc8483b1a src/Pure/General/linear_set.scala --- 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] = diff -r 13a185b64fff -r 8f6dc8483b1a src/Pure/PIDE/text.scala --- 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] = diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/jedit_main/actions.xml --- 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 @@ + + + isabelle.jedit.Isabelle.navigate_backwards(view); + + + + + isabelle.jedit.Isabelle.navigate_forwards(view); + + isabelle.jedit.Isabelle.open_browser_info(view); diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/patches/search_bar --- /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); + diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/patches/vfs_marker diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/src/document_model.scala --- 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, diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/src/font_info.scala --- 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) } } diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/src/isabelle.scala --- 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") } diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/src/isabelle_navigator.scala --- /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) + } + } +} diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/src/jedit_editor.scala --- 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( diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/src/jedit_lib.scala --- 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() diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/src/main_plugin.scala --- 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) } diff -r 13a185b64fff -r 8f6dc8483b1a src/Tools/jEdit/src/pretty_text_area.scala --- 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" }