Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Thu, 21 Aug 2025 20:07:40 +0200
changeset 83023 56d2510fd5ac
parent 83022 5fe1d566794e
child 83024 0b7cc1bf68e8
tuned;
src/Tools/jEdit/src/session_build.scala file | annotate | diff | comparison | revisions
src/Tools/jEdit/src/status_widget.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/session_build.scala	Thu Aug 21 19:55:30 2025 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Thu Aug 21 20:07:40 2025 +0200
@@ -38,7 +38,7 @@
     text.editable = false
     text.columns = 60
     text.rows = 24
-    text.font = GUI.copy_font((new Label).font)
+    text.font = GUI.copy_font(GUI.label_font())
     text.caret.color = text.background
 
     private val scroll_text = new ScrollPane(text)
--- a/src/Tools/jEdit/src/status_widget.scala	Thu Aug 21 19:55:30 2025 +0200
+++ b/src/Tools/jEdit/src/status_widget.scala	Thu Aug 21 20:07:40 2025 +0200
@@ -25,7 +25,7 @@
   abstract class GUI(view: View) extends JComponent {
     /* init */
 
-    setFont(new JLabel().getFont)
+    setFont(GUI.label_font())
 
     private val font_render_context = new FontRenderContext(null, true, false)
     private val line_metrics = getFont.getLineMetrics(template, font_render_context)
isabelle