src/Pure/Tools/fontforge.scala
author wenzelm
Thu, 22 Nov 2018 17:34:37 +0100
changeset 69328 4646fcb59121
child 69329 8bbde4dba926
permissions -rw-r--r--
support for fontforge and its scripting language;
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
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     4
Support for fontforge and its scripting language:
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
     5
https://github.com/fontforge/fontforge/blob/master/fontforge/scripting.c
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
  {
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    26
    val quote = if (s.contains('"')) '\'' else '"'
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    27
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    28
    def err(c: Char): Nothing =
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    29
      error("Bad character in fontforge string: \\u" +
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    30
        String.format(Locale.ROOT, "%04x", new Integer(c)))
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
    {
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    34
      if (c == '\u0000' || c == '\r' || c == quote) err(c)
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('\\')
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    41
    s.iterator.map(escape(_)).mkString(quote.toString, "", quote.toString)
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
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    44
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    45
  /* execute process */
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    46
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    47
  def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result =
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    48
    Isabelle_System.with_tmp_file("fontforge")(script_file =>
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    49
    {
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    50
      File.write(script_file, script)
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    51
      Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) +
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    52
        " -lang=ff -script " + File.bash_path(script_file) + " " + args)
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    53
    })
4646fcb59121 support for fontforge and its scripting language;
wenzelm
parents:
diff changeset
    54
}