--- a/Admin/components/components.sha1 Fri Nov 01 14:10:52 2024 +0000
+++ b/Admin/components/components.sha1 Fri Nov 01 16:57:33 2024 +0100
@@ -242,6 +242,7 @@
f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz
7fc9df033ec6b49dc1dad85eb240ab4f80653aa3 jedit-20231120.tar.gz
fbfd1d8a117a5bd844f230903d561cb88d3e5189 jedit-20240425.tar.gz
+5117b7d0283adf31cf2bde17a9912eb775a0822f jedit-20241101.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
@@ -489,6 +490,7 @@
bee1c9416a086e553057171e5cb571271ed02c60 scala-3.2.1.tar.gz
989736bb2693fa2c484f45841364a0bcb642acc1 scala-3.3.0.tar.gz
347437eb000f93bc751cbe6eccd31e7e798e10e5 scala-3.3.3.tar.gz
+32b86128463b89e0a40943cc5dd426526f1065e7 scala-3.3.4.tar.gz
bdc7406747790b590518182d8b4131b4a0e90c07 scala-3.4.1.tar.gz
0983f776b3b9dd95164a747d176d65d0e45f843b scala-3.4.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
--- a/Admin/components/main Fri Nov 01 14:10:52 2024 +0000
+++ b/Admin/components/main Fri Nov 01 16:57:33 2024 +0100
@@ -14,7 +14,7 @@
isabelle_setup-20240327
javamail-20240109
jdk-21.0.3
-jedit-20240425
+jedit-20241101
jfreechart-1.5.3
jortho-1.0-2
jsoup-1.17.2
@@ -30,7 +30,7 @@
postgresql-42.7.3
prismjs-1.29.0
rsync-3.2.7-1
-scala-3.3.3
+scala-3.3.4
smbc-0.4.1
spass-3.8ds-2
sqlite-3.45.2.0
--- a/NEWS Fri Nov 01 14:10:52 2024 +0000
+++ b/NEWS Fri Nov 01 16:57:33 2024 +0100
@@ -120,6 +120,13 @@
unbundle no datatype_record_syntax
+*** Isabelle/jEdit Prover IDE ***
+
+* Action isabelle.select_structure (with keyboard shortcut C+7) extends
+the editor selection by adding the enclosing formal structure, based on
+formal markup by the prover.
+
+
*** Isabelle/VSCode Prover IDE ***
* General improvements: Persistent decorations for PIDE markup, correct
--- a/etc/options Fri Nov 01 14:10:52 2024 +0000
+++ b/etc/options Fri Nov 01 16:57:33 2024 +0100
@@ -309,6 +309,9 @@
public option editor_output_state : bool = false
-- "implicit output of proof state"
+public option editor_auto_hovering : bool = true
+ -- "automatic mouse hovering without keyboard modifier"
+
public option editor_document_session : string = ""
-- "session for interactive document preparation"
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Nov 01 16:57:33 2024 +0100
@@ -419,13 +419,13 @@
\<^item> @{notation_kind_def mixfix}: general mixfix notation, with delimiters
surrounding its arguments.
- \<^item> @{notation_kind_def prefix}: notation with delimiters before its
- arguments.
+ \<^item> @{notation_kind_def prefix}: notation with delimiter before its
+ argument.
- \<^item> @{notation_kind_def postfix}: notation with delimiters after its
- arguments.
+ \<^item> @{notation_kind_def postfix}: notation with delimiter after its
+ argument.
- \<^item> @{notation_kind_def "infix"}: notation with delimiters between its
+ \<^item> @{notation_kind_def "infix"}: notation with delimiter between its
arguments (automatically inserted for @{keyword "infix"} annotations,
see \secref{sec:infixes}).
--- a/src/Pure/Admin/component_jedit.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Pure/Admin/component_jedit.scala Fri Nov 01 16:57:33 2024 +0100
@@ -316,6 +316,8 @@
isabelle.reset-words.label=Reset non-permanent words
isabelle.select-entity.label=Select all occurences of formal entity at caret
isabelle.select-entity.shortcut=CS+ENTER
+isabelle.select-structure.label=Select structure around selection or caret
+isabelle.select-structure.shortcut=C+7
isabelle.set-continuous-checking.label=Set continuous checking
isabelle.set-node-required.label=Set node required
isabelle.toggle-breakpoint.label=Toggle Breakpoint
@@ -501,7 +503,7 @@
/** Isabelle tool wrappers **/
- val default_version = "5.6.0"
+ val default_version = "5.7.0"
def default_java_home: Path = Path.explode("$JAVA_HOME").expand
val isabelle_tool =
--- a/src/Pure/Admin/component_scala.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Pure/Admin/component_scala.scala Fri Nov 01 16:57:33 2024 +0100
@@ -34,20 +34,20 @@
}
val main_download: Download =
- Download("scala", "3.4.2", base_version = "",
+ Download("scala", "3.3.4", base_version = "",
url = "https://github.com/lampepfl/dotty/releases/download/{V}/scala3-{V}.tar.gz")
val lib_downloads: List[Download] = List(
Download("scala-parallel-collections", "1.0.4",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parallel-collections_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parallel-collections_{B}/{V}/scala-parallel-collections_{B}-{V}.jar"),
- Download("scala-parser-combinators", "2.3.0",
+ Download("scala-parser-combinators", "2.4.0",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parser-combinators_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_{B}/{V}/scala-parser-combinators_{B}-{V}.jar"),
Download("scala-swing", "3.0.0",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-swing_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-swing_{B}/{V}/scala-swing_{B}-{V}.jar"),
- Download("scala-xml", "2.2.0",
+ Download("scala-xml", "2.3.0",
"https://mvnrepository.com/artifact/org.scala-lang.modules/scala-xml_{B}/{V}",
physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_{B}/{V}/scala-xml_{B}-{V}.jar")
)
--- a/src/Pure/General/pretty.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Pure/General/pretty.scala Fri Nov 01 16:57:33 2024 +0100
@@ -21,13 +21,9 @@
val bullet: XML.Body = XML.elem(Markup.BULLET, space) :: space
def block(body: XML.Body,
- open_block: Boolean = false,
consistent: Boolean = false,
indent: Int = 2
- ): XML.Tree = {
- val markup = Markup.Block(open_block = open_block, consistent = consistent, indent = indent)
- XML.Elem(markup, body)
- }
+ ): XML.Tree = XML.Elem(Markup.Block(consistent = consistent, indent = indent), body)
def brk(width: Int, indent: Int = 0): XML.Tree =
XML.Elem(Markup.Break(width = width, indent = indent), spaces(width))
@@ -169,10 +165,10 @@
List(make_block(make_tree(body2), markup = markup, markup_body = Some(body1)))
case XML.Elem(markup, body) =>
markup match {
- case Markup.Block(open_block, consistent, indent) =>
+ case Markup.Block(consistent, indent) =>
List(
make_block(make_tree(body),
- open_block = open_block, consistent = consistent, indent = indent))
+ consistent = consistent, indent = indent, open_block = false))
case Markup.Break(width, indent) =>
List(Break(false, force_nat(width), force_nat(indent)))
case Markup(Markup.ITEM, _) =>
--- a/src/Pure/PIDE/markup.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Pure/PIDE/markup.scala Fri Nov 01 16:57:33 2024 +0100
@@ -259,24 +259,21 @@
/* pretty printing */
- val Open_Block = new Properties.Boolean("open_block")
val Consistent = new Properties.Boolean("consistent")
val Indent = new Properties.Int("indent")
val Width = new Properties.Int("width")
object Block {
val name = "block"
- def apply(open_block: Boolean = false, consistent: Boolean = false, indent: Int = 0): Markup =
+ def apply(consistent: Boolean = false, indent: Int = 0): Markup =
Markup(name,
- (if (open_block) Open_Block(open_block) else Nil) :::
(if (consistent) Consistent(consistent) else Nil) :::
(if (indent != 0) Indent(indent) else Nil))
- def unapply(markup: Markup): Option[(Boolean, Boolean, Int)] =
+ def unapply(markup: Markup): Option[(Boolean, Int)] =
if (markup.name == name) {
- val open_block = Open_Block.get(markup.properties)
val consistent = Consistent.get(markup.properties)
val indent = Indent.get(markup.properties)
- Some((open_block, consistent, indent))
+ Some((consistent, indent))
}
else None
}
--- a/src/Pure/PIDE/rendering.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Pure/PIDE/rendering.scala Fri Nov 01 16:57:33 2024 +0100
@@ -222,6 +222,11 @@
val text_color_elements = Markup.Elements(text_color.keySet)
+ val structure_elements =
+ Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,
+ Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
+ Markup.COMMAND_SPAN)
+
val tooltip_elements =
Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION, Markup.TIMING,
Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
@@ -572,6 +577,26 @@
}
+ /* markup structure */
+
+ def markup_structure(
+ elements: Markup.Elements,
+ ranges: List[Text.Range],
+ filter: Text.Markup => Boolean = _ => true
+ ): List[Text.Markup] = {
+ def cumulate(range: Text.Range): List[Text.Info[Option[Text.Markup]]] =
+ snapshot.cumulate[Option[Text.Markup]](range, None, elements, _ =>
+ {
+ case (old, markup) =>
+ Some(if (old.isEmpty || filter(markup)) Some(markup) else old)
+ })
+
+ Library.distinct(
+ for (range <- ranges; case Text.Info(_, Some(m)) <- cumulate(range))
+ yield m)
+ }
+
+
/* tooltips */
def timing_threshold: Double = 0.0
--- a/src/Pure/ROOT.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Pure/ROOT.scala Fri Nov 01 16:57:33 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/jedit_main/actions.xml Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/jedit_main/actions.xml Fri Nov 01 16:57:33 2024 +0100
@@ -82,6 +82,11 @@
isabelle.jedit.Isabelle.select_entity(textArea);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.select-structure">
+ <CODE>
+ isabelle.jedit.Isabelle.select_structure(textArea);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.complete">
<CODE>
isabelle.jedit.Isabelle.complete(view, false);
--- a/src/Tools/jEdit/patches/accelerator_font Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/accelerator_font Fri Nov 01 16:57:33 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2020-09-03 05:31:04.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2021-05-10 11:02:05.784257753 +0200
-@@ -1130,9 +1130,7 @@
+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 {
--- a/src/Tools/jEdit/patches/docking Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/docking Fri Nov 01 16:57:33 2024 +0100
@@ -1,6 +1,6 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2021-05-10 11:02:05.760257760 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-10-29 11:50:54.062016616 +0100
@@ -45,14 +45,15 @@
* @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
* @since jEdit 4.0pre1
--- a/src/Tools/jEdit/patches/extended_styles_brackets Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/extended_styles_brackets Fri Nov 01 16:57:33 2024 +0100
@@ -1,6 +1,6 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-04-25 12:56:22.208257322 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-10-29 11:50:54.066016546 +0100
@@ -332,9 +332,9 @@
//{{{ Package private members
@@ -36,10 +36,10 @@
protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)
{
return size() > capacity;
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2023-11-20 15:31:55.825519645 +0100
-@@ -914,6 +914,11 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-10-29 11:50:54.066016546 +0100
+@@ -919,6 +919,11 @@
return chunkCache.getLineInfo(screenLine).physicalLine;
} //}}}
@@ -51,7 +51,7 @@
//{{{ getScreenLineOfOffset() method
/**
* Returns the screen (wrapped) line containing the specified offset.
-@@ -1622,8 +1627,8 @@
+@@ -1627,8 +1632,8 @@
}
// Scan backwards, trying to find a bracket
@@ -62,18 +62,9 @@
int count = 1;
char openBracket = '\0';
char closeBracket = '\0';
-@@ -6336,7 +6341,7 @@
- {
- int following = charBreaker.following(offset -
- index0Offset);
-- if (following == BreakIterator.DONE)
-+ if (following == BreakIterator.DONE || (Runtime.version().feature() >= 20 && following == offset - index0Offset))
- {
- // This means a end of line. Then it is
- // safe to assume 1 code unit is a character.
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2020-09-03 05:31:03.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2021-05-10 18:20:57.418571547 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-08-03 19:53:20.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-10-29 11:50:54.066016546 +0100
@@ -115,6 +115,8 @@
case '⦄': if (direction != null) direction[0] = false; return '⦃';
case '⟪': if (direction != null) direction[0] = true; return '⟫';
@@ -83,10 +74,10 @@
default: return '\0';
}
} //}}}
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2021-05-10 11:02:05.820257742 +0200
-@@ -344,8 +344,28 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-10-29 11:50:54.066016546 +0100
+@@ -357,8 +357,28 @@
}
}
--- a/src/Tools/jEdit/patches/folding Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/folding Fri Nov 01 16:57:33 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-09-03 05:31:04.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2021-05-10 11:02:05.776257756 +0200
-@@ -1968,29 +1968,23 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2024-10-29 11:50:54.062016616 +0100
+@@ -2054,29 +2054,23 @@
{
Segment seg = new Segment();
newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
--- a/src/Tools/jEdit/patches/laf_fonts Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/laf_fonts Fri Nov 01 16:57:33 2024 +0100
@@ -1,5 +1,6 @@
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2020-09-03 05:31:04.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2021-02-01 18:00:07.541681144 +0100
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2024-10-29 11:50:54.062016616 +0100
@@ -414,7 +414,9 @@
// adjust swing properties for button, menu, and label, and list and
@@ -11,3 +12,4 @@
// This is handled a little differently from other jEdit settings
// as this flag needs to be known very early in the
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java
--- a/src/Tools/jEdit/patches/panel_font Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/panel_font Fri Nov 01 16:57:33 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-09-03 05:31:02.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2021-05-10 11:23:04.107511056 +0200
-@@ -52,6 +52,7 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2024-08-03 19:53:16.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2024-10-29 11:50:54.062016616 +0100
+@@ -53,6 +53,7 @@
import javax.swing.JComponent;
import javax.swing.JPanel;
import javax.swing.JPopupMenu;
@@ -9,7 +9,7 @@
import javax.swing.JToggleButton;
import javax.swing.UIManager;
import javax.swing.border.Border;
-@@ -163,6 +164,7 @@
+@@ -164,6 +165,7 @@
{
button = new JToggleButton();
button.setMargin(new Insets(1,1,1,1));
@@ -17,7 +17,7 @@
}
GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
button.setRequestFocusEnabled(false);
-@@ -690,8 +692,6 @@
+@@ -683,8 +685,6 @@
renderHints = new RenderingHints(
RenderingHints.KEY_ANTIALIASING,
RenderingHints.VALUE_ANTIALIAS_ON);
--- a/src/Tools/jEdit/patches/props Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/props Fri Nov 01 16:57:33 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props
---- jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props 2020-09-03 05:31:10.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props 2021-05-10 11:02:05.788257753 +0200
-@@ -1277,8 +1277,7 @@
+diff -ru jedit5.7.0/jEdit/org/jedit/localization/jedit_en.props jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props
+--- jedit5.7.0/jEdit/org/jedit/localization/jedit_en.props 2024-08-03 19:53:22.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props 2024-10-29 11:50:54.066016546 +0100
+@@ -1282,8 +1282,7 @@
The most likely reason is that the JAR file is corrupt; try\n\
reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
for a full stack trace.
@@ -11,4 +11,3 @@
plugin-error.already-loaded=Two copies installed. Please remove one of the \
two copies.
plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}.
-Binary files jedit5.6.0/jedit.jar and jedit5.6.0-patched/jedit.jar differ
--- a/src/Tools/jEdit/patches/putenv Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/putenv Fri Nov 01 16:57:33 2024 +0100
@@ -1,6 +1,6 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2021-05-10 11:23:04.139510558 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2024-10-29 11:50:54.062016616 +0100
@@ -131,6 +131,21 @@
static final Pattern winPattern = Pattern.compile(winPatternString);
@@ -27,21 +27,21 @@
if (m.find())
{
String varName = m.group(2);
-- String expansion = System.getenv(varName);
+- String expansion = jEdit.systemManager.getenv(varName);
+ String expansion = getenv(varName);
if (expansion != null)
- return m.replaceFirst(expansion);
- }
-@@ -179,7 +194,7 @@
+ {
+ expansion = Matcher.quoteReplacement(expansion);
+@@ -182,7 +197,7 @@
return arg;
}
String varName = m.group(2);
-- String expansion = System.getenv(varName);
+- String expansion = jEdit.systemManager.getenv(varName);
+ String expansion = getenv(varName);
if (expansion == null) {
if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
expansion = jEdit.getSettingsDirectory();
-@@ -189,7 +204,7 @@
+@@ -192,7 +207,7 @@
varName = varName.toUpperCase();
String uparg = arg.toUpperCase();
m = p.matcher(uparg);
@@ -50,7 +50,7 @@
}
}
if (expansion != null) {
-@@ -1682,13 +1697,11 @@
+@@ -1674,13 +1689,11 @@
//{{{ VarCompressor constructor
VarCompressor()
{
@@ -65,3 +65,63 @@
{
String k = entry.getKey();
if (k.equalsIgnoreCase("pwd") || k.equalsIgnoreCase("oldpwd")) continue;
+diff -ru jedit5.7.0/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java jedit5.7.0-patched/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java
+--- jedit5.7.0/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java 2024-08-03 19:53:29.000000000 +0200
++++ jedit5.7.0-patched/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java 2024-10-29 12:21:05.284840022 +0100
+@@ -167,56 +167,6 @@
+ }
+
+ @Test
+- public void expandVariablesEnvWindowsAsWindows() throws Exception
+- {
+- jEdit.systemManager = Mockito.mock(SystemManager.class);
+- var captor = ArgumentCaptor.forClass(String.class);
+- var value = "c:\\home\\jEdit";
+- Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
+- updateOS(WINDOWS_NT);
+- var key = "jEdit_TEST";
+- assertEquals(value, MiscUtilities.expandVariables('%' + key + '%'));
+- assertEquals(captor.getValue(), key);
+- }
+- @Test
+- public void expandVariablesEnvWindowsAsUnix() throws Exception
+- {
+- jEdit.systemManager = Mockito.mock(SystemManager.class);
+- var captor = ArgumentCaptor.forClass(String.class);
+- var value = "c:\\home\\jEdit";
+- Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
+- updateOS(UNIX);
+- var key = "jEdit_TEST";
+- assertEquals(value, MiscUtilities.expandVariables('%' + key + '%'));
+- assertEquals(captor.getValue(), key);
+- }
+-
+- @Test
+- public void expandVariablesEnvUnix() throws Exception
+- {
+- jEdit.systemManager = Mockito.mock(SystemManager.class);
+- var captor = ArgumentCaptor.forClass(String.class);
+- var value = "c:\\home\\jEdit";
+- Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
+- updateOS(UNIX);
+- var key = "jEdit_TEST";
+- assertEquals(value, MiscUtilities.expandVariables('$' + key));
+- assertEquals(captor.getValue(), key);
+- }
+-
+- @Test
+- public void expandVariablesEnvUnix2() throws Exception
+- {
+- jEdit.systemManager = Mockito.mock(SystemManager.class);
+- var captor = ArgumentCaptor.forClass(String.class);
+- var value = "c:\\home\\jEdit";
+- Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
+- updateOS(UNIX);
+- var key = "jEdit_TEST";
+- assertEquals(value, MiscUtilities.expandVariables("${" + key + '}'));
+- }
+-
+- @Test
+ public void expandVariablesEnvUnixNoMatch() throws Exception
+ {
+ updateOS(UNIX);
--- a/src/Tools/jEdit/patches/title Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/title Fri Nov 01 16:57:33 2024 +0100
@@ -1,7 +1,6 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/View.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/View.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/View.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/View.java 2021-05-10 11:02:05.792257750 +0200
-@@ -1262,15 +1262,10 @@
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java 2024-10-29 11:50:54.066016546 +0100
+@@ -1264,15 +1264,10 @@
StringBuilder title = new StringBuilder();
--- a/src/Tools/jEdit/patches/vfs_manager Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/vfs_manager Fri Nov 01 16:57:33 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2020-09-03 05:31:03.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2021-05-10 11:02:05.808257746 +0200
-@@ -380,6 +380,18 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2024-10-29 11:50:54.062016616 +0100
+@@ -339,6 +339,18 @@
if(vfsUpdates.size() == 1)
{
--- a/src/Tools/jEdit/patches/vfs_marker Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/patches/vfs_marker Fri Nov 01 16:57:33 2024 +0100
@@ -1,7 +1,7 @@
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-03 05:31:04.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2021-05-10 11:02:05.824257741 +0200
-@@ -1194,6 +1194,7 @@
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-08-03 19:53:15.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-10-29 11:50:54.058016686 +0100
+@@ -1195,6 +1195,7 @@
VFSFile[] selectedFiles = browserView.getSelectedFiles();
Buffer buffer = null;
@@ -9,7 +9,7 @@
check_selected:
for (VFSFile file : selectedFiles)
-@@ -1243,7 +1244,10 @@
+@@ -1244,7 +1245,10 @@
}
if (_buffer != null)
@@ -20,7 +20,7 @@
}
// otherwise if a file is selected in OPEN_DIALOG or
// SAVE_DIALOG mode, just let the listener(s)
-@@ -1252,21 +1256,30 @@
+@@ -1253,21 +1257,30 @@
if(buffer != null)
{
@@ -53,9 +53,9 @@
}
Object[] listeners = listenerList.getListenerList();
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2020-09-03 05:31:03.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2021-05-10 11:02:05.824257741 +0200
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-08-03 19:53:14.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-10-29 11:50:54.062016616 +0100
@@ -302,6 +302,12 @@
}
} //}}}
@@ -69,10 +69,10 @@
//{{{ getPath() method
public String getPath()
{
-diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
---- jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java 2020-09-03 05:31:01.000000000 +0200
-+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2021-05-10 11:02:05.824257741 +0200
-@@ -4242,7 +4242,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 2024-10-29 11:50:54.062016616 +0100
+@@ -4233,7 +4233,7 @@
} //}}}
//{{{ gotoMarker() method
--- a/src/Tools/jEdit/src/isabelle.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Nov 01 16:57:33 2024 +0100
@@ -360,7 +360,7 @@
}
- /* formal entities */
+ /* formal entities and structure */
def goto_entity(view: View): Unit = {
val text_area = view.getTextArea
@@ -384,6 +384,17 @@
}
}
+ def select_structure(text_area: JEditTextArea): Unit = {
+ for (rendering <- Document_View.get_rendering(text_area)) {
+ val sel_ranges = JEdit_Lib.selection_ranges(text_area)
+ val caret_range = JEdit_Lib.caret_range(text_area)
+ val ranges = if (sel_ranges.isEmpty) List(caret_range) else sel_ranges
+ for (info <- rendering.markup_structure(Rendering.structure_elements, ranges)) {
+ text_area.addToSelection(new Selection.Range(info.range.start, info.range.stop))
+ }
+ }
+ }
+
/* completion */
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 01 16:57:33 2024 +0100
@@ -21,7 +21,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}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter, Selection}
object JEdit_Lib {
@@ -179,6 +179,21 @@
def caret_range(text_area: TextArea): Text.Range =
point_range(text_area.getBuffer, text_area.getCaretPosition)
+ def selection_ranges(text_area: TextArea): List[Text.Range] = {
+ val buffer = text_area.getBuffer
+ text_area.getSelection.toList.flatMap(
+ {
+ case rect: Selection.Rect =>
+ List.from(
+ for {
+ l <- (rect.getStartLine to rect.getEndLine).iterator
+ r = Text.Range(rect.getStart(buffer, l), rect.getEnd(buffer, l))
+ if !r.is_singularity
+ } yield r)
+ case sel: Selection => List(Text.Range(sel.getStart, sel.getEnd))
+ })
+ }
+
def visible_range(text_area: TextArea): Option[Text.Range] = {
val buffer = text_area.getBuffer
val n = text_area.getVisibleLines
--- a/src/Tools/jEdit/src/jedit_options.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/src/jedit_options.scala Fri Nov 01 16:57:33 2024 +0100
@@ -73,6 +73,11 @@
}
}
+ object auto_hovering extends Bool_Access("editor_auto_hovering") {
+ class GUI extends Bool_GUI(this, "Auto hovering") {
+ tooltip = "Automatic mouse hovering without keyboard modifier"
+ }
+ }
/* editor pane for plugin options */
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Nov 01 16:57:33 2024 +0100
@@ -63,6 +63,8 @@
private val output_state_button = new JEdit_Options.output_state.GUI
+ private val auto_hovering_button = new JEdit_Options.auto_hovering.GUI
+
private val auto_update_button = new GUI.Check("Auto update", init = do_update) {
tooltip = "Indicate automatic update following cursor movement"
override def clicked(state: Boolean): Unit = {
@@ -80,7 +82,7 @@
private val controls =
Wrap_Panel(
- List(output_state_button, auto_update_button,
+ List(output_state_button, auto_hovering_button, auto_update_button,
update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
@@ -94,6 +96,7 @@
GUI_Thread.later {
handle_resize()
output_state_button.load()
+ auto_hovering_button.load()
handle_update(do_update, None)
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 01 14:10:52 2024 +0000
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Nov 01 16:57:33 2024 +0100
@@ -147,8 +147,8 @@
private class Active_Area[A](
render: JEdit_Rendering => Text.Range => Option[Text.Info[A]],
- val require_control: Boolean = false,
- val ignore_control: Boolean = false,
+ require_control: => Boolean = false,
+ ignore_control: => Boolean = false,
cursor: Int = -1
) {
private var the_text_info: Option[(String, Text.Info[A])] = None
@@ -192,7 +192,8 @@
// owned by GUI thread
private val highlight_area =
- new Active_Area[Color](_.highlight, ignore_control = true)
+ new Active_Area[Color](_.highlight, require_control = true,
+ ignore_control = JEdit_Options.auto_hovering())
private val hyperlink_area =
new Active_Area[PIDE.editor.Hyperlink](