src/Pure/Admin/build_fonts.scala
author wenzelm
Sat Nov 24 18:56:44 2018 +0100 (19 months ago)
changeset 69343 395c4fb15ea2
parent 69341 6aa24ccd8049
child 69354 600727ff6889
permissions -rw-r--r--
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
     1 /*  Title:      Pure/Admin/build_fonts.scala
     2     Author:     Makarius
     3 
     4 Build of Isabelle fonts: DejaVu + special symbols.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Build_Fonts
    11 {
    12   /* relevant codepoint ranges */
    13 
    14   object Range
    15   {
    16     def base_font: Seq[Int] =
    17       (0x0020 to 0x007e) ++  // ASCII
    18       (0x00a0 to 0x024f) ++  // Latin Extended-A/B
    19       (0x0400 to 0x04ff) ++  // Cyrillic
    20       (0x0600 to 0x06ff) ++  // Arabic
    21       Seq(
    22         0x2018,  // single quote
    23         0x2019,  // single quote
    24         0x201a,  // single quote
    25         0x201c,  // double quote
    26         0x201d,  // double quote
    27         0x201e,  // double quote
    28         0x2039,  // single guillemet
    29         0x203a,  // single guillemet
    30         0x204b,  // FOOTNOTE
    31         0x20ac,  // Euro
    32         0xfb01,  // ligature fi
    33         0xfb02,  // ligature fl
    34         0xfffd,  // replacement character
    35       )
    36 
    37     def isabelle_font: Seq[Int] =
    38       Seq(
    39         0x05,  // X
    40         0x06,  // Y
    41         0x07,  // EOF
    42         0x7f,  // DEL
    43         0xaf,  // INVERSE
    44         0xac,  // logicalnot
    45         0xb0,  // degree
    46         0xb1,  // plusminus
    47         0xb7,  // periodcentered
    48         0xd7,  // multiply
    49         0xf7,  // divide
    50       ) ++
    51       (0x0370 to 0x03ff) ++  // Greek (pseudo math)
    52       (0x0590 to 0x05ff) ++  // Hebrew (non-mono)
    53       Seq(
    54         0x2010,  // hyphen
    55         0x2013,  // dash
    56         0x2014,  // dash
    57         0x2015,  // dash
    58         0x2020,  // dagger
    59         0x2021,  // double dagger
    60         0x2022,  // bullet
    61         0x2026,  // ellipsis
    62         0x2030,  // perthousand
    63         0x2032,  // minute
    64         0x2033,  // second
    65         0x2038,  // caret
    66         0x20cd,  // currency symbol
    67       ) ++
    68       (0x2100 to 0x214f) ++  // Letterlike Symbols
    69       (0x2190 to 0x21ff) ++  // Arrows
    70       (0x2200 to 0x22ff) ++  // Mathematical Operators
    71       (0x2300 to 0x23ff) ++  // Miscellaneous Technical
    72       Seq(
    73         0x2423,  // graphic for space
    74         0x2500,  // box drawing
    75         0x2501,  // box drawing
    76         0x2508,  // box drawing
    77         0x2509,  // box drawing
    78         0x2550,  // box drawing
    79       ) ++
    80       (0x25a0 to 0x25ff) ++  // Geometric Shapes
    81       Seq(
    82         0x261b,  // ACTION
    83         0x2660,  // spade suit
    84         0x2661,  // heart suit
    85         0x2662,  // diamond suit
    86         0x2663,  // club suit
    87         0x266d,  // musical flat
    88         0x266e,  // musical natural
    89         0x266f,  // musical sharp
    90         0x2756,  // UNDEFINED
    91         0x2759,  // BOLD
    92         0x27a7,  // DESCR
    93         0x27e6,  // left white square bracket
    94         0x27e7,  // right white square bracket
    95         0x27e8,  // left angle bracket
    96         0x27e9,  // right angle bracket
    97       ) ++
    98       (0x27f0 to 0x27ff) ++  // Supplemental Arrows-A
    99       (0x2900 to 0x297f) ++  // Supplemental Arrows-B
   100       (0x2980 to 0x29ff) ++  // Miscellaneous Mathematical Symbols-B
   101       (0x2a00 to 0x2aff) ++  // Supplemental Mathematical Operators
   102       Seq(0x2b1a) ++  // VERBATIM
   103       (0x1d400 to 0x1d7ff) ++  // Mathematical Alphanumeric Symbols
   104       Seq(
   105         0x1f310,  // globe with meridians (Symbola font)
   106         0x1f4d3,  // notebook (Symbola font)
   107         0x1f5c0,  // folder (Symbola font)
   108         0x1f5cf,  // page (Symbola font)
   109       )
   110   }
   111 
   112 
   113   /* font families */
   114 
   115   sealed case class Family(
   116     plain: String = "",
   117     bold: String = "",
   118     italic: String = "",
   119     bold_italic: String = "")
   120   {
   121     val fonts: List[String] =
   122       proper_string(plain).toList :::
   123       proper_string(bold).toList :::
   124       proper_string(italic).toList :::
   125       proper_string(bold_italic).toList
   126 
   127     def get(index: Int): String = fonts(index % fonts.length)
   128   }
   129 
   130   object Family
   131   {
   132     def isabelle_text: Family =
   133       Family(
   134         plain = "IsabelleText.sfd",
   135         bold = "IsabelleTextBold.sfd")
   136 
   137     def deja_vu_sans_mono: Family =
   138       Family(
   139         plain = "DejaVuSansMono.ttf",
   140         bold = "DejaVuSansMono-Bold.ttf",
   141         italic = "DejaVuSansMono-Oblique.ttf",
   142         bold_italic = "DejaVuSansMono-BoldOblique.ttf")
   143 
   144     def deja_vu_sans: Family =
   145       Family(
   146         plain = "DejaVuSans.ttf",
   147         bold = "DejaVuSans-Bold.ttf",
   148         italic = "DejaVuSans-Oblique.ttf",
   149         bold_italic = "DejaVuSans-BoldOblique.ttf")
   150 
   151     def deja_vu_serif: Family =
   152       Family(
   153         plain = "DejaVuSerif.ttf",
   154         bold = "DejaVuSerif-Bold.ttf",
   155         italic = "DejaVuSerif-Italic.ttf",
   156         bold_italic = "DejaVuSerif-BoldItalic.ttf")
   157   }
   158 
   159 
   160   /* build fonts */
   161 
   162   private def find_file(dirs: List[Path], name: String): Path =
   163   {
   164     val path = Path.explode(name)
   165     dirs.collectFirst({ case dir if (dir + path).is_file => dir + path }) match {
   166       case Some(file) => file
   167       case None =>
   168         error(cat_lines(
   169           ("Failed to find font file " + path + " in directories:") ::
   170             dirs.map(dir => "  " + dir.toString)))
   171     }
   172   }
   173 
   174   val default_sources: List[Family] =
   175     List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif)
   176 
   177   def build_fonts(
   178     sources: List[Family] = default_sources,
   179     source_dirs: List[Path] = Nil,
   180     target_prefix: String = "Isabelle",
   181     target_version: String = "",
   182     target_dir: Path = Path.current,
   183     progress: Progress = No_Progress)
   184   {
   185     Isabelle_System.mkdirs(target_dir)
   186 
   187     val font_dirs = source_dirs ::: List(Path.explode("~~/lib/fonts"))
   188 
   189     for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex } {
   190       val isabelle_file = find_file(font_dirs, Family.isabelle_text.get(index))
   191 
   192       val source_file = find_file(font_dirs, source_font)
   193       val source_names = Fontforge.font_names(source_file)
   194 
   195       val target_names = source_names.update(prefix = target_prefix, version = target_version)
   196       val target_file = target_dir + target_names.ttf
   197 
   198       progress.echo("Creating " + target_file.toString + " ...")
   199       Fontforge.execute(
   200         Fontforge.commands(
   201           Fontforge.open(isabelle_file),
   202           Fontforge.select(Range.isabelle_font),
   203           Fontforge.copy,
   204           Fontforge.close,
   205 
   206           Fontforge.open(source_file),
   207           Fontforge.select(Range.base_font),
   208           Fontforge.select_invert,
   209           Fontforge.clear,
   210           Fontforge.select(Range.isabelle_font),
   211           Fontforge.paste,
   212 
   213           target_names.set,
   214           Fontforge.generate(target_file),
   215           Fontforge.close)
   216       ).check
   217     }
   218   }
   219 
   220 
   221   /* Isabelle tool wrapper */
   222 
   223   val isabelle_tool =
   224     Isabelle_Tool("build_fonts", "construct Isabelle fonts", args =>
   225     {
   226       var source_dirs: List[Path] = Nil
   227       var target_dir = Path.current
   228 
   229       val getopts = Getopts("""
   230 Usage: isabelle build_fonts [OPTIONS]
   231 
   232   Options are:
   233     -D DIR       target directory (default ".")
   234     -d DIR       additional source directory
   235 
   236   Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
   237 """,
   238         "D:" -> (arg => target_dir = Path.explode(arg)),
   239         "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
   240 
   241       val more_args = getopts(args)
   242       if (more_args.nonEmpty) getopts.usage()
   243 
   244       val progress = new Console_Progress
   245 
   246       build_fonts(source_dirs = source_dirs, target_dir = target_dir, progress = progress)
   247     })
   248 }