--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/java_monitor Mon Dec 21 22:47:53 2020 +0100
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: monitor another Java process
+
+isabelle_admin_build jars || exit $?
+
+isabelle java isabelle.Java_Monitor "$@"
--- a/src/Doc/JEdit/JEdit.thy Mon Dec 21 22:03:39 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy Mon Dec 21 22:47:53 2020 +0100
@@ -2110,9 +2110,9 @@
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.
+ JVM: a double-click opens an external Java monitor process with detailed
+ information and controls for the Java process underlying
+ Isabelle/Scala/jEdit (this is based on \<^verbatim>\<open>jconsole\<close>).
\<^medskip>
The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent
--- a/src/Pure/System/isabelle_system.scala Mon Dec 21 22:03:39 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala Mon Dec 21 22:47:53 2020 +0100
@@ -356,9 +356,6 @@
watchdog = watchdog, strict = strict)
}
- def jconsole(): Process_Result =
- bash("isabelle_jdk jconsole " + java.lang.ProcessHandle.current().pid).check
-
private lazy val gnutar_check: Boolean =
try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
catch { case ERROR(_) => false }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/java_monitor.scala Mon Dec 21 22:47:53 2020 +0100
@@ -0,0 +1,148 @@
+/* Title: Pure/Tools/java_monitor.scala
+ Author: Makarius
+
+Wrapper for the OpenJDK "jconsole" tool, with various adjustments.
+*/
+
+package isabelle
+
+
+import java.awt.Component
+import javax.swing.UIManager
+import sun.tools.jconsole.{JConsole, LocalVirtualMachine, VMPanel, ProxyClient}
+
+
+object Java_Monitor
+{
+ /* default arguments */
+
+ def default_pid: Long = ProcessHandle.current().pid
+ val default_update_interval = Time.seconds(3)
+
+
+ /* java monitor on this JVM: asynchronous GUI application with with system exit */
+
+ def java_monitor_internal(
+ pid: Long = default_pid,
+ look_and_feel: String = "",
+ update_interval: Time = default_update_interval)
+ {
+ val vm =
+ if (pid.toInt.toLong == pid) LocalVirtualMachine.getLocalVirtualMachine(pid.toInt)
+ else null
+ if (vm == null) error("Bad JVM process " + pid)
+
+ GUI_Thread.later {
+ proper_string(look_and_feel) match {
+ case None =>
+ case Some(laf) =>
+ UIManager.setLookAndFeel(laf)
+ System.setProperty("swing.defaultlaf", laf)
+ }
+
+ val jconsole = new JConsole(false)
+
+ val screen = GUI.mouse_location()
+ val width = 1200 min screen.bounds.width
+ val height = 900 min screen.bounds.height
+ jconsole.setBounds(
+ screen.bounds.x + (screen.bounds.width - width) / 2,
+ screen.bounds.y + (screen.bounds.height - height) / 2,
+ width, height)
+
+ jconsole.setVisible(true)
+
+ Untyped.method(classOf[JConsole], "createMDI").invoke(jconsole)
+
+ Isabelle_Thread.fork(name = "JConsole.addVmid") {
+ try {
+ val proxy_client = ProxyClient.getProxyClient(vm)
+
+ GUI_Thread.later {
+ try {
+ val vm_panel =
+ Untyped.constructor(classOf[VMPanel], classOf[ProxyClient], Integer.TYPE)
+ .newInstance(proxy_client, java.lang.Integer.valueOf(update_interval.ms.toInt))
+
+ Untyped.field(vm_panel, "shouldUseSSL").setBoolean(vm_panel, false)
+
+ Untyped.method(classOf[JConsole], "addFrame", classOf[VMPanel])
+ .invoke(jconsole, vm_panel)
+
+ GUI_Thread.later { jconsole.tileWindows() }
+
+ vm_panel.connect()
+ }
+ catch {
+ case exn: Throwable =>
+ GUI.error_dialog(jconsole, "Error", GUI.scrollable_text(Exn.message(exn)))
+ }
+ }
+ }
+ catch {
+ case exn: Throwable =>
+ GUI.error_dialog(jconsole, "Error", GUI.scrollable_text(Exn.message(exn)))
+ }
+ }
+ }
+ }
+
+
+ /* java monitor on new JVM: asynchronous process */
+
+ def java_monitor_external(
+ parent: Component,
+ pid: Long = default_pid,
+ look_and_feel: String = "",
+ update_interval: Time = default_update_interval)
+ {
+ Future.thread(name = "java_monitor", daemon = true) {
+ try {
+ Isabelle_System.bash(
+ "isabelle java_monitor " +
+ " -P " + Bash.string(pid.toString) +
+ " -L " + Bash.string(look_and_feel) +
+ " -s " + Bash.string(update_interval.seconds.toString)).check
+ }
+ catch {
+ case exn: Throwable =>
+ GUI_Thread.later {
+ GUI.error_dialog(parent, "System error", GUI.scrollable_text(Exn.message(exn)))
+ }
+ }
+ }
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool {
+ var look_and_feel = ""
+ var pid = 0L
+ var update_interval = default_update_interval
+
+ val getopts = Getopts("""
+Usage: isabelle java_monitor [OPTIONS]
+
+ Options are:
+ -L CLASS class name of GUI look-and-feel
+ -P PID Java process id (REQUIRED)
+ -s SECONDS update interval in seconds (default: """ + default_update_interval + """)
+
+ Monitor another Java process.
+""",
+ "L:" -> (arg => look_and_feel = arg),
+ "P:" -> (arg => pid = Value.Long.parse(arg)),
+ "s:" -> (arg => update_interval = Time.seconds(Value.Double.parse(arg))))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty || pid == 0L) getopts.usage()
+
+ java_monitor_internal(pid = pid, look_and_feel = look_and_feel, update_interval = update_interval)
+
+ Thread.sleep(Long.MaxValue)
+ }
+ }
+}
--- a/src/Pure/build-jars Mon Dec 21 22:03:39 2020 +0100
+++ b/src/Pure/build-jars Mon Dec 21 22:47:53 2020 +0100
@@ -168,6 +168,7 @@
src/Pure/Tools/doc.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/fontforge.scala
+ src/Pure/Tools/java_monitor.scala
src/Pure/Tools/main.scala
src/Pure/Tools/mkroot.scala
src/Pure/Tools/phabricator.scala
--- a/src/Tools/jEdit/src/Isabelle.props Mon Dec 21 22:03:39 2020 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props Mon Dec 21 22:47:53 2020 +0100
@@ -34,7 +34,7 @@
isabelle-session-browser \
isabelle.preview \
isabelle.draft \
- isabelle.jconsole \
+ isabelle.java-monitor \
- \
isabelle-debugger \
isabelle-documentation \
--- a/src/Tools/jEdit/src/actions.xml Mon Dec 21 22:03:39 2020 +0100
+++ b/src/Tools/jEdit/src/actions.xml Mon Dec 21 22:47:53 2020 +0100
@@ -217,9 +217,9 @@
isabelle.jedit.Keymap_Merge.check_dialog(view);
</CODE>
</ACTION>
- <ACTION NAME="isabelle.jconsole">
+ <ACTION NAME="isabelle.java-monitor">
<CODE>
- isabelle.jedit.Isabelle.jconsole(view);
+ isabelle.jedit.Isabelle.java_monitor(view);
</CODE>
</ACTION>
</ACTIONS>
--- a/src/Tools/jEdit/src/isabelle.scala Mon Dec 21 22:03:39 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Dec 21 22:47:53 2020 +0100
@@ -588,17 +588,8 @@
}
- /* jconsole */
+ /* java monitor */
- def jconsole(view: View) {
- Future.thread(name = "jconsole", daemon = true) {
- try { Isabelle_System.jconsole() }
- catch {
- case exn: Throwable =>
- GUI_Thread.later {
- GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
- }
- }
- }
- }
+ def java_monitor(view: View): Unit =
+ Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf())
}
--- a/src/Tools/jEdit/src/jEdit.props Mon Dec 21 22:03:39 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Mon Dec 21 22:47:53 2020 +0100
@@ -234,7 +234,7 @@
isabelle.increase-font-size.shortcut=C+PLUS
isabelle.increase-font-size2.label=Increase font size (clone)
isabelle.increase-font-size2.shortcut=C+EQUALS
-isabelle.jconsole.label=Java/VM monitor
+isabelle.java-monitor.label=Java/VM monitor
isabelle.last-error.label=Go to last error
isabelle.last-error.shortcut=CS+z
isabelle.message.label=Show message
--- a/src/Tools/jEdit/src/status_widget.scala Mon Dec 21 22:03:39 2020 +0100
+++ b/src/Tools/jEdit/src/status_widget.scala Mon Dec 21 22:47:53 2020 +0100
@@ -149,7 +149,7 @@
setToolTipText("Java heap memory (double-click for monitor application)")
- override def action: String = "isabelle.jconsole"
+ override def action: String = "isabelle.java-monitor"
}
class Java_Factory extends StatusWidgetFactory