src/Pure/System/isabelle_fonts.scala

clarified order;

/*  Title:      Pure/System/isabelle_system.scala
    Author:     Makarius

Fonts from the Isabelle system environment, notably the "Isabelle DejaVu"
collection.
*/

package isabelle


import java.awt.Font


object Isabelle_Fonts
{
  /* standard names */

  val mono: String = "Isabelle DejaVu Sans Mono"
  val sans: String = "Isabelle DejaVu Sans"
  val serif: String = "Isabelle DejaVu Serif"


  /* environment entries */

  object Entry
  {
    object Ordering extends scala.math.Ordering[Entry]
    {
      def compare(entry1: Entry, entry2: Entry): Int =
        entry1.family compare entry2.family match {
          case 0 => entry1.style compare entry2.style
          case ord => ord
        }
    }
  }

  sealed case class Entry(path: Path, html: Boolean = false)
  {
    def bytes: Bytes = Bytes.read(path)

    lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
    def family: String = font.getFamily
    def name: String = font.getFontName
    def style: Int =
      (if (is_bold) Font.BOLD else 0) +
      (if (is_italic) Font.ITALIC else 0)

    // educated guess for style: Font.createFont always produces Font.PLAIN
    private lazy val name_lowercase = Word.lowercase(name)
    def is_bold: Boolean =
      name_lowercase.containsSlice("bold")
    def is_italic: Boolean =
      name_lowercase.containsSlice("italic") ||
      name_lowercase.containsSlice("oblique")
  }

  def make_entries(
    getenv: String => String = Isabelle_System.getenv_strict(_),
    html: Boolean = false): List[Entry] =
  {
    Path.split(getenv("ISABELLE_FONTS")).map(Entry(_)) :::
    (if (html) Path.split(getenv("ISABELLE_FONTS_HTML")).map(Entry(_, html = true)) else Nil)
  }

  private lazy val all_fonts: List[Entry] =
    make_entries(html = true).sorted(Entry.Ordering)

  def fonts(html: Boolean = false): List[Entry] =
    if (html) all_fonts else all_fonts.filter(entry => !entry.html)
}