| author | wenzelm | 
| Tue, 23 Jan 2024 19:56:52 +0100 | |
| changeset 79521 | db2b5c04075d | 
| parent 75410 | 832f764093e1 | 
| permissions | -rw-r--r-- | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 1 | /* Title: Pure/Tools/java_monitor.scala | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 2 | Author: Makarius | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 3 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 4 | Wrapper for the OpenJDK "jconsole" tool, with various adjustments. | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 5 | */ | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 6 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 7 | package isabelle | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 8 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 9 | |
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 10 | import java.lang.Class | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 11 | import java.awt.Component | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 12 | import javax.swing.UIManager | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 13 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 14 | |
| 75393 | 15 | object Java_Monitor {
 | 
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 16 | /* Java classes */ | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 17 | |
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 18 |   object ClassOf {
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 19 |     val Component: Class[_ <: AnyRef] = Class.forName("java.awt.Component")
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 20 |     val JConsole: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.JConsole")
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 21 |     val LocalVirtualMachine: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.LocalVirtualMachine")
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 22 |     val Messages: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.Messages")
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 23 |     val ProxyClient: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.ProxyClient")
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 24 |     val Resources: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.Resources")
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 25 |     val VMPanel: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.VMPanel")
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 26 | } | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 27 | |
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 28 | |
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 29 | /* default arguments */ | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 30 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 31 | def default_pid: Long = ProcessHandle.current().pid | 
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 32 | val default_update_interval: Time = Time.seconds(3) | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 33 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 34 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 35 | /* java monitor on this JVM: asynchronous GUI application with with system exit */ | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 36 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 37 | def java_monitor_internal( | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 38 | pid: Long = default_pid, | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 39 | look_and_feel: String = "", | 
| 75393 | 40 | update_interval: Time = default_update_interval | 
| 41 |   ): Unit = {
 | |
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 42 | val vm = | 
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 43 |       if (pid.toInt.toLong == pid) {
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 44 | Untyped.the_method(ClassOf.LocalVirtualMachine, "getLocalVirtualMachine") | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 45 | .invoke(null, pid.toInt) | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 46 | } | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 47 | else null | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 48 |     if (vm == null) error("Bad JVM process " + pid)
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 49 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 50 |     GUI_Thread.later {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 51 |       proper_string(look_and_feel) match {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 52 | case None => | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 53 | case Some(laf) => | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 54 | UIManager.setLookAndFeel(laf) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 55 |           System.setProperty("swing.defaultlaf", laf)
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 56 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 57 | |
| 72981 | 58 |       Desktop_App.about_handler {
 | 
| 59 | GUI.dialog(null, "Java Monitor", | |
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 60 | Untyped.the_method(ClassOf.Resources, "format"). | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 61 | invoke(null, | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 62 | Untyped.get_static(ClassOf.Messages, "JCONSOLE_VERSION"), | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 63 |                 System.getProperty("java.runtime.version")))
 | 
| 72981 | 64 | } | 
| 65 | ||
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 66 | val jconsole = | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 67 | Untyped.the_constructor(ClassOf.JConsole).newInstance(false).asInstanceOf[Component] | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 68 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 69 | val screen = GUI.mouse_location() | 
| 72977 | 70 | val width = (1200 max (screen.bounds.width / 2)) min screen.bounds.width | 
| 71 | val height = (900 max (screen.bounds.height / 2)) min screen.bounds.height | |
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 72 | Untyped.method(ClassOf.Component, "setBounds", classOf[Int], classOf[Int], classOf[Int], classOf[Int]) | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 73 | .invoke(jconsole, | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 74 | screen.bounds.x + (screen.bounds.width - width) / 2, | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 75 | screen.bounds.y + (screen.bounds.height - height) / 2, | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 76 | width, height) | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 77 | |
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 78 | Untyped.the_method(ClassOf.Component, "setVisible").invoke(jconsole, true) | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 79 | |
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 80 | Untyped.the_method(ClassOf.JConsole, "createMDI").invoke(jconsole) | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 81 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 82 |       Isabelle_Thread.fork(name = "JConsole.addVmid") {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 83 |         try {
 | 
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 84 | val proxy_client = | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 85 | Untyped.method(ClassOf.ProxyClient, "getProxyClient", ClassOf.LocalVirtualMachine) | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 86 | .invoke(null, vm) | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 87 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 88 |           GUI_Thread.later {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 89 |             try {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 90 | val vm_panel = | 
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 91 | Untyped.constructor(ClassOf.VMPanel, ClassOf.ProxyClient, Integer.TYPE) | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 92 | .newInstance(proxy_client, java.lang.Integer.valueOf(update_interval.ms.toInt)) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 93 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 94 | Untyped.field(vm_panel, "shouldUseSSL").setBoolean(vm_panel, false) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 95 | |
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 96 | Untyped.method(ClassOf.JConsole, "addFrame", ClassOf.VMPanel) | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 97 | .invoke(jconsole, vm_panel) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 98 | |
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 99 |               GUI_Thread.later {
 | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 100 | Untyped.the_method(ClassOf.JConsole, "tileWindows").invoke(jconsole) | 
| 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 101 | } | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 102 | |
| 75410 
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
 wenzelm parents: 
75393diff
changeset | 103 | Untyped.the_method(ClassOf.VMPanel, "connect").invoke(vm_panel) | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 104 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 105 |             catch {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 106 | case exn: Throwable => | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 107 | GUI.error_dialog(jconsole, "Error", GUI.scrollable_text(Exn.message(exn))) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 108 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 109 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 110 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 111 |         catch {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 112 | case exn: Throwable => | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 113 | GUI.error_dialog(jconsole, "Error", GUI.scrollable_text(Exn.message(exn))) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 114 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 115 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 116 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 117 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 118 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 119 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 120 | /* java monitor on new JVM: asynchronous process */ | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 121 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 122 | def java_monitor_external( | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 123 | parent: Component, | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 124 | pid: Long = default_pid, | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 125 | look_and_feel: String = "", | 
| 75393 | 126 | update_interval: Time = default_update_interval | 
| 127 |   ): Unit = {
 | |
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 128 |     Future.thread(name = "java_monitor", daemon = true) {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 129 |       try {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 130 | Isabelle_System.bash( | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 131 | "isabelle java_monitor " + | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 132 | " -P " + Bash.string(pid.toString) + | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 133 | " -L " + Bash.string(look_and_feel) + | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 134 | " -s " + Bash.string(update_interval.seconds.toString)).check | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 135 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 136 |       catch {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 137 | case exn: Throwable => | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 138 |           GUI_Thread.later {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 139 | GUI.error_dialog(parent, "System error", GUI.scrollable_text(Exn.message(exn))) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 140 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 141 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 142 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 143 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 144 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 145 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 146 | /* command line entry point */ | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 147 | |
| 75393 | 148 |   def main(args: Array[String]): Unit = {
 | 
| 72976 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 149 |     Command_Line.tool {
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 150 | var look_and_feel = "" | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 151 | var pid = 0L | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 152 | var update_interval = default_update_interval | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 153 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 154 |       val getopts = Getopts("""
 | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 155 | Usage: isabelle java_monitor [OPTIONS] | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 156 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 157 | Options are: | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 158 | -L CLASS class name of GUI look-and-feel | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 159 | -P PID Java process id (REQUIRED) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 160 | -s SECONDS update interval in seconds (default: """ + default_update_interval + """) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 161 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 162 | Monitor another Java process. | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 163 | """, | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 164 | "L:" -> (arg => look_and_feel = arg), | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 165 | "P:" -> (arg => pid = Value.Long.parse(arg)), | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 166 | "s:" -> (arg => update_interval = Time.seconds(Value.Double.parse(arg)))) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 167 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 168 | val more_args = getopts(args) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 169 | if (more_args.nonEmpty || pid == 0L) getopts.usage() | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 170 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 171 | java_monitor_internal(pid = pid, look_and_feel = look_and_feel, update_interval = update_interval) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 172 | |
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 173 | Thread.sleep(Long.MaxValue) | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 174 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 175 | } | 
| 
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
 wenzelm parents: diff
changeset | 176 | } |