--- a/Admin/components/components.sha1 Fri Sep 11 14:14:58 2020 +0100
+++ b/Admin/components/components.sha1 Fri Sep 11 14:15:14 2020 +0100
@@ -171,6 +171,7 @@
1e53598a02ec8d8736b15f480cbe2c84767a7827 jedit_build-20190508.tar.gz
b9c6f49d3f6ebe2e85a50595ce7412d01a4314ac jedit_build-20190717.tar.gz
1c753beb93e92e95e99e8ead23a68346bd1af44a jedit_build-20200610.tar.gz
+533b1ee6459f59bcbe4f09e214ad2cb990fb6952 jedit_build-20200908.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
--- a/Admin/components/main Fri Sep 11 14:14:58 2020 +0100
+++ b/Admin/components/main Fri Sep 11 14:15:14 2020 +0100
@@ -6,7 +6,7 @@
e-2.0-3
isabelle_fonts-20190717
jdk-11.0.5+10
-jedit_build-20200610
+jedit_build-20200908
jfreechart-1.5.0
jortho-1.0-2
kodkodi-1.5.6
--- a/NEWS Fri Sep 11 14:14:58 2020 +0100
+++ b/NEWS Fri Sep 11 14:15:14 2020 +0100
@@ -16,16 +16,15 @@
*** Isabelle/jEdit Prover IDE ***
-* The jEdit status line includes a widget for Isabelle/ML heap usage,
-including an indication for ongoing garbage collection (as "ML
-cleanup").
+* The jEdit status line includes widgets both for JVM and ML heap usage.
+Ongoing ML ongoing garbage collection is shown as "ML cleanup".
* The Monitor dockable provides buttons to request a full garbage
collection and sharing of live data on the ML heap. It also includes
information about the Java Runtime system.
-* Update to jedit-5.6pre1, the latest pre-release. This version works
-properly on macOS by default, without the special MacOSX plugin.
+* Update to jedit-5.6.0, the latest release. This version works properly
+on macOS by default, without the special MacOSX plugin.
*** Document preparation ***
--- a/src/Doc/JEdit/JEdit.thy Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy Fri Sep 11 14:15:14 2020 +0100
@@ -2103,10 +2103,13 @@
Isabelle~/ General\<close>.
\<^medskip>
- The jEdit status line includes monitor widgets for current heap usage of
- Java and Isabelle/ML, respectively. The one for ML includes information
- about ongoing garbage collection (as ``ML cleanup''); a double-click opens
- a new instance of the \<^emph>\<open>Monitor\<close> panel for further details.
+ The jEdit status line includes a monitor widget for the current heap usage
+ of the Isabelle/ML process; this includes information about ongoing garbage
+ collection (shown as ``ML cleanup''). A double-click opens a new instance of
+ the \<^emph>\<open>Monitor\<close> panel, as explained below. There is a similar widget for the
+ Java VM: a double-click opens the external \<^verbatim>\<open>jconsole\<close> application, with
+ detailed information and controls for the Java process underlying
+ Isabelle/Scala/jEdit.
\<^medskip>
The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent
@@ -2249,10 +2252,6 @@
\<^bold>\<open>Workaround:\<close> Increase JVM heap parameters by editing platform-specific
files (for ``properties'' or ``options'') that are associated with the main
app bundle.
-
- Also note that jEdit provides a heap space monitor in the status line
- (bottom-right). Double-clicking on that causes full garbage-collection,
- which sometimes helps in low-memory situations.
\<close>
end
--- a/src/Doc/System/Environment.thy Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Doc/System/Environment.thy Fri Sep 11 14:15:14 2020 +0100
@@ -308,13 +308,16 @@
stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close>
array.
- \<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close>
- within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred
- entry-point for high-end tools implemented in Isabelle/Scala --- compiled
- once when the Isabelle distribution is built. These tools are provided by
- Isabelle/Pure and cannot be augmented in user-space.
+ \<^enum> An internal tool that is registered in \<^verbatim>\<open>etc/settings\<close> via the shell
+ function \<^bash_function>\<open>isabelle_scala_service\<close>, referring to a
+ suitable instance of class \<^scala_type>\<open>isabelle.Isabelle_Scala_Tools\<close>.
+ This is the preferred approach for non-trivial systems programming in
+ Isabelle/Scala: instead of adhoc interpretation of \<^verbatim>\<open>scala\<close> scripts,
+ which is somewhat slow and only type-checked at runtime, there are
+ properly compiled \<^verbatim>\<open>jar\<close> modules (see also the shell function
+ \<^bash_function>\<open>classpath\<close> in \secref{sec:scala}).
- There are also some administrative tools that are available from a bare
+ There are also various administrative tools that are available from a bare
repository clone of Isabelle, but not in regular distributions.
\<close>
--- a/src/Doc/System/Scala.thy Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Doc/System/Scala.thy Fri Sep 11 14:15:14 2020 +0100
@@ -4,7 +4,7 @@
imports Base
begin
-chapter \<open>Isabelle/Scala systems programming\<close>
+chapter \<open>Isabelle/Scala systems programming \label{sec:scala}\<close>
text \<open>
Isabelle/ML and Isabelle/Scala are the two main implementation languages of
--- a/src/Pure/ML/ml_statistics.scala Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Pure/ML/ml_statistics.scala Fri Sep 11 14:15:14 2020 +0100
@@ -99,7 +99,7 @@
private def consume(props: Properties.T): Unit = synchronized
{
if (session != null) {
- val props1 = (session.xml_cache.props(props ::: Platform.jvm_statistics()))
+ val props1 = (session.xml_cache.props(props ::: Java_Statistics.jvm_statistics()))
session.runtime_statistics.post(Session.Runtime_Statistics(props1))
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/java_statistics.scala Fri Sep 11 14:15:14 2020 +0100
@@ -0,0 +1,45 @@
+/* Title: Pure/System/java_statistics.scala
+ Author: Makarius
+
+Java runtime statistics.
+*/
+
+package isabelle
+
+
+object Java_Statistics
+{
+ /* memory status */
+
+ sealed case class Memory_Status(heap_size: Long, heap_free: Long)
+ {
+ def heap_used: Long = (heap_size - heap_free) max 0
+ def heap_used_fraction: Double =
+ if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size
+ }
+
+ def memory_status(): Memory_Status =
+ {
+ val heap_size = Runtime.getRuntime.totalMemory()
+ val heap_used = heap_size - Runtime.getRuntime.freeMemory()
+ Memory_Status(heap_size, heap_used)
+ }
+
+
+ /* JVM statistics */
+
+ def jvm_statistics(): Properties.T =
+ {
+ val status = memory_status()
+ val threads = Thread.activeCount()
+ val workers = Isabelle_Thread.pool.getPoolSize
+ val workers_active = Isabelle_Thread.pool.getActiveCount
+
+ List(
+ "java_heap_size" -> status.heap_size.toString,
+ "java_heap_used" -> status.heap_used.toString,
+ "java_threads_total" -> threads.toString,
+ "java_workers_total" -> workers.toString,
+ "java_workers_active" -> workers_active.toString)
+ }
+}
--- a/src/Pure/System/platform.scala Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Pure/System/platform.scala Fri Sep 11 14:15:14 2020 +0100
@@ -68,24 +68,4 @@
/* JVM name */
val jvm_name: String = System.getProperty("java.vm.name", "")
-
-
- /* JVM statistics */
-
- def jvm_statistics(): Properties.T =
- {
- val heap_size = Runtime.getRuntime.totalMemory()
- val heap_used = heap_size - Runtime.getRuntime.freeMemory()
-
- val threads = Thread.activeCount()
- val workers = Isabelle_Thread.pool.getPoolSize
- val workers_active = Isabelle_Thread.pool.getActiveCount
-
- List(
- "java_heap_size" -> heap_size.toString,
- "java_heap_used" -> heap_used.toString,
- "java_threads_total" -> threads.toString,
- "java_workers_total" -> workers.toString,
- "java_workers_active" -> workers_active.toString)
- }
}
--- a/src/Pure/build-jars Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Pure/build-jars Fri Sep 11 14:15:14 2020 +0100
@@ -126,6 +126,7 @@
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/isabelle_tool.scala
+ src/Pure/System/java_statistics.scala
src/Pure/System/linux.scala
src/Pure/System/numa.scala
src/Pure/System/options.scala
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Sep 11 14:15:14 2020 +0100
@@ -49,7 +49,6 @@
"src/Tools/jEdit/src/jedit_sessions.scala"
"src/Tools/jEdit/src/jedit_spell_checker.scala"
"src/Tools/jEdit/src/keymap_merge.scala"
- "src/Tools/jEdit/src/ml_status.scala"
"src/Tools/jEdit/src/monitor_dockable.scala"
"src/Tools/jEdit/src/output_dockable.scala"
"src/Tools/jEdit/src/plugin.scala"
@@ -66,6 +65,7 @@
"src/Tools/jEdit/src/simplifier_trace_window.scala"
"src/Tools/jEdit/src/sledgehammer_dockable.scala"
"src/Tools/jEdit/src/state_dockable.scala"
+ "src/Tools/jEdit/src/status_widget.scala"
"src/Tools/jEdit/src/symbols_dockable.scala"
"src/Tools/jEdit/src/syntax_style.scala"
"src/Tools/jEdit/src/syslog_dockable.scala"
@@ -390,7 +390,7 @@
target_shasum > "$TARGET_SHASUM"
- cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6pre1manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf"
+ cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6.0manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf"
cp "$TARGET_DIR/doc/CHANGES.txt" "$TARGET_DIR/doc/jedit-changes"
cat > "$TARGET_DIR/doc/Contents" <<EOF
Original jEdit Documentation
--- a/src/Tools/jEdit/patches/accelerator_font Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/accelerator_font Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 2020-05-20 11:10:13.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2020-06-10 15:30:42.744707440 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2020-09-08 20:13:23.561140312 +0200
@@ -1130,9 +1130,7 @@
return new Font("Monospaced", Font.PLAIN, 12);
}
--- a/src/Tools/jEdit/patches/docking Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/docking Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-05-20 11:10:10.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-06-10 15:33:52.388038983 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-09-08 20:13:23.565140195 +0200
@@ -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 Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/extended_styles Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 2020-06-09 17:01:03.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2020-06-10 15:38:59.771992636 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-08 20:13:23.565140195 +0200
@@ -332,9 +332,9 @@
//{{{ Package private members
@@ -13,7 +13,8 @@
//}}}
//{{{ Chunk constructor
-@@ -585,7 +585,7 @@
+@@ -584,8 +584,8 @@
+ // this is either style.getBackgroundColor() or
// styles[defaultID].getBackgroundColor()
private Color background;
- private char[] chars;
@@ -23,9 +24,9 @@
private GlyphData glyphData;
//}}}
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 2020-05-20 11:10:10.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2020-06-10 15:38:03.605353644 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-08 20:13:23.569140077 +0200
@@ -914,6 +914,11 @@
return chunkCache.getLineInfo(screenLine).physicalLine;
} //}}}
@@ -38,9 +39,9 @@
//{{{ getScreenLineOfOffset() method
/**
* Returns the screen (wrapped) line containing the specified offset.
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2020-05-20 11:10:13.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2020-06-10 16:10:50.165837982 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2020-09-08 20:13:23.569140077 +0200
@@ -344,8 +344,28 @@
}
}
--- a/src/Tools/jEdit/patches/folding Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/folding Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-05-20 11:10:12.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-06-10 16:03:10.547355787 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-09-08 20:13:23.573139959 +0200
@@ -1968,29 +1968,23 @@
{
Segment seg = new Segment();
--- a/src/Tools/jEdit/patches/props Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/props Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/jedit/localization/jedit_en.props 5.6pre1/jEdit-patched/org/jedit/localization/jedit_en.props
---- 5.6pre1/jEdit-orig/org/jedit/localization/jedit_en.props 2019-12-22 22:03:35.000000000 +0100
-+++ 5.6pre1/jEdit-patched/org/jedit/localization/jedit_en.props 2020-06-10 15:36:37.051536302 +0200
+diff -ru 5.6.0/jEdit-orig/org/jedit/localization/jedit_en.props 5.6.0/jEdit-patched/org/jedit/localization/jedit_en.props
+--- 5.6.0/jEdit-orig/org/jedit/localization/jedit_en.props 2020-09-03 05:31:10.000000000 +0200
++++ 5.6.0/jEdit-patched/org/jedit/localization/jedit_en.props 2020-09-08 20:13:35.644786809 +0200
@@ -1277,8 +1277,7 @@
The most likely reason is that the JAR file is corrupt; try\n\
reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
--- a/src/Tools/jEdit/patches/putenv Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/putenv Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 2020-06-09 22:58:00.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2020-06-10 15:36:56.603033473 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2020-09-08 20:13:35.648786692 +0200
@@ -131,6 +131,21 @@
static final Pattern winPattern = Pattern.compile(winPatternString);
--- a/src/Tools/jEdit/patches/title Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/title Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/View.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/View.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/View.java 2020-06-10 14:07:09.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/View.java 2020-06-10 15:37:09.546703839 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/View.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/View.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/View.java 2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/View.java 2020-09-08 20:13:35.652786577 +0200
@@ -1262,15 +1262,10 @@
StringBuilder title = new StringBuilder();
--- a/src/Tools/jEdit/patches/vfs_manager Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/vfs_manager Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 2020-05-20 11:10:11.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java 2020-06-10 15:37:21.842393040 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 2020-09-03 05:31:03.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java 2020-09-08 20:13:35.656786460 +0200
@@ -380,6 +380,18 @@
if(vfsUpdates.size() == 1)
--- a/src/Tools/jEdit/patches/vfs_marker Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/patches/vfs_marker Fri Sep 11 14:15:14 2020 +0100
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-05-20 11:10:12.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-06-10 15:37:37.310005209 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-08 20:13:45.348505646 +0200
@@ -1194,6 +1194,7 @@
VFSFile[] selectedFiles = browserView.getSelectedFiles();
@@ -53,9 +53,9 @@
}
Object[] listeners = listenerList.getListenerList();
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 2020-05-20 11:10:11.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2020-06-10 15:37:37.314005109 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 2020-09-03 05:31:03.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2020-09-08 20:13:45.348505646 +0200
@@ -302,6 +302,12 @@
}
} //}}}
@@ -69,9 +69,9 @@
//{{{ getPath() method
public String getPath()
{
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/jEdit.java 2020-05-26 16:55:37.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2020-06-10 15:37:37.314005109 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2020-09-08 20:13:45.348505646 +0200
@@ -4242,7 +4242,7 @@
} //}}}
--- a/src/Tools/jEdit/src/jEdit.props Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Fri Sep 11 14:15:14 2020 +0100
@@ -337,7 +337,8 @@
view.height=850
view.middleMousePaste=true
view.showToolbar=true
-view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor memory-status ml-status errors clock
+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
view.width=1200
xml-insert-closing-tag.shortcut=
--- a/src/Tools/jEdit/src/ml_status.scala Fri Sep 11 14:14:58 2020 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,144 +0,0 @@
-/* Title: Tools/jEdit/src/ml_status.scala
- Author: Makarius
-
-ML status bar: heap and garbage collection.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.{Color, Dimension, Graphics, Graphics2D, Insets, RenderingHints}
-import java.awt.font.FontRenderContext
-import java.awt.event.{MouseAdapter, MouseEvent}
-import javax.swing.{JComponent, JLabel}
-
-import org.gjt.sp.jedit.{View, jEdit}
-import org.gjt.sp.jedit.gui.statusbar.{StatusWidgetFactory, Widget}
-
-
-object ML_Status
-{
- private val template = "99999/99999MB"
-
- private class GUI(view: View) extends JComponent
- {
- /* component state -- owned by GUI thread */
-
- private var status = ML_Statistics.memory_status(Nil)
-
-
- /* init */
-
- setFont(new JLabel().getFont)
- setToolTipText("ML heap memory (double-click for monitor panel)")
-
- private val font_render_context = new FontRenderContext(null, true, false)
- private val line_metrics = getFont.getLineMetrics(template, font_render_context)
-
- {
- val bounds = getFont.getStringBounds(template, font_render_context)
- val dim = new Dimension(bounds.getWidth.toInt, bounds.getHeight.toInt)
- setPreferredSize(dim)
- setMaximumSize(dim)
- }
-
- setForeground(jEdit.getColorProperty("view.status.foreground"))
- setBackground(jEdit.getColorProperty("view.status.background"))
-
- def progress_foreground: Color = jEdit.getColorProperty("view.status.memory.foreground")
- def progress_background: Color = jEdit.getColorProperty("view.status.memory.background")
-
-
- /* paint */
-
- private def update(new_status: ML_Statistics.Memory_Status)
- {
- if (status != new_status) {
- status = new_status
- repaint()
- }
- }
-
- override def paintComponent(gfx: Graphics)
- {
- super.paintComponent(gfx)
-
- val insets = new Insets(0, 0, 0, 0)
-
- val width = getWidth - insets.left - insets.right
- val height = getHeight - insets.top - insets.bottom - 1
-
- val (text, fraction) =
- status.gc_progress match {
- case Some(p) => ("ML cleanup", 1.0 - p)
- case None =>
- ((status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
- status.heap_used_fraction)
- }
-
- val width2 = (width * fraction).toInt
-
- val text_bounds = gfx.getFont.getStringBounds(text, font_render_context)
- val text_x = insets.left + ((width - text_bounds.getWidth).toInt / 2)
- val text_y = (insets.top + line_metrics.getAscent).toInt
-
- gfx.asInstanceOf[Graphics2D].
- setRenderingHint(
- RenderingHints.KEY_TEXT_ANTIALIASING,
- RenderingHints.VALUE_TEXT_ANTIALIAS_ON)
-
- gfx.setColor(progress_background)
- gfx.fillRect(insets.left, insets.top, width2, height)
-
- gfx.setColor(progress_foreground)
- gfx.setClip(insets.left, insets.top, width2, height)
- gfx.drawString(text, text_x, text_y)
-
- gfx.setColor(getForeground)
- gfx.setClip(insets.left + width2, insets.top, getWidth - insets.left - width2, height)
- gfx.drawString(text, text_x, text_y)
- }
-
-
- /* main */
-
- private val main =
- Session.Consumer[Session.Runtime_Statistics](getClass.getName) {
- case stats =>
- val status = ML_Statistics.memory_status(stats.props)
- GUI_Thread.later { update(status) }
- }
-
- override def addNotify()
- {
- super.addNotify()
- PIDE.session.runtime_statistics += main
- }
-
- override def removeNotify()
- {
- super.removeNotify()
- PIDE.session.runtime_statistics -= main
- }
-
-
- /* mouse listener */
-
- addMouseListener(new MouseAdapter {
- override def mouseClicked(evt: MouseEvent)
- {
- if (evt.getClickCount == 2) {
- view.getInputHandler.invokeAction("isabelle-monitor-float")
- }
- }
- })
- }
-
- class Widget_Factory extends StatusWidgetFactory
- {
- override def getWidget(view: View): Widget =
- new Widget { override def getComponent: JComponent = new GUI(view) }
- }
-}
--- a/src/Tools/jEdit/src/services.xml Fri Sep 11 14:14:58 2020 +0100
+++ b/src/Tools/jEdit/src/services.xml Fri Sep 11 14:15:14 2020 +0100
@@ -50,7 +50,10 @@
<SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="graphview">
new isabelle.jedit.Graphview_Dockable$Handler()
</SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="java-status">
+ new isabelle.jedit.Status_Widget$Java_Factory();
+ </SERVICE>
<SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="ml-status">
- new isabelle.jedit.ML_Status$Widget_Factory();
+ new isabelle.jedit.Status_Widget$ML_Factory();
</SERVICE>
</SERVICES>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/status_widget.scala Fri Sep 11 14:15:14 2020 +0100
@@ -0,0 +1,222 @@
+/* Title: Tools/jEdit/src/status_widget.scala
+ Author: Makarius
+
+ML status bar: heap and garbage collection.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+import java.awt.{Color, Dimension, Graphics, Graphics2D, Insets, RenderingHints}
+import java.awt.font.FontRenderContext
+import java.awt.event.{ActionEvent, ActionListener, MouseAdapter, MouseEvent}
+
+import javax.swing.{JComponent, JLabel, Timer}
+import org.gjt.sp.jedit.{View, jEdit}
+import org.gjt.sp.jedit.gui.statusbar.{StatusWidgetFactory, Widget}
+
+
+object Status_Widget
+{
+ /** generic GUI **/
+
+ private val template = "ABC: 99999/99999MB"
+
+ abstract class GUI(view: View) extends JComponent
+ {
+ /* init */
+
+ setFont(new JLabel().getFont)
+
+ private val font_render_context = new FontRenderContext(null, true, false)
+ private val line_metrics = getFont.getLineMetrics(template, font_render_context)
+
+ {
+ val bounds = getFont.getStringBounds(template, font_render_context)
+ val dim = new Dimension(bounds.getWidth.toInt, bounds.getHeight.toInt)
+ setPreferredSize(dim)
+ setMaximumSize(dim)
+ }
+
+ setForeground(jEdit.getColorProperty("view.status.foreground"))
+ setBackground(jEdit.getColorProperty("view.status.background"))
+
+ def progress_foreground: Color = jEdit.getColorProperty("view.status.memory.foreground")
+ def progress_background: Color = jEdit.getColorProperty("view.status.memory.background")
+
+
+ /* paint */
+
+ def get_status: (String, Double)
+
+ override def paintComponent(gfx: Graphics)
+ {
+ super.paintComponent(gfx)
+
+ val insets = new Insets(0, 0, 0, 0)
+
+ val width = getWidth - insets.left - insets.right
+ val height = getHeight - insets.top - insets.bottom - 1
+
+ val (text, fraction) = get_status
+ val width2 = (width * fraction).toInt
+
+ val text_bounds = gfx.getFont.getStringBounds(text, font_render_context)
+ val text_x = insets.left + ((width - text_bounds.getWidth).toInt / 2)
+ val text_y = (insets.top + line_metrics.getAscent).toInt
+
+ gfx.asInstanceOf[Graphics2D].
+ setRenderingHint(
+ RenderingHints.KEY_TEXT_ANTIALIASING,
+ RenderingHints.VALUE_TEXT_ANTIALIAS_ON)
+
+ gfx.setColor(progress_background)
+ gfx.fillRect(insets.left, insets.top, width2, height)
+
+ gfx.setColor(progress_foreground)
+ gfx.setClip(insets.left, insets.top, width2, height)
+ gfx.drawString(text, text_x, text_y)
+
+ gfx.setColor(getForeground)
+ gfx.setClip(insets.left + width2, insets.top, getWidth - insets.left - width2, height)
+ gfx.drawString(text, text_x, text_y)
+ }
+
+
+ /* mouse listener */
+
+ def action: String
+
+ addMouseListener(new MouseAdapter {
+ override def mouseClicked(evt: MouseEvent)
+ {
+ if (evt.getClickCount == 2) {
+ view.getInputHandler.invokeAction(action)
+ }
+ }
+ })
+ }
+
+
+
+ /** Java **/
+
+ class Java_GUI(view: View) extends GUI(view)
+ {
+ /* component state -- owned by GUI thread */
+
+ private var status = Java_Statistics.memory_status()
+
+ def get_status: (String, Double) =
+ {
+ ("JVM: " + (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
+ status.heap_used_fraction)
+ }
+
+ private def update_status(new_status: Java_Statistics.Memory_Status)
+ {
+ if (status != new_status) {
+ status = new_status
+ repaint()
+ }
+ }
+
+
+ /* timer */
+
+ private val timer =
+ new Timer(500, new ActionListener {
+ override def actionPerformed(e: ActionEvent) {
+ update_status(Java_Statistics.memory_status())
+ }
+ })
+
+ override def addNotify()
+ {
+ super.addNotify()
+ timer.start()
+ }
+
+ override def removeNotify()
+ {
+ super.removeNotify()
+ timer.stop()
+ }
+
+
+ /* action */
+
+ setToolTipText("Java heap memory (double-click for monitor application)")
+
+ override def action: String = "isabelle.jconsole"
+ }
+
+ class Java_Factory extends StatusWidgetFactory
+ {
+ override def getWidget(view: View): Widget =
+ new Widget { override def getComponent: JComponent = new Java_GUI(view) }
+ }
+
+
+
+ /** ML **/
+
+ class ML_GUI(view: View) extends GUI(view)
+ {
+ /* component state -- owned by GUI thread */
+
+ private var status = ML_Statistics.memory_status(Nil)
+
+ def get_status: (String, Double) =
+ status.gc_progress match {
+ case Some(p) => ("ML cleanup", 1.0 - p)
+ case None =>
+ ("ML: " + (status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
+ status.heap_used_fraction)
+ }
+
+ private def update_status(new_status: ML_Statistics.Memory_Status)
+ {
+ if (status != new_status) {
+ status = new_status
+ repaint()
+ }
+ }
+
+
+ /* main */
+
+ private val main =
+ Session.Consumer[Session.Runtime_Statistics](getClass.getName) {
+ case stats =>
+ val status = ML_Statistics.memory_status(stats.props)
+ GUI_Thread.later { update_status(status) }
+ }
+
+ override def addNotify()
+ {
+ super.addNotify()
+ PIDE.session.runtime_statistics += main
+ }
+
+ override def removeNotify()
+ {
+ super.removeNotify()
+ PIDE.session.runtime_statistics -= main
+ }
+
+
+ /* action */
+
+ setToolTipText("ML heap memory (double-click for monitor panel)")
+
+ override def action: String = "isabelle-monitor-float"
+ }
+
+ class ML_Factory extends StatusWidgetFactory
+ {
+ override def getWidget(view: View): Widget =
+ new Widget { override def getComponent: JComponent = new ML_GUI(view) }
+ }
+}