--- a/Admin/components/components.sha1 Fri Nov 15 21:37:26 2024 +0100
+++ b/Admin/components/components.sha1 Fri Nov 15 21:43:22 2024 +0100
@@ -244,6 +244,7 @@
7fc9df033ec6b49dc1dad85eb240ab4f80653aa3 jedit-20231120.tar.gz
fbfd1d8a117a5bd844f230903d561cb88d3e5189 jedit-20240425.tar.gz
5117b7d0283adf31cf2bde17a9912eb775a0822f jedit-20241101.tar.gz
+a8b11ddf7f6838ea53868e46cb4555b7fa60e776 jedit-20241115.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Fri Nov 15 21:37:26 2024 +0100
+++ b/Admin/components/main Fri Nov 15 21:43:22 2024 +0100
@@ -14,7 +14,7 @@
isabelle_setup-20240327
javamail-20240109
jdk-21.0.5
-jedit-20241101
+jedit-20241115
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.17.2
--- a/NEWS Fri Nov 15 21:37:26 2024 +0100
+++ b/NEWS Fri Nov 15 21:43:22 2024 +0100
@@ -140,9 +140,7 @@
C-modifier.
* An active highlight area in the input buffer or output panel may be
-turned into a text selection by using the ALT modifier. Together with
-SHIFT modifier, an existing selection is augmented (otherwise it is
-reset).
+turned into a text selection by using the ALT modifier.
* The "Documentation" panel supports plain text files again, notably
"jedit-changes". This was broken in Isabelle2022, Isabelle2023,
--- a/src/Pure/Admin/component_jedit.scala Fri Nov 15 21:37:26 2024 +0100
+++ b/src/Pure/Admin/component_jedit.scala Fri Nov 15 21:43:22 2024 +0100
@@ -106,7 +106,6 @@
component_path: Path,
version: String,
original: Boolean = false,
- java_home: Path = default_java_home,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("ant", test = "-version")
@@ -172,8 +171,7 @@
progress.echo("Building jEdit ...")
Isabelle_System.copy_dir(source_dir, tmp_source_dir)
- progress.bash("env JAVA_HOME=" + File.bash_platform_path(java_home) + " ant",
- cwd = tmp_source_dir, echo = true).check
+ progress.bash("ant", cwd = tmp_source_dir, echo = true).check
Isabelle_System.copy_file(tmp_source_dir + Path.explode("build/jedit.jar"), jedit_patched_dir)
val java_sources =
@@ -506,14 +504,12 @@
/** Isabelle tool wrappers **/
val default_version = "5.7.0"
- def default_java_home: Path = Path.explode("$JAVA_HOME").expand
val isabelle_tool =
Isabelle_Tool("component_jedit", "build Isabelle component from the jEdit text-editor",
Scala_Project.here,
{ args =>
var target_dir = Path.current
- var java_home = default_java_home
var original = false
var version = default_version
@@ -522,14 +518,12 @@
Options are:
-D DIR target directory (default ".")
- -J JAVA_HOME Java version for building jedit.jar (e.g. version 11)
-O retain copy of original jEdit directory
-V VERSION jEdit version (default: """ + quote(default_version) + """)
Build auxiliary jEdit component from original sources, with some patches.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
- "J:" -> (arg => java_home = Path.explode(arg)),
"O" -> (_ => original = true),
"V:" -> (arg => version = arg))
@@ -539,7 +533,6 @@
val component_dir = target_dir + Path.basic("jedit-" + Date.Format.alt_date(Date.now()))
val progress = new Console_Progress()
- build_jedit(component_dir, version, original = original,
- java_home = java_home, progress = progress)
+ build_jedit(component_dir, version, original = original, progress = progress)
})
}
--- a/src/Pure/ROOT.ML Fri Nov 15 21:37:26 2024 +0100
+++ b/src/Pure/ROOT.ML Fri Nov 15 21:43:22 2024 +0100
@@ -373,3 +373,4 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
+
--- a/src/Pure/ROOT.scala Fri Nov 15 21:37:26 2024 +0100
+++ b/src/Pure/ROOT.scala Fri Nov 15 21:43:22 2024 +0100
@@ -29,4 +29,3 @@
def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
def if_proper(b: Boolean, body: => String): String = Library.if_proper(b, body)
}
-
--- a/src/Tools/jEdit/patches/accelerator_font Fri Nov 15 21:37:26 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
---- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-10-29 11:50:54.062016616 +0100
-@@ -1094,9 +1094,7 @@
- return new Font("Monospaced", Font.PLAIN, 12);
- }
- else {
-- Font font2 =
-- new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
-- Font.PLAIN, font1.getSize());
-+ Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
- FontRenderContext frc = new FontRenderContext(null, true, false);
- float scale =
- font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/menus_and_sidekick Fri Nov 15 21:43:22 2024 +0100
@@ -0,0 +1,56 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-10-29 11:50:54.062016616 +0100
+@@ -1094,9 +1094,7 @@
+ return new Font("Monospaced", Font.PLAIN, 12);
+ }
+ else {
+- Font font2 =
+- new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
+- Font.PLAIN, font1.getSize());
++ Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
+ FontRenderContext frc = new FontRenderContext(null, true, false);
+ float scale =
+ font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StatusBar.java 2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StatusBar.java 2024-11-15 20:22:26.451538237 +0100
+@@ -225,8 +225,11 @@
+ else
+ this.message.setText(" ");
+ }
+- else
+- this.message.setText(message);
++ else {
++ Exception exn = new Exception();
++ if (!exn.getStackTrace()[1].getClassName().startsWith("sidekick."))
++ this.message.setText(message);
++ }
+ } //}}}
+
+ //{{{ setMessageComponent() method
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-11-15 18:42:41.560326356 +0100
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-11-15 20:33:52.458587638 +0100
+@@ -1617,6 +1617,21 @@
+ }
+ //}}}
+
++ //{{{ isPopupTrigger() method
++ /**
++ * Returns if the specified event is the popup trigger event.
++ * This implements precisely defined behavior, as opposed to
++ * MouseEvent.isPopupTrigger().
++ * @param evt The event
++ * @since jEdit 3.2pre8
++ * @deprecated use {@link GenericGUIUtilities#requestFocus(Window, Component)}
++ */
++ @Deprecated
++ public static boolean isPopupTrigger(MouseEvent evt)
++ {
++ return GenericGUIUtilities.isPopupTrigger(evt);
++ } //}}}
++
+ //{{{ init() method
+ static void init()
+ {
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 15 21:37:26 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 15 21:43:22 2024 +0100
@@ -12,6 +12,7 @@
import java.io.{File => JFile}
import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit}
import java.awt.event.{InputEvent, KeyEvent, KeyListener}
+import java.awt.font.FontRenderContext
import javax.swing.{Icon, ImageIcon, JScrollBar, JWindow, SwingUtilities}
import scala.util.parsing.input.CharSequenceReader
@@ -22,7 +23,7 @@
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.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection, AntiAlias}
object JEdit_Lib {
@@ -294,13 +295,25 @@
}
- /* graphics range */
+ /* font */
+
+ def init_font_context(view: View, painter: TextAreaPainter): Unit = {
+ painter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
+ painter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
+ val old = painter.getFontRenderContext
+ Untyped.set[FontRenderContext](painter, "fontRenderContext",
+ new FontRenderContext(view.getGraphicsConfiguration.getDefaultTransform,
+ old.getAntiAliasingHint, old.getFractionalMetricsHint))
+ }
def font_metric(painter: TextAreaPainter): Font_Metric =
new Font_Metric(
font = painter.getFont,
context = painter.getFontRenderContext)
+
+ /* graphics range */
+
case class Gfx_Range(x: Int, y: Int, length: Int)
// NB: jEdit always normalizes \r\n and \r to \n
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 15 21:37:26 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 15 21:43:22 2024 +0100
@@ -21,7 +21,7 @@
import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler}
-import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
+import org.gjt.sp.jedit.textarea.JEditEmbeddedTextArea
import org.gjt.sp.jedit.syntax.SyntaxStyle
import org.gjt.sp.jedit.gui.KeyEventTranslator
import org.gjt.sp.util.{SyntaxUtilities, Log}
@@ -42,7 +42,14 @@
private var current_base_results = Command.Results.empty
private var current_rendering: JEdit_Rendering =
JEdit_Rendering(current_base_snapshot, Nil, Command.Results.empty)
- private var future_refresh: Option[Future[Unit]] = None
+
+ private val future_refresh = Synchronized[Option[Future[Unit]]](None)
+ private def fork_refresh(body: => Unit): Future[Unit] =
+ future_refresh.change_result({ old =>
+ old.foreach(_.cancel())
+ val future = Future.fork(body)
+ (future, Some(future))
+ })
private val rich_text_area =
new Rich_Text_Area(view, pretty_text_area, () => current_rendering, close_action,
@@ -56,10 +63,8 @@
def refresh(): Unit = {
GUI_Thread.require {}
- val font = current_font_info.font
- getPainter.setFont(font)
- getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
- getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
+ getPainter.setFont(current_font_info.font)
+ JEdit_Lib.init_font_context(view, getPainter)
getPainter.setStyles(
SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))
@@ -93,9 +98,8 @@
val snapshot = current_base_snapshot
val results = current_base_results
- future_refresh.foreach(_.cancel())
- future_refresh =
- Some(Future.fork {
+ lazy val current_refresh: Future[Unit] = fork_refresh(
+ {
val (rich_texts, rendering) =
try {
val rich_texts = Rich_Text.format(output, margin, metric, cache = PIDE.cache)
@@ -109,15 +113,7 @@
}
GUI_Thread.later {
- val current_metric = JEdit_Lib.font_metric(getPainter)
- val current_margin = Rich_Text.component_margin(current_metric, getPainter)
- if (true || // FIXME
- metric == current_metric &&
- margin == current_margin &&
- output == current_output &&
- snapshot == current_base_snapshot &&
- results == current_base_results
- ) {
+ if (future_refresh.value.contains(current_refresh)) {
current_rendering = rendering
val scroll_bottom = JEdit_Lib.scrollbar_bottom(pretty_text_area)
@@ -137,6 +133,7 @@
}
}
})
+ current_refresh
}
}
@@ -254,6 +251,7 @@
case KeyEvent.VK_ESCAPE =>
if (Isabelle.dismissed_popups(view)) evt.consume()
+ else if (getSelectionCount != 0) { selectNone(); evt.consume() }
case _ =>
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 15 21:37:26 2024 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 15 21:43:22 2024 +0100
@@ -285,7 +285,8 @@
if (JEdit_Lib.alt_modifier(evt)) {
highlight_area.info.map(_.range) match {
case Some(range) =>
- if (!JEdit_Lib.shift_modifier(evt)) text_area.selectNone()
+ text_area.requestFocus()
+ text_area.selectNone()
text_area.addToSelection(new Selection.Range(range.start, range.stop))
case None =>
}