src/Pure/GUI/desktop_app.scala
author wenzelm
Fri, 26 Apr 2024 13:25:44 +0200
changeset 80150 96f60533ec1d
parent 75393 87ebf5a50283
permissions -rw-r--r--
update Windows test machines;
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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 72981
diff changeset
    12
object Desktop_App {
72981
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    13
  def desktop_action(action: Desktop.Action, f: Desktop => Unit): Unit =
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    14
    if (Desktop.isDesktopSupported) {
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    15
      val desktop = Desktop.getDesktop
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    16
      if (desktop.isSupported(action)) f(desktop)
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    17
    }
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    18
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    19
  def about_handler(handler: => Unit): Unit =
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    20
    desktop_action(Desktop.Action.APP_ABOUT, _.setAboutHandler(_ => handler))
c78d1dfc6571 more friendly desktop application on macOS;
wenzelm
parents:
diff changeset
    21
}