src/Pure/Tools/fontforge.scala
author wenzelm
Thu Nov 22 17:34:37 2018 +0100 (20 months ago)
changeset 69328 4646fcb59121
child 69329 8bbde4dba926
permissions -rw-r--r--
support for fontforge and its scripting language;
wenzelm@69328
     1
/*  Title:      Pure/Tools/fontforge.scala
wenzelm@69328
     2
    Author:     Makarius
wenzelm@69328
     3
wenzelm@69328
     4
Support for fontforge and its scripting language:
wenzelm@69328
     5
https://github.com/fontforge/fontforge/blob/master/fontforge/scripting.c
wenzelm@69328
     6
*/
wenzelm@69328
     7
wenzelm@69328
     8
package isabelle
wenzelm@69328
     9
wenzelm@69328
    10
wenzelm@69328
    11
import java.io.{File => JFile}
wenzelm@69328
    12
import java.util.Locale
wenzelm@69328
    13
wenzelm@69328
    14
wenzelm@69328
    15
object Fontforge
wenzelm@69328
    16
{
wenzelm@69328
    17
  /** scripting language **/
wenzelm@69328
    18
wenzelm@69328
    19
  type Script = String
wenzelm@69328
    20
wenzelm@69328
    21
wenzelm@69328
    22
  /* concrete syntax */
wenzelm@69328
    23
wenzelm@69328
    24
  def string(s: String): Script =
wenzelm@69328
    25
  {
wenzelm@69328
    26
    val quote = if (s.contains('"')) '\'' else '"'
wenzelm@69328
    27
wenzelm@69328
    28
    def err(c: Char): Nothing =
wenzelm@69328
    29
      error("Bad character in fontforge string: \\u" +
wenzelm@69328
    30
        String.format(Locale.ROOT, "%04x", new Integer(c)))
wenzelm@69328
    31
wenzelm@69328
    32
    def escape(c: Char): String =
wenzelm@69328
    33
    {
wenzelm@69328
    34
      if (c == '\u0000' || c == '\r' || c == quote) err(c)
wenzelm@69328
    35
      else if (c == '\n') "\\n"
wenzelm@69328
    36
      else if (c == '\\') "\\\\"
wenzelm@69328
    37
      else c.toString
wenzelm@69328
    38
    }
wenzelm@69328
    39
wenzelm@69328
    40
    if (s.nonEmpty && s(0) == '\\') err('\\')
wenzelm@69328
    41
    s.iterator.map(escape(_)).mkString(quote.toString, "", quote.toString)
wenzelm@69328
    42
  }
wenzelm@69328
    43
wenzelm@69328
    44
wenzelm@69328
    45
  /* execute process */
wenzelm@69328
    46
wenzelm@69328
    47
  def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result =
wenzelm@69328
    48
    Isabelle_System.with_tmp_file("fontforge")(script_file =>
wenzelm@69328
    49
    {
wenzelm@69328
    50
      File.write(script_file, script)
wenzelm@69328
    51
      Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) +
wenzelm@69328
    52
        " -lang=ff -script " + File.bash_path(script_file) + " " + args)
wenzelm@69328
    53
    })
wenzelm@69328
    54
}