Quelle component_fonts.scala Sprache: Scala

/*  Title:      Pure/Admin/component_fonts.scala
    Author:     Makarius

Build standard Isabelle fonts: DejaVu base + Isabelle symbols.
*/

package isabelle

object Component_Fonts {
  /* relevant codepoint ranges */

  object Range {
    def base_font: Seq[Int] =
      (0x0020 to 0x007e) ++  // ASCII
      (0x00a0 to 0x024f) ++  // Latin Extended-A/B
      (0x0400 to 0x04ff) ++  // Cyrillic
      (0x0600 to 0x06ff) ++  // Arabic
      Seq(
        0x02dd,  // hungarumlaut
        0x2018,  // single quote
        0x2019,  // single quote
        0x201a,  // single quote
        0x201c,  // double quote
        0x201d,  // double quote
        0x201e,  // double quote
        0x2022,  // regular bullet
        0x2023,  // triangular bullet
        0x2039,  // single guillemet
        0x203a,  // single guillemet
        0x204b,  // FOOTNOTE
        0x20ac,  // Euro
        0x2710,  // pencil
        0xfb01,  // ligature fi
        0xfb02,  // ligature fl
        0xfffd,  // replacement character
      )

    def isabelle_font: Seq[Int] =
      Seq(
        0x05,  // X
        0x06,  // Y
        0x07,  // EOF
        0x7f,  // DEL
        0xaf,  // INVERSE
        0xac,  // logicalnot
        0xb0,  // degree
        0xb1,  // plusminus
        0xb7,  // periodcentered
        0xd7,  // multiply
        0xf7,  // divide
      ) ++
      (0x0370 to 0x03ff) ++  // Greek (pseudo math)
      (0x0590 to 0x05ff) ++  // Hebrew (non-mono)
      Seq(
        0x2010,  // hyphen
        0x2013,  // dash
        0x2014,  // dash
        0x2015,  // dash
        0x2016,  // big parallel
        0x2020,  // dagger
        0x2021,  // double dagger
        0x2026,  // ellipsis
        0x2030,  // perthousand
        0x2032,  // minute
        0x2033,  // second
        0x2038,  // caret
        0x2040,  // sequence concatenation
        0x20cd,  // currency symbol
      ) ++
      (0x2100 to 0x214f) ++  // Letterlike Symbols
      (0x2190 to 0x21ff) ++  // Arrows
      (0x2200 to 0x22ff) ++  // Mathematical Operators
      (0x2300 to 0x23ff) ++  // Miscellaneous Technical
      Seq(
        0x2423,  // graphic for space
        0x2500,  // box drawing
        0x2501,  // box drawing
        0x2508,  // box drawing
        0x2509,  // box drawing
        0x2550,  // box drawing
      ) ++
      (0x25a0 to 0x25ff) ++  // Geometric Shapes
      Seq(
        0x261b,  // ACTION
        0x2660,  // spade suit
        0x2661,  // heart suit
        0x2662,  // diamond suit
        0x2663,  // club suit
        0x266d,  // musical flat
        0x266e,  // musical natural
        0x266f,  // musical sharp
        0x2713,  // check mark
        0x2717,  // ballot X
        0x2756,  // UNDEFINED
        0x2759,  // BOLD
        0x27a7,  // DESCR
        0x27e6,  // left white square bracket
        0x27e7,  // right white square bracket
        0x27e8,  // left angle bracket
        0x27e9,  // right angle bracket
        0x27ea,  // left double angle bracket
        0x27eb,  // right double angle bracket
      ) ++
      (0x27f0 to 0x27ff) ++  // Supplemental Arrows-A
      (0x2900 to 0x297f) ++  // Supplemental Arrows-B
      (0x2980 to 0x29ff) ++  // Miscellaneous Mathematical Symbols-B
      (0x2a00 to 0x2aff) ++  // Supplemental Mathematical Operators
      Seq(0x2b1a) ++  // VERBATIM
      (0x1d400 to 0x1d7ff) ++  // Mathematical Alphanumeric Symbols
      Seq(
        0x1f310,  // globe with meridians (Symbola font)
        0x1f4d3,  // notebook (Symbola font)
        0x1f5c0,  // folder (Symbola font)
        0x1f5cf,  // page (Symbola font)
      )

    def isabelle_math_font: Seq[Int] =
      (0x21 to 0x2f) ++  // bang .. slash
      (0x3a to 0x40) ++  // colon .. atsign
      (0x5b to 0x5f) ++  // leftbracket .. underscore
      (0x7b to 0x7e) ++  // leftbrace .. tilde
      Seq(
        0xa9,  // copyright
        0xae,  // registered
      )

    val vacuous_font: Seq[Int] =
      Seq(0x3c)  // "<" as template
  }

  /* font families */

  sealed case class Family(
    plain: String = "",
    bold: String = "",
    italic: String = "",
    bold_italic: String = ""
  ) {
    val fonts: List[String] =
      proper_string(plain).toList :::
      proper_string(bold).toList :::
      proper_string(italic).toList :::
      proper_string(bold_italic).toList

    def get(index: Int): String = fonts(index % fonts.length)
  }

  object Family {
    def isabelle_symbols: Family =
      Family(
        plain = "IsabelleSymbols.sfd",
        bold = "IsabelleSymbolsBold.sfd")

    def deja_vu_sans_mono: Family =
      Family(
        plain = "DejaVuSansMono.ttf",
        bold = "DejaVuSansMono-Bold.ttf",
        italic = "DejaVuSansMono-Oblique.ttf",
        bold_italic = "DejaVuSansMono-BoldOblique.ttf")

    def deja_vu_sans: Family =
      Family(
        plain = "DejaVuSans.ttf",
        bold = "DejaVuSans-Bold.ttf",
        italic = "DejaVuSans-Oblique.ttf",
        bold_italic = "DejaVuSans-BoldOblique.ttf")

    def deja_vu_serif: Family =
      Family(
        plain = "DejaVuSerif.ttf",
        bold = "DejaVuSerif-Bold.ttf",
        italic = "DejaVuSerif-Italic.ttf",
        bold_italic = "DejaVuSerif-BoldItalic.ttf")

    def vacuous: Family = Family(plain = "Vacuous.sfd")
  }

  /* hinting */

  // see https://www.freetype.org/ttfautohint/doc/ttfautohint.html
  private def auto_hint(source: Path, target: Path): Unit = {
    Isabelle_System.bash("ttfautohint -i " +
      File.bash_path(source) + " " + File.bash_path(target)).check
  }

  private def make_path(hinted: Boolean = false): Path =
    if (hinted) Path.basic("ttf-hinted") else Path.basic("ttf")

  private val hinting = List(false, true)

  /* build fonts */

  private def find_file(dirs: List[Path], name: String): Path = {
    val path = Path.explode(name)
    dirs.collectFirst({ case dir if (dir + path).is_file => dir + path }) match {
      case Some(file) => file
      case None =>
        error(cat_lines(
          ("Failed to find font file " + path + " in directories:") ::
            dirs.map(dir => " " + dir.toString)))
    }
  }

  val default_download_url =
    "https://github.com/dejavu-fonts/dejavu-fonts/releases/download/version_2_37/dejavu-fonts-ttf-2.37.zip"

  val default_sources: List[Family] =
    List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif)

  def build_fonts(
    download_url: String = default_download_url,
    target_dir: Path = Path.current,
    target_prefix: String = "Isabelle",
    sources: List[Family] = default_sources,
    progress: Progress = new Progress
  ): Unit = {
    Isabelle_System.require_command("ttfautohint")

    Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
      Isabelle_System.with_tmp_dir("download") { download_dir =>

        /* download */

        Isabelle_System.download_file(download_url, download_file, progress = progress)
        Isabelle_System.extract(download_file, download_dir)

        val dejavu_dir = File.get_dir(download_dir, title = download_url) + Path.basic("ttf")

        /* component */

        val component_date = Date.Format.alt_date(Date.now())
        val component_name = "isabelle_fonts-" + component_date
        val component_dir =
          Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)

        for (hinted <- hinting) {
          Isabelle_System.make_directory(component_dir.path + make_path(hinted = hinted))
        }

        val font_dirs = List(dejavu_dir, Path.explode("~~/Admin/isabelle_fonts"))
        for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)

        // Isabelle fonts

        val fonts =
          for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex }
          yield {
            val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index))

            val source_file = find_file(font_dirs, source_font)
            val source_names = Fontforge.font_names(source_file)

            val font_names = source_names.update(prefix = target_prefix, version = component_date)

            Isabelle_System.with_tmp_file("font", "ttf") { tmp_file =>
              for (hinted <- hinting) {
                val font_file = component_dir.path + make_path(hinted = hinted) + font_names.ttf
                progress.echo("Font " + font_file + " ...")

                if (hinted) auto_hint(source_file, tmp_file)
                else Isabelle_System.copy_file(source_file, tmp_file)

                Fontforge.execute(
                  Fontforge.commands(
                    Fontforge.open(isabelle_file),
                    Fontforge.select(Range.isabelle_font),
                    Fontforge.copy,
                    Fontforge.close,

                    Fontforge.open(tmp_file),
                    Fontforge.select(Range.base_font),
                    Fontforge.select_invert,
                    Fontforge.clear,
                    Fontforge.select(Range.isabelle_font),
                    Fontforge.paste,

                    font_names.set,
                    Fontforge.generate(font_file),
                    Fontforge.close)
                ).check
              }
            }

            (font_names.ttf, index)
          }

        // Vacuous font

        {
          val vacuous_file = find_file(font_dirs, Family.vacuous.get(0))

          val font_dir = component_dir.path + make_path()
          val font_names = Fontforge.font_names(vacuous_file)
          val font_file = font_dir + font_names.ttf

          progress.echo("Font " + font_file + " ...")

          val domain =
            (for ((name, index) <- fonts if index == 0)
              yield Fontforge.font_domain(font_dir + name))
            .flatten.distinct.sorted

          Fontforge.execute(
            Fontforge.commands(
              Fontforge.open(vacuous_file),
              Fontforge.select(Range.vacuous_font),
              Fontforge.copy) +

            domain.map(code =>
                Fontforge.commands(
                  Fontforge.select(Seq(code)),
                  Fontforge.paste))
              .mkString("\n", "\n", "\n") +

            Fontforge.commands(
              Fontforge.generate(font_file),
              Fontforge.close)
          ).check
        }

        /* settings */

        def make_settings(hinted: Boolean = false): String =
          "\n isabelle_fonts \\\n" +
          (for ((ttf, _) <- fonts) yield
            """ "$COMPONENT/""" + make_path(hinted = hinted).file_name + "/" + ttf.file_name + "\"")
          .mkString(" \\\n")

        component_dir.write_settings("""
if grep "isabelle_fonts_hinted.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
then""" + make_settings() + """
else""" + make_settings(hinted = true) + """
fi

isabelle_fonts_hidden "$COMPONENT/""" + make_path().file_name + """/Vacuous.ttf"
""")

        /* README */

        Isabelle_System.copy_file(
          Path.explode("~~/Admin/isabelle_fonts/README"), component_dir.README)
      }
    }
  }

  /* Isabelle tool wrapper */

  val isabelle_tool =
    Isabelle_Tool("component_fonts", "construct Isabelle fonts", Scala_Project.here,
      { args =>
        var target_dir = Path.current
        var download_url = default_download_url

        val getopts = Getopts("""
Usage: isabelle component_fonts [OPTIONS]

  Options are:
    -D DIR       target directory (default ".")
    -U URL       download URL (default: """" + default_download_url + """")

  Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
""",
          "D:" -> (arg => target_dir = Path.explode(arg)),
          "U:" -> (arg => download_url = arg))

        val more_args = getopts(args)
        if (more_args.nonEmpty) getopts.usage()

        val progress = new Console_Progress

        build_fonts(download_url = download_url, target_dir = target_dir, progress = progress)
      })
}

quality84%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.