author | paulson <lp15@cam.ac.uk> |
Wed, 24 Apr 2024 20:56:26 +0100 | |
changeset 80149 | 40a3fc07a587 |
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:
75393
diff
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:
75393
diff
changeset
|
16 |
/* Java classes */ |
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
wenzelm
parents:
75393
diff
changeset
|
17 |
|
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
wenzelm
parents:
75393
diff
changeset
|
18 |
object ClassOf { |
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
wenzelm
parents:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
changeset
|
26 |
} |
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
wenzelm
parents:
75393
diff
changeset
|
27 |
|
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
wenzelm
parents:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
changeset
|
61 |
invoke(null, |
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
wenzelm
parents:
75393
diff
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:
75393
diff
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:
75393
diff
changeset
|
66 |
val jconsole = |
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
wenzelm
parents:
75393
diff
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:
75393
diff
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:
75393
diff
changeset
|
73 |
.invoke(jconsole, |
832f764093e1
avoid static access to sun.tools.jconsole: more robust compilation (notably with scala3), but less robust invocation;
wenzelm
parents:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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:
75393
diff
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 |
} |