Admin/isabelle_fonts/README
author wenzelm
Sun, 21 Mar 2021 23:05:17 +0100
changeset 73460 144431a135e9
parent 73457 3ede182a479a
child 73467 090add96f5f9
permissions -rw-r--r--
update README (actually after update of component);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
     1
Isabelle DejaVu fonts
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
     2
=====================
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
     3
69270
15463f546ee0 clarified isabelle_fonts license, to be used when the component is updated next time;
wenzelm
parents: 63677
diff changeset
     4
The Isabelle fonts are subject to the same BSD-3-clause license as Isabelle.
15463f546ee0 clarified isabelle_fonts license, to be used when the component is updated next time;
wenzelm
parents: 63677
diff changeset
     5
69354
600727ff6889 clarified Admin resources;
wenzelm
parents: 69343
diff changeset
     6
TTF files are produced automatically from the Deja Vu font family with symbols
70374
2b4c40722f0b updated to isabelle_fonts-20190717;
wenzelm
parents: 69797
diff changeset
     7
from the IsabelleSymbols font (formerly IsabelleText):
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
     8
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
     9
  isabelle build_fonts -d dejavu-fonts-ttf-2.37/ttf
29077
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    10
70374
2b4c40722f0b updated to isabelle_fonts-20190717;
wenzelm
parents: 69797
diff changeset
    11
The IsabelleSymbols template (see Admin/isabelle_fonts in the repository) has
69354
600727ff6889 clarified Admin resources;
wenzelm
parents: 69343
diff changeset
    12
been assembled manually, by composing glyphs from Bluesky TeX fonts (scaled
600727ff6889 clarified Admin resources;
wenzelm
parents: 69343
diff changeset
    13
222%) with some additions from DejaVu Sans Mono and DejaVu Sans. Some
600727ff6889 clarified Admin resources;
wenzelm
parents: 69343
diff changeset
    14
additional symbols are from Symbola, see http://greekfonts.teilar.gr "In lieu
600727ff6889 clarified Admin resources;
wenzelm
parents: 69343
diff changeset
    15
of a licence; fonts and documents in this site are free for any use; George
600727ff6889 clarified Admin resources;
wenzelm
parents: 69343
diff changeset
    16
Douros".
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
    17
73460
144431a135e9 update README (actually after update of component);
wenzelm
parents: 73457
diff changeset
    18
The blackboard-bold glyphs are from font "txmia" (package "pxfonts"):
144431a135e9 update README (actually after update of component);
wenzelm
parents: 73457
diff changeset
    19
these are subject to GPL.
144431a135e9 update README (actually after update of component);
wenzelm
parents: 73457
diff changeset
    20
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
    21
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
    22
    Makarius
73460
144431a135e9 update README (actually after update of component);
wenzelm
parents: 73457
diff changeset
    23
    21-Mar-2021
69343
395c4fb15ea2 use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents: 69270
diff changeset
    24
63677
be8b557ec73e some icons from Symbola font;
wenzelm
parents: 40966
diff changeset
    25
29077
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    26
----------------------------------------------------------------------------
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    27
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    28
Computer Modern PostScript Fonts
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    29
(Adobe Type 1 format)
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    30
2001/06/06
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    31
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    32
-----------------------------------------------------------------------------
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    33
The PostScript Type 1 implementation of the Computer Modern fonts produced by
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    34
and previously distributed by Blue Sky Research and Y&Y, Inc. are now freely
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    35
available for general use. This has been accomplished through the cooperation
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    36
of a consortium of scientific publishers with Blue Sky Research and Y&Y.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    37
Members of this consortium include:
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    38
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    39
        Elsevier Science
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    40
        IBM Corporation
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    41
        Society for Industrial and Applied Mathematics (SIAM)
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    42
        Springer-Verlag
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    43
        American Mathematical Society (AMS)
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    44
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    45
In order to assure the authenticity of these fonts, copyright will be held
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    46
by the American Mathematical Society. This is not meant to restrict in any
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    47
way the legitimate use of the fonts, such as (but not limited to) electronic
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    48
distribution of documents containing these fonts, inclusion of these fonts
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    49
into other public domain or commercial font collections or computer
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    50
applications, use of the outline data to create derivative fonts and/or
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    51
faces, etc. However, the AMS does require that the AMS copyright notice be
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    52
removed from any derivative versions of the fonts which have been altered in
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    53
any way. In addition, to ensure the fidelity of TeX documents using Computer
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    54
Modern fonts, Professor Donald Knuth, creator of the Computer Modern faces,
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    55
has requested that any alterations which yield different font metrics be
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    56
given a different name.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    57
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    58
----------------------------------------------------------------------------
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    59
----------------------------------------------------------------------------
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    60
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    61
Bitstream Vera Fonts Copyright
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    62
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    63
The fonts have a generous copyright, allowing derivative works (as
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    64
long as "Bitstream" or "Vera" are not in the names), and full
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    65
redistribution (so long as they are not *sold* by themselves). They
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    66
can be be bundled, redistributed and sold with any software.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    67
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    68
The fonts are distributed under the following copyright:
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    69
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    70
Copyright
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    71
=========
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    72
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    73
Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. Bitstream
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    74
Vera is a trademark of Bitstream, Inc.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    75
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    76
Permission is hereby granted, free of charge, to any person obtaining
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    77
a copy of the fonts accompanying this license ("Fonts") and associated
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    78
documentation files (the "Font Software"), to reproduce and distribute
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    79
the Font Software, including without limitation the rights to use,
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    80
copy, merge, publish, distribute, and/or sell copies of the Font
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    81
Software, and to permit persons to whom the Font Software is furnished
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    82
to do so, subject to the following conditions:
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    83
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    84
The above copyright and trademark notices and this permission notice
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    85
shall be included in all copies of one or more of the Font Software
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    86
typefaces.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    87
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    88
The Font Software may be modified, altered, or added to, and in
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    89
particular the designs of glyphs or characters in the Fonts may be
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    90
modified and additional glyphs or characters may be added to the
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    91
Fonts, only if the fonts are renamed to names not containing either
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    92
the words "Bitstream" or the word "Vera".
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    93
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    94
This License becomes null and void to the extent applicable to Fonts
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    95
or Font Software that has been modified and is distributed under the
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    96
"Bitstream Vera" names.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    97
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    98
The Font Software may be sold as part of a larger software package but
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
    99
no copy of one or more of the Font Software typefaces may be sold by
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   100
itself.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   101
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   102
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   103
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   104
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   105
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   106
BITSTREAM OR THE GNOME FOUNDATION BE LIABLE FOR ANY CLAIM, DAMAGES OR
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   107
OTHER LIABILITY, INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL,
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   108
OR CONSEQUENTIAL DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   109
OTHERWISE, ARISING FROM, OUT OF THE USE OR INABILITY TO USE THE FONT
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   110
SOFTWARE OR FROM OTHER DEALINGS IN THE FONT SOFTWARE.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   111
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   112
Except as contained in this notice, the names of Gnome, the Gnome
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   113
Foundation, and Bitstream Inc., shall not be used in advertising or
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   114
otherwise to promote the sale, use or other dealings in this Font
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   115
Software without prior written authorization from the Gnome Foundation
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   116
or Bitstream Inc., respectively. For further information, contact:
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   117
fonts at gnome dot org.
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   118
20c277589fe6 added README with original licenses;
wenzelm
parents:
diff changeset
   119
----------------------------------------------------------------------------