# HG changeset patch # User wenzelm # Date 1543082204 -3600 # Node ID 395c4fb15ea2ce374bd78969316df1d5edbee35b # Parent fa981730b9645b36cc6411a6ec7b4f21606c2f28 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.; diff -r fa981730b964 -r 395c4fb15ea2 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sat Nov 24 16:41:18 2018 +0100 +++ b/Admin/components/components.sha1 Sat Nov 24 18:56:44 2018 +0100 @@ -70,6 +70,7 @@ b70690c85c05d0ca5bc29287abd20142f6ddcfb0 isabelle_fonts-20171222.tar.gz c17c482e411bbaf992498041a3e1dea80336aaa6 isabelle_fonts-20171230.tar.gz 3affbb306baff37c360319b21cbaa2cc96ebb282 isabelle_fonts-20180113.tar.gz +bee32019e5d7cf096ef2ea1d836c732e9a7628cc isabelle_fonts-20181124.tar.gz 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz 71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz 8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz diff -r fa981730b964 -r 395c4fb15ea2 Admin/components/main --- a/Admin/components/main Sat Nov 24 16:41:18 2018 +0100 +++ b/Admin/components/main Sat Nov 24 18:56:44 2018 +0100 @@ -4,7 +4,7 @@ csdp-6.x cvc4-1.5-4 e-2.0-2 -isabelle_fonts-20180113 +isabelle_fonts-20181124 jdk-11+28 jedit_build-20181026 jfreechart-1.5.0 diff -r fa981730b964 -r 395c4fb15ea2 NEWS --- a/NEWS Sat Nov 24 16:41:18 2018 +0100 +++ b/NEWS Sat Nov 24 18:56:44 2018 +0100 @@ -9,6 +9,18 @@ *** General *** +* The font family "Isabelle DejaVu" is systematically derived from the +existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif" +and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique". +The DejaVu base fonts are retricted to well-defined Unicode ranges and +augmented by special Isabelle symbols, taken from the former +"IsabelleText" font (which is no longer provided separately). The line +metrics and overall rendering quality is closer to original DejaVu. +INCOMPATIBILITY with display configuration expecting the old +"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead. + +* The Isabelle fonts render "\" properly as superscript "-1". + * Old-style inner comments (* ... *) within the term language are no longer supported (legacy feature in Isabelle2018). @@ -22,6 +34,14 @@ *** Isabelle/jEdit Prover IDE *** +* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle +DejaVu" collection by default, which provides uniform rendering quality +with the usual Isabelle symbols. For Java/Swing GUI elements this +requires the Metal look-and-feel: it is the default on Linux, but not +macOS nor Windows. Line spacing no longer needs to be adjusted: +properties for the old IsabelleText font had "Global Options / Text Area +/ Extra vertical line spacing (in pixels): -2", now it defaults to 0. + * Improved sub-pixel font rendering (especially on Linux), thanks to OpenJDK 11. diff -r fa981730b964 -r 395c4fb15ea2 etc/isabelle.css --- a/etc/isabelle.css Sat Nov 24 16:41:18 2018 +0100 +++ b/etc/isabelle.css Sat Nov 24 18:56:44 2018 +0100 @@ -17,16 +17,16 @@ direction: ltr; unicode-bidi: bidi-override; background-color: #FFFFFF; padding: 10px; - font-family: IsabelleText; + font-family: "Isabelle DejaVu Sans Mono", monospace; line-height: 147%; } .theories { background-color: #FFFFFF; padding: 10px; } .sessions { background-color: #FFFFFF; padding: 10px; } -.document { white-space: normal; font-family: sans-serif; } +.document { white-space: normal; font-family: "Isabelle DejaVu Serif", serif; } .name { font-style: italic; } -.filename { font-family: fixed; } +.filename { font-family: "Isabelle DejaVu Sans Mono", monospace; } /* basic syntax markup */ diff -r fa981730b964 -r 395c4fb15ea2 etc/symbols --- a/etc/symbols Sat Nov 24 16:41:18 2018 +0100 +++ b/etc/symbols Sat Nov 24 18:56:44 2018 +0100 @@ -358,36 +358,36 @@ \ code: 0x0003f5 \ code: 0x002311 \ code: 0x0023ce -\ code: 0x002015 group: document argument: space_cartouche font: IsabelleText -\<^cancel> code: 0x002326 group: document argument: cartouche font: IsabelleText +\ code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^latex> group: document argument: cartouche -\ code: 0x002039 group: punctuation font: IsabelleText abbrev: << -\ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> -\<^here> code: 0x002302 font: IsabelleText -\<^undefined> code: 0x002756 font: IsabelleText -\<^noindent> code: 0x0021e4 group: document font: IsabelleText -\<^smallskip> code: 0x002508 group: document font: IsabelleText -\<^medskip> code: 0x002509 group: document font: IsabelleText -\<^bigskip> code: 0x002501 group: document font: IsabelleText -\<^item> code: 0x0025aa group: document font: IsabelleText -\<^enum> code: 0x0025b8 group: document font: IsabelleText -\<^descr> code: 0x0027a7 group: document font: IsabelleText -\<^footnote> code: 0x00204b group: document argument: cartouche font: IsabelleText -\<^verbatim> code: 0x0025a9 group: document argument: cartouche font: IsabelleText -\<^theory_text> code: 0x002b1a group: document argument: cartouche font: IsabelleText -\<^emph> code: 0x002217 group: document argument: cartouche font: IsabelleText -\<^bold> code: 0x002759 group: control argument: cartouche group: document font: IsabelleText -\<^sub> code: 0x0021e9 group: control font: IsabelleText -\<^sup> code: 0x0021e7 group: control font: IsabelleText -\<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_( -\<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_) -\<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^( -\<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^) -\<^file> code: 0x01F5CF group: icon argument: cartouche font: IsabelleText -\<^dir> code: 0x01F5C0 group: icon argument: cartouche font: IsabelleText -\<^url> code: 0x01F310 group: icon argument: cartouche font: IsabelleText -\<^doc> code: 0x01F4D3 group: icon argument: cartouche font: IsabelleText -\<^action> code: 0x00261b group: icon argument: cartouche font: IsabelleText +\ code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: << +\ code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >> +\<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono +\<^undefined> code: 0x002756 font: Isabelle␣DejaVu␣Sans␣Mono +\<^noindent> code: 0x0021e4 group: document font: Isabelle␣DejaVu␣Sans␣Mono +\<^smallskip> code: 0x002508 group: document font: Isabelle␣DejaVu␣Sans␣Mono +\<^medskip> code: 0x002509 group: document font: Isabelle␣DejaVu␣Sans␣Mono +\<^bigskip> code: 0x002501 group: document font: Isabelle␣DejaVu␣Sans␣Mono +\<^item> code: 0x0025aa group: document font: Isabelle␣DejaVu␣Sans␣Mono +\<^enum> code: 0x0025b8 group: document font: Isabelle␣DejaVu␣Sans␣Mono +\<^descr> code: 0x0027a7 group: document font: Isabelle␣DejaVu␣Sans␣Mono +\<^footnote> code: 0x00204b group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^verbatim> code: 0x0025a9 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^theory_text> code: 0x002b1a group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^emph> code: 0x002217 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^bold> code: 0x002759 group: control argument: cartouche group: document font: Isabelle␣DejaVu␣Sans␣Mono +\<^sub> code: 0x0021e9 group: control font: Isabelle␣DejaVu␣Sans␣Mono +\<^sup> code: 0x0021e7 group: control font: Isabelle␣DejaVu␣Sans␣Mono +\<^bsub> code: 0x0021d8 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_( +\<^esub> code: 0x0021d9 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_) +\<^bsup> code: 0x0021d7 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^( +\<^esup> code: 0x0021d6 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^) +\<^file> code: 0x01F5CF group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^dir> code: 0x01F5C0 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^url> code: 0x01F310 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^doc> code: 0x01F4D3 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono +\<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^assert> \<^binding> argument: cartouche \<^class> argument: cartouche diff -r fa981730b964 -r 395c4fb15ea2 lib/fonts/README --- a/lib/fonts/README Sat Nov 24 16:41:18 2018 +0100 +++ b/lib/fonts/README Sat Nov 24 18:56:44 2018 +0100 @@ -1,13 +1,23 @@ +Isabelle DejaVu fonts +===================== + The Isabelle fonts are subject to the same BSD-3-clause license as Isabelle. -The fonts have been assembled with FontForge -(http://fontforge.sourceforge.net), by composing glyphs from existing (free) -fonts: Bluesky TeX fonts (scaled 222%) and Bitstream Vera Mono, with some -additions from DejaVu Sans Mono and DejaVu Sans. +TTF files are produced automatically from the Deja Vu font family, with +special symbols from the IsabelleText font in $ISABELLE_HOME/lib/fonts: + + isabelle build_fonts -d dejavu-fonts-ttf-2.37/ttf -Some additional symbols are from Symbola. See http://greekfonts.teilar.gr -"In lieu of a licence; fonts and documents in this site are free for any use; -George Douros". +The IsabelleText template has been assembled manually, by composing glyphs +from Bluesky TeX fonts (scaled 222%) with some additions from DejaVu Sans Mono +and DejaVu Sans. Some additional symbols are from Symbola, see +http://greekfonts.teilar.gr "In lieu of a licence; fonts and documents in this +site are free for any use; George Douros". + + + Makarius + 23-Nov-2018 + ---------------------------------------------------------------------------- diff -r fa981730b964 -r 395c4fb15ea2 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sat Nov 24 16:41:18 2018 +0100 +++ b/src/Doc/JEdit/JEdit.thy Sat Nov 24 18:56:44 2018 +0100 @@ -525,21 +525,20 @@ text \Correct rendering via Unicode requires a font that contains glyphs for the corresponding codepoints. There are also various unusual symbols with particular purpose in Isabelle, e.g.\ control symbols and very long arrows. - Isabelle/jEdit prefers its own application fonts \<^verbatim>\IsabelleText\, which - ensures that standard collection of Isabelle symbols is actually shown on - the screen (or printer) as expected. + Isabelle/jEdit prefers its own font collection \<^verbatim>\Isabelle DejaVu\, which + ensures that all standard Isabelle symbols are shown on the screen (or + printer) as expected. Note that a Java/AWT/Swing application can load additional fonts only if - they are not installed on the operating system already! Some outdated - version of \<^verbatim>\IsabelleText\ that happens to be provided by the operating - system would prevent Isabelle/jEdit to use its bundled version. This could - lead to missing glyphs (black rectangles), when the system version of - \<^verbatim>\IsabelleText\ is older than the application version. This problem can be - avoided by refraining to ``install'' any version of \<^verbatim>\IsabelleText\ in the - first place, although it might be tempting to use the same font in other - applications. + they are not installed on the operating system already! Outdated versions of + Isabelle fonts that happen to be provided by the operating system prevent + Isabelle/jEdit to use its bundled version. This could lead to missing glyphs + (black rectangles), when the system version of a font is older than the + application version. This problem can be avoided by refraining to + ``install'' any version of \<^verbatim>\IsabelleText\ in the first place, although it + might be tempting to use the same font in other applications. - HTML pages generated by Isabelle refer to the same \<^verbatim>\IsabelleText\ font as a + HTML pages generated by Isabelle refer to the same Isabelle fonts as a server-side resource. Thus a web-browser can use that without requiring a locally installed copy. \ @@ -2141,7 +2140,7 @@ \<^item> \<^bold>\Problem:\ Mac OS X system fonts sometimes lead to character drop-outs in the main text area. - \<^bold>\Workaround:\ Use the default \<^verbatim>\IsabelleText\ font. + \<^bold>\Workaround:\ Use the default \<^verbatim>\Isabelle DejaVu\ fonts. \<^item> \<^bold>\Problem:\ Some Linux/X11 input methods such as IBus tend to disrupt key event handling of Java/AWT/Swing. diff -r fa981730b964 -r 395c4fb15ea2 src/Pure/Admin/build_fonts.scala --- a/src/Pure/Admin/build_fonts.scala Sat Nov 24 16:41:18 2018 +0100 +++ b/src/Pure/Admin/build_fonts.scala Sat Nov 24 18:56:44 2018 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/Admin/build_fonts.scala Author: Makarius -Build of Isabelle fonts: Deja Vu + special symbols. +Build of Isabelle fonts: DejaVu + special symbols. */ package isabelle @@ -186,24 +186,6 @@ val font_dirs = source_dirs ::: List(Path.explode("~~/lib/fonts")) - for (isabelle_font <- Family.isabelle_text.fonts) { - val isabelle_file = find_file(font_dirs, isabelle_font) - val isabelle_names = Fontforge.font_names(isabelle_file) - - val target_names = isabelle_names.update(version = target_version) - val target_file = target_dir + target_names.ttf - - progress.echo("Creating " + target_file.toString + " ...") - Fontforge.execute( - Fontforge.commands( - Fontforge.open(isabelle_file), - target_names.set, - Fontforge.generate(target_file), - Fontforge.close - ) - ).check - } - for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex } { val isabelle_file = find_file(font_dirs, Family.isabelle_text.get(index)) @@ -251,7 +233,7 @@ -D DIR target directory (default ".") -d DIR additional source directory - Construct Isabelle fonts from Deja Vu font families and Isabelle symbols. + Construct Isabelle fonts from DejaVu font families and Isabelle symbols. """, "D:" -> (arg => target_dir = Path.explode(arg)), "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg)))) diff -r fa981730b964 -r 395c4fb15ea2 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Sat Nov 24 16:41:18 2018 +0100 +++ b/src/Pure/GUI/gui.scala Sat Nov 24 18:56:44 2018 +0100 @@ -236,7 +236,7 @@ font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform))) } - def font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font = + def font(family: String = "Isabelle DejaVu Sans", size: Int = 1, bold: Boolean = false): Font = new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) def install_fonts() diff -r fa981730b964 -r 395c4fb15ea2 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Sat Nov 24 16:41:18 2018 +0100 +++ b/src/Pure/Thy/html.scala Sat Nov 24 18:56:44 2018 +0100 @@ -358,19 +358,31 @@ def fonts_css(make_url: String => String = fonts_url()): String = { - def font_face(name: String, ttf_name: String, bold: Boolean = false): String = + def font_face( + name: String, ttf_name: String, bold: Boolean = false, italic: Boolean = false): String = cat_lines( List( "@font-face {", " font-family: '" + name + "';", " src: url('" + make_url(ttf_name) + "') format('truetype');") ::: (if (bold) List(" font-weight: bold;") else Nil) ::: + (if (italic) List(" font-style: italic;") else Nil) ::: List("}")) List( "/* Isabelle fonts */", - font_face("IsabelleText", "IsabelleText.ttf"), - font_face("IsabelleText", "IsabelleTextBold.ttf", bold = true), + font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono.ttf"), + font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Bold.ttf", bold = true), + font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Oblique.ttf", italic = true), + font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-BoldOblique.ttf", bold = true, italic = true), + font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans.ttf"), + font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Bold.ttf", bold = true), + font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Oblique.ttf", italic = true), + font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-BoldOblique.ttf", bold = true, italic = true), + font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif.ttf"), + font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Bold.ttf", bold = true), + font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Oblique.ttf", italic = true), + font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-BoldOblique.ttf", bold = true, italic = true), font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n") } diff -r fa981730b964 -r 395c4fb15ea2 src/Tools/VSCode/extension/README.md --- a/src/Tools/VSCode/extension/README.md Sat Nov 24 16:41:18 2018 +0100 +++ b/src/Tools/VSCode/extension/README.md Sat Nov 24 18:56:44 2018 +0100 @@ -161,7 +161,7 @@ ## Known Limitations of Isabelle/VSCode - * Lack of specific support for the `IsabelleText` fonts: these need to be + * Lack of specific support for the Isabelle fonts: these need to be manually installed on the system and configured for VSCode (see also `$ISABELLE_FONTS` within the Isabelle environment). diff -r fa981730b964 -r 395c4fb15ea2 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Sat Nov 24 16:41:18 2018 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Sat Nov 24 18:56:44 2018 +0100 @@ -12,7 +12,7 @@ complete-word.shortcut= console.dock-position=floating console.encoding=UTF-8 -console.font=IsabelleText +console.font=Isabelle DejaVu Sans Mono console.fontsize=14 delete-line.shortcut=A+d delete.shortcut2=C+d @@ -183,6 +183,7 @@ focus-buffer-switcher.shortcut2=A+CIRCUMFLEX foldPainter=Circle gatchan.highlight.overview=false +helpviewer.font=Isabelle DejaVu Serif home.shortcut= insert-newline-indent.shortcut= insert-newline.shortcut= @@ -251,6 +252,8 @@ logo.icon.medium=32x32/apps/isabelle.gif lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel match-bracket.shortcut2=C+9 +metal.primary.font=Isabelle DejaVu Sans +metal.secondary.font=Isabelle DejaVu Sans navigator.showOnToolbar=true next-bracket.shortcut2=C+e C+9 options.shortcuts.deletekeymap.label=Delete @@ -258,12 +261,12 @@ options.shortcuts.duplicatekeymap.label=Duplicate options.shortcuts.resetkeymap.dialog.title=Reset keymap options.shortcuts.resetkeymap.label=Reset -options.textarea.lineSpacing=-2 +options.textarea.lineSpacing=0 plugin-blacklist.MacOSX.jar=true plugin.MacOSXPlugin.altDispatcher=false plugin.MacOSXPlugin.disableOption=true prev-bracket.shortcut2=C+e C+8 -print.font=IsabelleText +print.font=Isabelle DejaVu Sans Mono print.glyphVector=true recent-buffer.shortcut2=C+CIRCUMFLEX restore.remote=false @@ -300,9 +303,10 @@ view.docking.framework=PIDE view.eolMarkers=false view.extendedState=0 -view.font=IsabelleText +view.font=Isabelle DejaVu Sans Mono view.fontsize=18 view.fracFontMetrics=false +view.gutter.font=Isabelle DejaVu Sans Mono view.gutter.fontsize=12 view.gutter.lineNumbers=false view.gutter.selectionAreaWidth=18