src/Pure/Tools/fontforge.scala
author wenzelm
Fri, 04 Jan 2019 21:49:06 +0100
changeset 69592 a80d8ec6c998
parent 69370 589896fe1df2
child 71163 b5822f4c3fde
permissions -rw-r--r--
support for isabelle update -u control_cartouches;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/fontforge.scala
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     3
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
     4
Support for fontforge and its scripting language: see
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
     5
/usr/share/doc/fontforge/scripting.html e.g. on Ubuntu Linux installation.
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     6
*/
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     7
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     8
package isabelle
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     9
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    10
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    11
import java.io.{File => JFile}
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    12
import java.util.Locale
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    13
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    14
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    15
object Fontforge
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    16
{
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    17
  /** scripting language **/
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    18
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    19
  type Script = String
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    20
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    21
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    22
  /* concrete syntax */
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    23
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    24
  def string(s: String): Script =
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    25
  {
69329
8bbde4dba926 tuned error;
wenzelm
parents: 69328
diff changeset
    26
    def err(c: Char): Nothing =
8bbde4dba926 tuned error;
wenzelm
parents: 69328
diff changeset
    27
      error("Bad character \\u" + String.format(Locale.ROOT, "%04x", new Integer(c)) +
8bbde4dba926 tuned error;
wenzelm
parents: 69328
diff changeset
    28
        " in fontforge string " + quote(s))
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    29
69329
8bbde4dba926 tuned error;
wenzelm
parents: 69328
diff changeset
    30
    val q = if (s.contains('"')) '\'' else '"'
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    31
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    32
    def escape(c: Char): String =
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    33
    {
69329
8bbde4dba926 tuned error;
wenzelm
parents: 69328
diff changeset
    34
      if (c == '\u0000' || c == '\r' || c == q) err(c)
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    35
      else if (c == '\n') "\\n"
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    36
      else if (c == '\\') "\\\\"
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    37
      else c.toString
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    38
    }
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    39
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    40
    if (s.nonEmpty && s(0) == '\\') err('\\')
69329
8bbde4dba926 tuned error;
wenzelm
parents: 69328
diff changeset
    41
    s.iterator.map(escape(_)).mkString(q.toString, "", q.toString)
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    42
  }
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    43
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    44
  def file_name(path: Path): Script = string(File.standard_path(path))
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    45
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    46
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    47
  /* commands */
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    48
69335
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    49
  def command_list(cmds: List[String]): Script = cat_lines(cmds)
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    50
  def commands(cmds: String*): Script = command_list(cmds.toList)
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    51
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    52
  // fonts
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    53
  def open(path: Path): Script = "Open(" + file_name(path) +")"
69335
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    54
  def close: Script = "Close()"
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    55
  def generate(path: Path): Script = "Generate(" + file_name(path) +")"
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    56
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    57
  // selection
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    58
  def select_all: Script = "SelectAll()"
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    59
  def select_none: Script = "SelectNone()"
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    60
  def select_invert: Script = "SelectInvert()"
69335
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    61
  def select(args: Seq[Int]): Script =
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    62
    command_list(select_none :: args.toList.map(code => "SelectMoreSingletons(" + code + ")"))
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    63
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    64
  def clear: Script = "Clear()"
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    65
  def copy: Script = "Copy()"
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    66
  def paste: Script = "Paste()"
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    67
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    68
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    69
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    70
  /** execute fontforge program **/
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    71
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    72
  def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result =
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    73
    Isabelle_System.with_tmp_file("fontforge")(script_file =>
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    74
    {
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    75
      File.write(script_file, script)
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    76
      Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) +
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    77
        " -lang=ff -script " + File.bash_path(script_file) + " " + args)
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    78
    })
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    79
69334
6b49700da068 clarified font_domain: strict excludes e.g. space character;
wenzelm
parents: 69333
diff changeset
    80
  def font_domain(path: Path, strict: Boolean = false): List[Int] =
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
    81
  {
69335
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    82
    val script =
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    83
      commands(
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    84
        open(path),
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    85
        "i = 0",
69370
589896fe1df2 more robust: enforce Unicode range;
wenzelm
parents: 69335
diff changeset
    86
        "while (i < CharCnt() && i < 0x110000)",
69335
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    87
        "  if (" + (if (strict) "DrawsSomething" else "WorthOutputting") + "(i)); Print(i); endif",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    88
        "  i = i + 1",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    89
        "endloop",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    90
        close)
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    91
    Library.trim_split_lines(execute(script).check.out).map(Value.Int.parse)
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    92
  }
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    93
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    94
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    95
  /* font names */
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    96
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    97
  sealed case class Font_Names(
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    98
    fontname: String = "",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
    99
    familyname: String = "",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   100
    fullname: String = "",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   101
    weight: String = "",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   102
    copyright: String = "",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   103
    fontversion: String = "")
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   104
  {
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   105
    override def toString: String = fontname
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   106
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   107
    def ttf: Path = Path.explode(fontname).ext("ttf")
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   108
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   109
    def update(prefix: String = "", version: String = ""): Font_Names =
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   110
    {
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   111
      val fontversion1 = proper_string(version) getOrElse fontversion
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   112
      if (prefix == "") copy(fontversion = fontversion1)
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   113
      else {
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   114
        copy(fontname = prefix + fontname,
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   115
          familyname = prefix + " " + familyname,
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   116
          fullname = prefix + " " + fullname,
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   117
          weight = weight,
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   118
          copyright = copyright,
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   119
          fontversion = fontversion1)
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   120
      }
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   121
    }
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   122
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   123
    def set: Script =
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   124
      List(fontname, familyname, fullname, weight, copyright, fontversion).map(string(_)).
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   125
        mkString("SetFontNames(", ",", ")")
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   126
  }
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   127
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   128
  def font_names(path: Path): Font_Names =
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   129
  {
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   130
    val script =
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   131
      commands(
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   132
        open(path),
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   133
        "Print($fontname)",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   134
        "Print($familyname)",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   135
        "Print($fullname)",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   136
        "Print($weight)",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   137
        "Print($fontversion)",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   138
        "Print($copyright)",
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   139
        close)
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   140
    Library.trim_split_lines(execute(script).check.out) match {
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   141
      case fontname :: familyname :: fullname :: weight :: fontversion :: copyright =>
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   142
        Font_Names(fontname, familyname, fullname, weight, cat_lines(copyright), fontversion)
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   143
      case res => error(cat_lines("Bad font names: " :: res))
76c8beaf3bab more operations;
wenzelm
parents: 69334
diff changeset
   144
    }
69333
c889afca73a5 proper documentation;
wenzelm
parents: 69329
diff changeset
   145
  }
69328
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
   146
}