# HG changeset patch # User wenzelm # Date 1608587273 -3600 # Node ID 51442c6dc29633308cbfadb160f476db63bbbb21 # Parent 315f9b4f9e7a55df12a52e42a246b4d49a7510be more robust Java monitor: avoid odd warning about insecure connection; diff -r 315f9b4f9e7a -r 51442c6dc296 lib/Tools/java_monitor --- /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 "$@" diff -r 315f9b4f9e7a -r 51442c6dc296 src/Doc/JEdit/JEdit.thy --- 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>\Monitor\ panel, as explained below. There is a similar widget for the - Java VM: a double-click opens the external \<^verbatim>\jconsole\ 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>\jconsole\). \<^medskip> The \<^emph>\Monitor\ panel visualizes various data collections about recent diff -r 315f9b4f9e7a -r 51442c6dc296 src/Pure/System/isabelle_system.scala --- 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 } diff -r 315f9b4f9e7a -r 51442c6dc296 src/Pure/Tools/java_monitor.scala --- /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) + } + } +} diff -r 315f9b4f9e7a -r 51442c6dc296 src/Pure/build-jars --- 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 diff -r 315f9b4f9e7a -r 51442c6dc296 src/Tools/jEdit/src/Isabelle.props --- 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 \ diff -r 315f9b4f9e7a -r 51442c6dc296 src/Tools/jEdit/src/actions.xml --- 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); - + - isabelle.jedit.Isabelle.jconsole(view); + isabelle.jedit.Isabelle.java_monitor(view); diff -r 315f9b4f9e7a -r 51442c6dc296 src/Tools/jEdit/src/isabelle.scala --- 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()) } diff -r 315f9b4f9e7a -r 51442c6dc296 src/Tools/jEdit/src/jEdit.props --- 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 diff -r 315f9b4f9e7a -r 51442c6dc296 src/Tools/jEdit/src/status_widget.scala --- 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