# HG changeset patch # User wenzelm # Date 1731703402 -3600 # Node ID c8283b7f079183a2c46d6f82dfad0f27a5093ca0 # Parent cea55809bb9d46a6cb9ffb8e3800d3afc64d7958# Parent b29b72f64a6cbe6013156ddf6c5653fb8f8731b9 merged diff -r cea55809bb9d -r c8283b7f0791 Admin/components/components.sha1 --- 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 diff -r cea55809bb9d -r c8283b7f0791 Admin/components/main --- 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 diff -r cea55809bb9d -r c8283b7f0791 NEWS --- 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, diff -r cea55809bb9d -r c8283b7f0791 src/Pure/Admin/component_jedit.scala --- 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) }) } diff -r cea55809bb9d -r c8283b7f0791 src/Pure/ROOT.ML --- 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"; + diff -r cea55809bb9d -r c8283b7f0791 src/Pure/ROOT.scala --- 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) } - diff -r cea55809bb9d -r c8283b7f0791 src/Tools/jEdit/patches/accelerator_font --- 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(); diff -r cea55809bb9d -r c8283b7f0791 src/Tools/jEdit/patches/menus_and_sidekick --- /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() + { diff -r cea55809bb9d -r c8283b7f0791 src/Tools/jEdit/src/jedit_lib.scala --- 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 diff -r cea55809bb9d -r c8283b7f0791 src/Tools/jEdit/src/pretty_text_area.scala --- 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 _ => } diff -r cea55809bb9d -r c8283b7f0791 src/Tools/jEdit/src/rich_text_area.scala --- 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 => }