src/Pure/Tools/java_monitor.scala
author wenzelm
Tue, 23 Nov 2021 12:29:09 +0100
changeset 74832 c299abcf7081
parent 73340 0ffcad1f6130
child 75393 87ebf5a50283
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    12
import sun.tools.jconsole.{JConsole, LocalVirtualMachine, VMPanel, ProxyClient,
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    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
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72981
diff changeset
    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
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    44
      Desktop_App.about_handler {
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    45
        GUI.dialog(null, "Java Monitor",
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    46
          JConsoleResources.format(
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    47
            Messages.JCONSOLE_VERSION, System.getProperty("java.runtime.version"))
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    48
        )
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    49
      }
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents: 72977
diff changeset
    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
e028331c578b clarified window size;
wenzelm
parents: 72976
diff changeset
    54
      val width = (1200 max (screen.bounds.width / 2)) min screen.bounds.width
e028331c578b clarified window size;
wenzelm
parents: 72976
diff changeset
    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
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72981
diff changeset
   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
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72981
diff changeset
   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
}