src/Pure/Tools/fontforge.scala
changeset 69328 4646fcb59121
child 69329 8bbde4dba926
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/fontforge.scala	Thu Nov 22 17:34:37 2018 +0100
     1.3 @@ -0,0 +1,54 @@
     1.4 +/*  Title:      Pure/Tools/fontforge.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Support for fontforge and its scripting language:
     1.8 +https://github.com/fontforge/fontforge/blob/master/fontforge/scripting.c
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +import java.io.{File => JFile}
    1.15 +import java.util.Locale
    1.16 +
    1.17 +
    1.18 +object Fontforge
    1.19 +{
    1.20 +  /** scripting language **/
    1.21 +
    1.22 +  type Script = String
    1.23 +
    1.24 +
    1.25 +  /* concrete syntax */
    1.26 +
    1.27 +  def string(s: String): Script =
    1.28 +  {
    1.29 +    val quote = if (s.contains('"')) '\'' else '"'
    1.30 +
    1.31 +    def err(c: Char): Nothing =
    1.32 +      error("Bad character in fontforge string: \\u" +
    1.33 +        String.format(Locale.ROOT, "%04x", new Integer(c)))
    1.34 +
    1.35 +    def escape(c: Char): String =
    1.36 +    {
    1.37 +      if (c == '\u0000' || c == '\r' || c == quote) err(c)
    1.38 +      else if (c == '\n') "\\n"
    1.39 +      else if (c == '\\') "\\\\"
    1.40 +      else c.toString
    1.41 +    }
    1.42 +
    1.43 +    if (s.nonEmpty && s(0) == '\\') err('\\')
    1.44 +    s.iterator.map(escape(_)).mkString(quote.toString, "", quote.toString)
    1.45 +  }
    1.46 +
    1.47 +
    1.48 +  /* execute process */
    1.49 +
    1.50 +  def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result =
    1.51 +    Isabelle_System.with_tmp_file("fontforge")(script_file =>
    1.52 +    {
    1.53 +      File.write(script_file, script)
    1.54 +      Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) +
    1.55 +        " -lang=ff -script " + File.bash_path(script_file) + " " + args)
    1.56 +    })
    1.57 +}