author | wenzelm |
Tue, 23 Nov 2021 12:29:09 +0100 | |
changeset 74832 | c299abcf7081 |
parent 73340 | 0ffcad1f6130 |
child 75393 | 87ebf5a50283 |
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 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
10 |
import java.awt.Component |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
11 |
import javax.swing.UIManager |
72981 | 12 |
import sun.tools.jconsole.{JConsole, LocalVirtualMachine, VMPanel, ProxyClient, |
13 |
Messages, Resources => JConsoleResources} |
|
72976
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
14 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
15 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
16 |
object Java_Monitor |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
17 |
{ |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
18 |
/* default arguments */ |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
19 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
20 |
def default_pid: Long = ProcessHandle.current().pid |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
21 |
val default_update_interval = Time.seconds(3) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
22 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
23 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
24 |
/* 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
|
25 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
26 |
def java_monitor_internal( |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
27 |
pid: Long = default_pid, |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
28 |
look_and_feel: String = "", |
73340 | 29 |
update_interval: Time = default_update_interval): Unit = |
72976
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 |
val vm = |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
32 |
if (pid.toInt.toLong == pid) LocalVirtualMachine.getLocalVirtualMachine(pid.toInt) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
33 |
else null |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
34 |
if (vm == null) error("Bad JVM process " + pid) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
35 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
36 |
GUI_Thread.later { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
37 |
proper_string(look_and_feel) match { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
38 |
case None => |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
39 |
case Some(laf) => |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
40 |
UIManager.setLookAndFeel(laf) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
41 |
System.setProperty("swing.defaultlaf", laf) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
42 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
43 |
|
72981 | 44 |
Desktop_App.about_handler { |
45 |
GUI.dialog(null, "Java Monitor", |
|
46 |
JConsoleResources.format( |
|
47 |
Messages.JCONSOLE_VERSION, System.getProperty("java.runtime.version")) |
|
48 |
) |
|
49 |
} |
|
50 |
||
72976
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
51 |
val jconsole = new JConsole(false) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
52 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
53 |
val screen = GUI.mouse_location() |
72977 | 54 |
val width = (1200 max (screen.bounds.width / 2)) min screen.bounds.width |
55 |
val height = (900 max (screen.bounds.height / 2)) min screen.bounds.height |
|
72976
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
56 |
jconsole.setBounds( |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
57 |
screen.bounds.x + (screen.bounds.width - width) / 2, |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
58 |
screen.bounds.y + (screen.bounds.height - height) / 2, |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
59 |
width, height) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
60 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
61 |
jconsole.setVisible(true) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
62 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
63 |
Untyped.method(classOf[JConsole], "createMDI").invoke(jconsole) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
64 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
65 |
Isabelle_Thread.fork(name = "JConsole.addVmid") { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
66 |
try { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
67 |
val proxy_client = ProxyClient.getProxyClient(vm) |
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 |
GUI_Thread.later { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
70 |
try { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
71 |
val vm_panel = |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
72 |
Untyped.constructor(classOf[VMPanel], classOf[ProxyClient], Integer.TYPE) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
73 |
.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
|
74 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
75 |
Untyped.field(vm_panel, "shouldUseSSL").setBoolean(vm_panel, false) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
76 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
77 |
Untyped.method(classOf[JConsole], "addFrame", classOf[VMPanel]) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
78 |
.invoke(jconsole, vm_panel) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
79 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
80 |
GUI_Thread.later { jconsole.tileWindows() } |
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 |
vm_panel.connect() |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
83 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
84 |
catch { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
85 |
case exn: Throwable => |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
86 |
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
|
87 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
88 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
89 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
90 |
catch { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
91 |
case exn: Throwable => |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
92 |
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
|
93 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
94 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
95 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
96 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
97 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
98 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
99 |
/* java monitor on new JVM: asynchronous process */ |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
100 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
101 |
def java_monitor_external( |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
102 |
parent: Component, |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
103 |
pid: Long = default_pid, |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
104 |
look_and_feel: String = "", |
73340 | 105 |
update_interval: Time = default_update_interval): Unit = |
72976
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
106 |
{ |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
107 |
Future.thread(name = "java_monitor", daemon = true) { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
108 |
try { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
109 |
Isabelle_System.bash( |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
110 |
"isabelle java_monitor " + |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
111 |
" -P " + Bash.string(pid.toString) + |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
112 |
" -L " + Bash.string(look_and_feel) + |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
113 |
" -s " + Bash.string(update_interval.seconds.toString)).check |
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 |
catch { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
116 |
case exn: Throwable => |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
117 |
GUI_Thread.later { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
118 |
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
|
119 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
120 |
} |
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 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
123 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
124 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
125 |
/* command line entry point */ |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
126 |
|
73340 | 127 |
def main(args: Array[String]): Unit = |
72976
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
128 |
{ |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
129 |
Command_Line.tool { |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
130 |
var look_and_feel = "" |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
131 |
var pid = 0L |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
132 |
var update_interval = default_update_interval |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
133 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
134 |
val getopts = Getopts(""" |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
135 |
Usage: isabelle java_monitor [OPTIONS] |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
136 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
137 |
Options are: |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
138 |
-L CLASS class name of GUI look-and-feel |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
139 |
-P PID Java process id (REQUIRED) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
140 |
-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
|
141 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
142 |
Monitor another Java process. |
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 |
"L:" -> (arg => look_and_feel = arg), |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
145 |
"P:" -> (arg => pid = Value.Long.parse(arg)), |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
146 |
"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
|
147 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
148 |
val more_args = getopts(args) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
149 |
if (more_args.nonEmpty || pid == 0L) getopts.usage() |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
150 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
151 |
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
|
152 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
153 |
Thread.sleep(Long.MaxValue) |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
154 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
155 |
} |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
156 |
} |