use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
--- 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
--- 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
--- 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 "\<inverse>" 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.
--- 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 */
--- 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 @@
\<some> code: 0x0003f5
\<hole> code: 0x002311
\<newline> code: 0x0023ce
-\<comment> code: 0x002015 group: document argument: space_cartouche font: IsabelleText
-\<^cancel> code: 0x002326 group: document argument: cartouche font: IsabelleText
+\<comment> 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
-\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
-\<close> 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
+\<open> code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: <<
+\<close> 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
--- 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
+
----------------------------------------------------------------------------
--- 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 \<open>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>\<open>IsabelleText\<close>, 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>\<open>Isabelle DejaVu\<close>, 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>\<open>IsabelleText\<close> 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>\<open>IsabelleText\<close> is older than the application version. This problem can be
- avoided by refraining to ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> 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>\<open>IsabelleText\<close> 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>\<open>IsabelleText\<close> 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.
\<close>
@@ -2141,7 +2140,7 @@
\<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
the main text area.
- \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
+ \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
event handling of Java/AWT/Swing.
--- 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))))
--- 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()
--- 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")
}
--- 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).
--- 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