# HG changeset patch
# User wenzelm
# Date 1608648562 -3600
# Node ID c78d1dfc65710169c4b5e70798e850bd2ff6a8e4
# Parent  7e7ed27fe62572eb43c427bd2242119714b33aa4
more friendly desktop application on macOS;

diff -r 7e7ed27fe625 -r c78d1dfc6571 lib/Tools/java_monitor
--- a/lib/Tools/java_monitor	Mon Dec 21 23:22:14 2020 +0100
+++ b/lib/Tools/java_monitor	Tue Dec 22 15:49:22 2020 +0100
@@ -4,4 +4,4 @@
 #
 # DESCRIPTION: monitor another Java process
 
-isabelle java isabelle.Java_Monitor "$@"
+isabelle java "-Dapple.awt.application.name=Java Monitor" isabelle.Java_Monitor "$@"
diff -r 7e7ed27fe625 -r c78d1dfc6571 src/Pure/GUI/desktop_app.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/GUI/desktop_app.scala	Tue Dec 22 15:49:22 2020 +0100
@@ -0,0 +1,22 @@
+/*  Title:      Pure/GUI/desktop_app.scala
+    Author:     Makarius
+
+Support for desktop applications, notably on macOS.
+*/
+
+package isabelle
+
+import java.awt.Desktop
+
+
+object Desktop_App
+{
+  def desktop_action(action: Desktop.Action, f: Desktop => Unit): Unit =
+    if (Desktop.isDesktopSupported) {
+      val desktop = Desktop.getDesktop
+      if (desktop.isSupported(action)) f(desktop)
+    }
+
+  def about_handler(handler: => Unit): Unit =
+    desktop_action(Desktop.Action.APP_ABOUT, _.setAboutHandler(_ => handler))
+}
diff -r 7e7ed27fe625 -r c78d1dfc6571 src/Pure/Tools/java_monitor.scala
--- a/src/Pure/Tools/java_monitor.scala	Mon Dec 21 23:22:14 2020 +0100
+++ b/src/Pure/Tools/java_monitor.scala	Tue Dec 22 15:49:22 2020 +0100
@@ -9,7 +9,8 @@
 
 import java.awt.Component
 import javax.swing.UIManager
-import sun.tools.jconsole.{JConsole, LocalVirtualMachine, VMPanel, ProxyClient}
+import sun.tools.jconsole.{JConsole, LocalVirtualMachine, VMPanel, ProxyClient,
+  Messages, Resources => JConsoleResources}
 
 
 object Java_Monitor
@@ -40,6 +41,13 @@
           System.setProperty("swing.defaultlaf", laf)
       }
 
+      Desktop_App.about_handler {
+        GUI.dialog(null, "Java Monitor",
+          JConsoleResources.format(
+            Messages.JCONSOLE_VERSION, System.getProperty("java.runtime.version"))
+        )
+      }
+
       val jconsole = new JConsole(false)
 
       val screen = GUI.mouse_location()
diff -r 7e7ed27fe625 -r c78d1dfc6571 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Dec 21 23:22:14 2020 +0100
+++ b/src/Pure/build-jars	Tue Dec 22 15:49:22 2020 +0100
@@ -45,6 +45,7 @@
   src/Pure/Concurrent/par_list.scala
   src/Pure/Concurrent/synchronized.scala
   src/Pure/GUI/color_value.scala
+  src/Pure/GUI/desktop_app.scala
   src/Pure/GUI/gui.scala
   src/Pure/GUI/gui_thread.scala
   src/Pure/GUI/popup.scala