src/Pure/GUI/desktop_app.scala
author wenzelm
Tue, 22 Dec 2020 15:49:22 +0100
changeset 72981 c78d1dfc6571
child 75393 87ebf5a50283
permissions -rw-r--r--
more friendly desktop application on macOS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72981
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/GUI/desktop_app.scala
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     3
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     4
Support for desktop applications, notably on macOS.
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     5
*/
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     6
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     7
package isabelle
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     8
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
     9
import java.awt.Desktop
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    10
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    11
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    12
object Desktop_App
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    13
{
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    14
  def desktop_action(action: Desktop.Action, f: Desktop => Unit): Unit =
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    15
    if (Desktop.isDesktopSupported) {
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    16
      val desktop = Desktop.getDesktop
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    17
      if (desktop.isSupported(action)) f(desktop)
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    18
    }
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    19
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    20
  def about_handler(handler: => Unit): Unit =
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    21
    desktop_action(Desktop.Action.APP_ABOUT, _.setAboutHandler(_ => handler))
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    22
}