products/sources/formale sprachen/Isabelle/Tools/jEdit/patches/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Unknown

diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 2020-09-03 05:31:04.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2020-09-08 20:13:23.561140312 +0200
@@ -1130,9 +1130,7 @@
     return new Font("Monospaced", Font.PLAIN, 12);
    }
    else {
-    Font font2 =
-     new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
-      Font.PLAIN, font1.getSize());
+    Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
     FontRenderContext frc = new FontRenderContext(null, true, false);
     float scale =
      font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();

[ Dauer der Verarbeitung: 0.6 Sekunden  (vorverarbeitet)  ]