src/Pure/Tools/java_monitor.scala
changeset 75410 832f764093e1
parent 75393 87ebf5a50283
equal deleted inserted replaced
75409:5640c4db7d37 75410:832f764093e1
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
       
    10 import java.lang.Class
    10 import java.awt.Component
    11 import java.awt.Component
    11 import javax.swing.UIManager
    12 import javax.swing.UIManager
    12 import sun.tools.jconsole.{JConsole, LocalVirtualMachine, VMPanel, ProxyClient,
       
    13   Messages, Resources => JConsoleResources}
       
    14 
    13 
    15 
    14 
    16 object Java_Monitor {
    15 object Java_Monitor {
       
    16   /* Java classes */
       
    17 
       
    18   object ClassOf {
       
    19     val Component: Class[_ <: AnyRef] = Class.forName("java.awt.Component")
       
    20     val JConsole: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.JConsole")
       
    21     val LocalVirtualMachine: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.LocalVirtualMachine")
       
    22     val Messages: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.Messages")
       
    23     val ProxyClient: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.ProxyClient")
       
    24     val Resources: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.Resources")
       
    25     val VMPanel: Class[_ <: AnyRef] = Class.forName("sun.tools.jconsole.VMPanel")
       
    26   }
       
    27 
       
    28 
    17   /* default arguments */
    29   /* default arguments */
    18 
    30 
    19   def default_pid: Long = ProcessHandle.current().pid
    31   def default_pid: Long = ProcessHandle.current().pid
    20   val default_update_interval = Time.seconds(3)
    32   val default_update_interval: Time = Time.seconds(3)
    21 
    33 
    22 
    34 
    23   /* java monitor on this JVM: asynchronous GUI application with with system exit */
    35   /* java monitor on this JVM: asynchronous GUI application with with system exit */
    24 
    36 
    25   def java_monitor_internal(
    37   def java_monitor_internal(
    26     pid: Long = default_pid,
    38     pid: Long = default_pid,
    27     look_and_feel: String = "",
    39     look_and_feel: String = "",
    28     update_interval: Time = default_update_interval
    40     update_interval: Time = default_update_interval
    29   ): Unit = {
    41   ): Unit = {
    30     val vm =
    42     val vm =
    31       if (pid.toInt.toLong == pid) LocalVirtualMachine.getLocalVirtualMachine(pid.toInt)
    43       if (pid.toInt.toLong == pid) {
       
    44         Untyped.the_method(ClassOf.LocalVirtualMachine, "getLocalVirtualMachine")
       
    45           .invoke(null, pid.toInt)
       
    46       }
    32       else null
    47       else null
    33     if (vm == null) error("Bad JVM process " + pid)
    48     if (vm == null) error("Bad JVM process " + pid)
    34 
    49 
    35     GUI_Thread.later {
    50     GUI_Thread.later {
    36       proper_string(look_and_feel) match {
    51       proper_string(look_and_feel) match {
    40           System.setProperty("swing.defaultlaf", laf)
    55           System.setProperty("swing.defaultlaf", laf)
    41       }
    56       }
    42 
    57 
    43       Desktop_App.about_handler {
    58       Desktop_App.about_handler {
    44         GUI.dialog(null, "Java Monitor",
    59         GUI.dialog(null, "Java Monitor",
    45           JConsoleResources.format(
    60           Untyped.the_method(ClassOf.Resources, "format").
    46             Messages.JCONSOLE_VERSION, System.getProperty("java.runtime.version"))
    61             invoke(null,
    47         )
    62               Untyped.get_static(ClassOf.Messages, "JCONSOLE_VERSION"),
       
    63                 System.getProperty("java.runtime.version")))
    48       }
    64       }
    49 
    65 
    50       val jconsole = new JConsole(false)
    66       val jconsole =
       
    67         Untyped.the_constructor(ClassOf.JConsole).newInstance(false).asInstanceOf[Component]
    51 
    68 
    52       val screen = GUI.mouse_location()
    69       val screen = GUI.mouse_location()
    53       val width = (1200 max (screen.bounds.width / 2)) min screen.bounds.width
    70       val width = (1200 max (screen.bounds.width / 2)) min screen.bounds.width
    54       val height = (900 max (screen.bounds.height / 2)) min screen.bounds.height
    71       val height = (900 max (screen.bounds.height / 2)) min screen.bounds.height
    55       jconsole.setBounds(
    72       Untyped.method(ClassOf.Component, "setBounds", classOf[Int], classOf[Int], classOf[Int], classOf[Int])
    56         screen.bounds.x + (screen.bounds.width - width) / 2,
    73         .invoke(jconsole,
    57         screen.bounds.y + (screen.bounds.height - height) / 2,
    74           screen.bounds.x + (screen.bounds.width - width) / 2,
    58         width, height)
    75           screen.bounds.y + (screen.bounds.height - height) / 2,
       
    76           width, height)
    59 
    77 
    60       jconsole.setVisible(true)
    78       Untyped.the_method(ClassOf.Component, "setVisible").invoke(jconsole, true)
    61 
    79 
    62       Untyped.method(classOf[JConsole], "createMDI").invoke(jconsole)
    80       Untyped.the_method(ClassOf.JConsole, "createMDI").invoke(jconsole)
    63 
    81 
    64       Isabelle_Thread.fork(name = "JConsole.addVmid") {
    82       Isabelle_Thread.fork(name = "JConsole.addVmid") {
    65         try {
    83         try {
    66           val proxy_client = ProxyClient.getProxyClient(vm)
    84           val proxy_client =
       
    85             Untyped.method(ClassOf.ProxyClient, "getProxyClient", ClassOf.LocalVirtualMachine)
       
    86               .invoke(null, vm)
    67 
    87 
    68           GUI_Thread.later {
    88           GUI_Thread.later {
    69             try {
    89             try {
    70               val vm_panel =
    90               val vm_panel =
    71                 Untyped.constructor(classOf[VMPanel], classOf[ProxyClient], Integer.TYPE)
    91                 Untyped.constructor(ClassOf.VMPanel, ClassOf.ProxyClient, Integer.TYPE)
    72                   .newInstance(proxy_client, java.lang.Integer.valueOf(update_interval.ms.toInt))
    92                   .newInstance(proxy_client, java.lang.Integer.valueOf(update_interval.ms.toInt))
    73 
    93 
    74               Untyped.field(vm_panel, "shouldUseSSL").setBoolean(vm_panel, false)
    94               Untyped.field(vm_panel, "shouldUseSSL").setBoolean(vm_panel, false)
    75 
    95 
    76               Untyped.method(classOf[JConsole], "addFrame", classOf[VMPanel])
    96               Untyped.method(ClassOf.JConsole, "addFrame", ClassOf.VMPanel)
    77                 .invoke(jconsole, vm_panel)
    97                 .invoke(jconsole, vm_panel)
    78 
    98 
    79               GUI_Thread.later { jconsole.tileWindows() }
    99               GUI_Thread.later {
       
   100                 Untyped.the_method(ClassOf.JConsole, "tileWindows").invoke(jconsole)
       
   101               }
    80 
   102 
    81               vm_panel.connect()
   103               Untyped.the_method(ClassOf.VMPanel, "connect").invoke(vm_panel)
    82             }
   104             }
    83             catch {
   105             catch {
    84               case exn: Throwable =>
   106               case exn: Throwable =>
    85                 GUI.error_dialog(jconsole, "Error", GUI.scrollable_text(Exn.message(exn)))
   107                 GUI.error_dialog(jconsole, "Error", GUI.scrollable_text(Exn.message(exn)))
    86             }
   108             }