diff -r b3ca4a6ed74b -r 87ebf5a50283 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Fri Apr 01 11:51:42 2022 +0200 +++ b/src/Pure/GUI/gui.scala Fri Apr 01 17:06:10 2022 +0200 @@ -17,8 +17,7 @@ import scala.swing.event.SelectionChanged -object GUI -{ +object GUI { /* Swing look-and-feel */ def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.setup() @@ -28,8 +27,7 @@ def is_macos_laf: Boolean = Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf - class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service - { + class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service { def info: UIManager.LookAndFeelInfo = new UIManager.LookAndFeelInfo(laf.getName, laf.getClass.getName) } @@ -37,8 +35,7 @@ lazy val look_and_feels: List[Look_And_Feel] = Isabelle_System.make_services(classOf[Look_And_Feel]) - def init_lafs(): Unit = - { + def init_lafs(): Unit = { val old_lafs = Set( "com.sun.java.swing.plaf.motif.MotifLookAndFeel", @@ -55,8 +52,7 @@ /* plain focus traversal, notably for text fields */ - def plain_focus_traversal(component: Component): Unit = - { + def plain_focus_traversal(component: Component): Unit = { val dummy_button = new JButton def apply(id: Int): Unit = component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id)) @@ -67,9 +63,12 @@ /* simple dialogs */ - def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false) - : ScrollPane = - { + def scrollable_text( + raw_txt: String, + width: Int = 60, + height: Int = 20, + editable: Boolean = false + ) : ScrollPane = { val txt = Output.clean_yxml(raw_txt) val text = new TextArea(txt) if (width > 0) text.columns = width @@ -78,9 +77,13 @@ new ScrollPane(text) } - private def simple_dialog(kind: Int, default_title: String, - parent: Component, title: String, message: Iterable[Any]): Unit = - { + private def simple_dialog( + kind: Int, + default_title: String, + parent: Component, + title: String, + message: Iterable[Any] + ): Unit = { GUI_Thread.now { val java_message = message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }). @@ -113,8 +116,8 @@ private val Zoom_Factor = "([0-9]+)%?".r abstract class Zoom_Box extends ComboBox[String]( - List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) - { + List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%") + ) { def changed: Unit def factor: Int = parse(selection.item) @@ -128,8 +131,7 @@ private def print(i: Int): String = i.toString + "%" - def set_item(i: Int): Unit = - { + def set_item(i: Int): Unit = { peer.getEditor match { case null => case editor => editor.setItem(print(i)) @@ -170,10 +172,8 @@ /* location within multi-screen environment */ - final case class Screen_Location(point: Point, bounds: Rectangle) - { - def relative(parent: Component, size: Dimension): Point = - { + final case class Screen_Location(point: Point, bounds: Rectangle) { + def relative(parent: Component, size: Dimension): Point = { val w = size.width val h = size.height @@ -190,8 +190,7 @@ } } - def screen_location(component: Component, point: Point): Screen_Location = - { + def screen_location(component: Component, point: Point): Screen_Location = { val screen_point = new Point(point.x, point.y) if (component != null) SwingUtilities.convertPointToScreen(screen_point, component) @@ -212,8 +211,7 @@ /* screen size */ - sealed case class Screen_Size(bounds: Rectangle, insets: Insets) - { + sealed case class Screen_Size(bounds: Rectangle, insets: Insets) { def full_screen_bounds: Rectangle = if (Platform.is_linux) { // avoid menu bar and docking areas @@ -234,8 +232,7 @@ else bounds } - def screen_size(component: Component): Screen_Size = - { + def screen_size(component: Component): Screen_Size = { val config = component.getGraphicsConfiguration val bounds = config.getBounds val insets = Toolkit.getDefaultToolkit.getScreenInsets(config) @@ -274,10 +271,8 @@ case _ => None } - def traverse_components(component: Component, apply: Component => Unit): Unit = - { - def traverse(comp: Component): Unit = - { + def traverse_components(component: Component, apply: Component => Unit): Unit = { + def traverse(comp: Component): Unit = { apply(comp) comp match { case cont: Container => @@ -310,43 +305,44 @@ /* Isabelle fonts */ - def imitate_font(font: Font, + def imitate_font( + font: Font, family: String = Isabelle_Fonts.sans, - scale: Double = 1.0): Font = - { + scale: Double = 1.0 + ): Font = { val font1 = new Font(family, font.getStyle, font.getSize) val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt) } - def imitate_font_css(font: Font, + def imitate_font_css( + font: Font, family: String = Isabelle_Fonts.sans, - scale: Double = 1.0): String = - { + scale: Double = 1.0 + ): String = { val font1 = new Font(family, font.getStyle, font.getSize) val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;" } - def use_isabelle_fonts(): Unit = - { + def use_isabelle_fonts(): Unit = { val default_font = label_font() val ui = UIManager.getDefaults - for (prop <- List( - "ToggleButton.font", - "CheckBoxMenuItem.font", - "Label.font", - "Menu.font", - "MenuItem.font", - "PopupMenu.font", - "Table.font", - "TableHeader.font", - "TextArea.font", - "TextField.font", - "TextPane.font", - "ToolTip.font", - "Tree.font")) - { + for (prop <- + List( + "ToggleButton.font", + "CheckBoxMenuItem.font", + "Label.font", + "Menu.font", + "MenuItem.font", + "PopupMenu.font", + "Table.font", + "TableHeader.font", + "TextArea.font", + "TextField.font", + "TextPane.font", + "ToolTip.font", + "Tree.font")) { val font = ui.get(prop) match { case font: Font => font case _ => default_font } ui.put(prop, GUI.imitate_font(font)) }