src/Pure/Tools/isabelle_fonts.scala
author wenzelm
Fri, 23 Nov 2018 14:50:32 +0100
changeset 69332 85ccc983748c
parent 69331 85cafb6e4db0
child 69336 14444ea196a0
permissions -rw-r--r--
clarified;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/isabelle_fonts.scala
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     3
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     4
Construction of Isabelle fonts.
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     5
*/
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     6
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     7
package isabelle
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     8
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
     9
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    10
object Isabelle_Fonts
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    11
{
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    12
  /* relevant codepoint ranges */
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    13
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    14
  object Range
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    15
  {
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    16
    def plain_text: Seq[Int] =
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    17
      (0x0020 to 0x007e) ++  // ASCII
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    18
      (0x00a0 to 0x024f) ++  // Latin Extended-A/B
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    19
      (0x0400 to 0x04ff) ++  // Cyrillic
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    20
      (0x0590 to 0x05ff) ++  // Hebrew (non-mono)
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    21
      (0x0600 to 0x06ff) ++  // Arabic
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    22
      Seq(
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    23
        0x2018,  // single quote
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    24
        0x2019,  // single quote
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    25
        0x201a,  // single quote
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    26
        0x201c,  // double quote
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    27
        0x201d,  // double quote
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    28
        0x201e,  // double quote
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    29
        0x2039,  // single guillemet
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    30
        0x203a,  // single guillemet
69331
85cafb6e4db0 tuned comments -- based on history;
wenzelm
parents: 69330
diff changeset
    31
        0x204b,  // FOOTNOTE
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    32
        0x20ac,  // Euro
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    33
        0xfb01,  // ligature fi
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    34
        0xfb02,  // ligature fl
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    35
        0xfffd,  // replacement character
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    36
      )
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    37
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    38
    def symbols: Seq[Int] =
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    39
      Seq(
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    40
        0x05,  // X
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    41
        0x06,  // Y
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    42
        0x07,  // EOF
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    43
        0x7f,  // DEL
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    44
        0xac,  // logicalnot
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    45
        0xb0,  // degree
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    46
        0xb1,  // plusminus
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    47
        0xb7,  // periodcentered
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    48
        0xd7,  // multiply
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    49
        0xf7,  // divide
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    50
      ) ++
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    51
      (0x0370 to 0x03ff) ++  // Greek (pseudo math)
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    52
      Seq(
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    53
        0x2010,  // hyphen
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    54
        0x2013,  // dash
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    55
        0x2014,  // dash
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    56
        0x2015,  // dash
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    57
        0x2020,  // dagger
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    58
        0x2021,  // double dagger
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    59
        0x2022,  // bullet
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    60
        0x2026,  // ellipsis
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    61
        0x2030,  // perthousand
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    62
        0x2032,  // minute
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    63
        0x2033,  // second
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    64
        0x2038,  // caret
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    65
        0x20cd,  // currency symbol
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    66
      ) ++
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    67
      (0x2100 to 0x214f) ++  // Letterlike Symbols
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    68
      (0x2190 to 0x21ff) ++  // Arrows
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    69
      (0x2200 to 0x22ff) ++  // Mathematical Operators
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    70
      (0x2300 to 0x23ff) ++  // Miscellaneous Technical
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    71
      Seq(
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    72
        0x2423,  // graphic for space
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    73
        0x2500,  // box drawing
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    74
        0x2501,  // box drawing
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    75
        0x2508,  // box drawing
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    76
        0x2509,  // box drawing
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    77
        0x2550,  // box drawing
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    78
      ) ++
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    79
      (0x25a0 to 0x25ff) ++  // Geometric Shapes
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    80
      Seq(
69331
85cafb6e4db0 tuned comments -- based on history;
wenzelm
parents: 69330
diff changeset
    81
        0x261b,  // ACTION
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    82
        0x2660,  // spade suit
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    83
        0x2661,  // heart suit
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    84
        0x2662,  // diamond suit
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    85
        0x2663,  // club suit
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    86
        0x266d,  // musical flat
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    87
        0x266e,  // musical natural
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    88
        0x266f,  // musical sharp
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    89
        0x2756,  // UNDEFINED
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    90
        0x2759,  // BOLD
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    91
        0x27a7,  // DESCR
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    92
        0x27e6,  // left white square bracket
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    93
        0x27e7,  // right white square bracket
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    94
        0x27e8,  // left angle bracket
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    95
        0x27e9,  // right angle bracket
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    96
      ) ++
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    97
      (0x27f0 to 0x27ff) ++  // Supplemental Arrows-A
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    98
      (0x2900 to 0x297f) ++  // Supplemental Arrows-B
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
    99
      (0x2980 to 0x29ff) ++  // Miscellaneous Mathematical Symbols-B
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   100
      (0x2a00 to 0x2aff) ++  // Supplemental Mathematical Operators
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   101
      Seq(0x2b1a) ++  // VERBATIM
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   102
      (0x1d400 to 0x1d7ff) ++  // Mathematical Alphanumeric Symbols
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   103
      Seq(
69331
85cafb6e4db0 tuned comments -- based on history;
wenzelm
parents: 69330
diff changeset
   104
        0x1f310,  // globe with meridians (Symbola font)
85cafb6e4db0 tuned comments -- based on history;
wenzelm
parents: 69330
diff changeset
   105
        0x1f4d3,  // notebook (Symbola font)
85cafb6e4db0 tuned comments -- based on history;
wenzelm
parents: 69330
diff changeset
   106
        0x1f5c0,  // folder (Symbola font)
85cafb6e4db0 tuned comments -- based on history;
wenzelm
parents: 69330
diff changeset
   107
        0x1f5cf,  // page (Symbola font)
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   108
      )
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   109
  }
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   110
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   111
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   112
  /* font families */
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   113
69332
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   114
  sealed case class Family(
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   115
    plain: String = "",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   116
    bold: String = "",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   117
    italic: String = "",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   118
    bold_italic: String = "",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   119
    fallback: Option[Family] = None)
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   120
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   121
  object Family
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   122
  {
69332
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   123
    def deja_vu_sans_mono: Family =
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   124
      Family(
69332
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   125
        plain = "DejaVuSansMono.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   126
        bold = "DejaVuSansMono-Bold.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   127
        italic = "DejaVuSansMono-Oblique.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   128
        bold_italic = "DejaVuSansMono-BoldOblique.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   129
        fallback = Some(deja_vu_sans))
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   130
69332
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   131
    def deja_vu_sans: Family =
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   132
      Family(
69332
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   133
        plain = "DejaVuSans.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   134
        bold = "DejaVuSans-Bold.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   135
        italic = "DejaVuSans-Oblique.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   136
        bold_italic = "DejaVuSans-BoldOblique.ttf")
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   137
69332
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   138
    def deja_vu_serif: Family =
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   139
      Family(
69332
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   140
        plain = "DejaVuSerif.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   141
        bold = "DejaVuSerif-Bold.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   142
        italic = "DejaVuSerif-Italic.ttf",
85ccc983748c clarified;
wenzelm
parents: 69331
diff changeset
   143
        bold_italic = "DejaVuSerif-BoldItalic.ttf")
69330
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   144
  }
6a33b12f8573 support for construction of Isabelle fonts;
wenzelm
parents:
diff changeset
   145
}