# HG changeset patch # User wenzelm # Date 1584044753 -3600 # Node ID e76692ec6e5a62c1f89b76be5722be277562bb78 # Parent 57c3224e4c3056916a87a26b9aa8d1c45b721996 more usable defaults for high resolution on Linux, where the desktop environment usually lacks automatic scaling; diff -r 57c3224e4c30 -r e76692ec6e5a src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Thu Mar 12 21:13:42 2020 +0100 +++ b/src/Pure/Admin/build_release.scala Thu Mar 12 21:25:53 2020 +0100 @@ -491,6 +491,7 @@ }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar")) } + val jedit_options = Path.explode("src/Tools/jEdit/etc/options") val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props") @@ -506,6 +507,19 @@ platform match { case Platform.Family.linux => + File.write(isabelle_target + jedit_options, + File.read(isabelle_target + jedit_options) + .replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24")) + + File.write(isabelle_target + jedit_props, + File.read(isabelle_target + jedit_props) + .replaceAll("console.fontsize=.*", "console.fontsize=18") + .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18") + .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18") + .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18") + .replaceAll("view.fontsize=.*", "view.fontsize=24") + .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16")) + File.write(isabelle_target + Path.explode("Isabelle.options"), terminate_lines(java_options_title :: java_options))