# HG changeset patch
# User wenzelm
# Date 1542904477 -3600
# Node ID 4646fcb59121a746beed887eb3db10af55478953
# Parent  264b44dce6bee148236930c840ad61dafb6b21d0
support for fontforge and its scripting language;

diff -r 264b44dce6be -r 4646fcb59121 etc/settings
--- a/etc/settings	Thu Nov 22 17:34:30 2018 +0100
+++ b/etc/settings	Thu Nov 22 17:34:37 2018 +0100
@@ -162,6 +162,7 @@
 ###
 
 ISABELLE_GNUPLOT="gnuplot"
+ISABELLE_FONTFORGE="fontforge"
 
 #ISABELLE_MLTON="/usr/bin/mlton"
 #ISABELLE_SMLNJ="/usr/bin/sml"
diff -r 264b44dce6be -r 4646fcb59121 src/Pure/Tools/fontforge.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/fontforge.scala	Thu Nov 22 17:34:37 2018 +0100
@@ -0,0 +1,54 @@
+/*  Title:      Pure/Tools/fontforge.scala
+    Author:     Makarius
+
+Support for fontforge and its scripting language:
+https://github.com/fontforge/fontforge/blob/master/fontforge/scripting.c
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+import java.util.Locale
+
+
+object Fontforge
+{
+  /** scripting language **/
+
+  type Script = String
+
+
+  /* concrete syntax */
+
+  def string(s: String): Script =
+  {
+    val quote = if (s.contains('"')) '\'' else '"'
+
+    def err(c: Char): Nothing =
+      error("Bad character in fontforge string: \\u" +
+        String.format(Locale.ROOT, "%04x", new Integer(c)))
+
+    def escape(c: Char): String =
+    {
+      if (c == '\u0000' || c == '\r' || c == quote) err(c)
+      else if (c == '\n') "\\n"
+      else if (c == '\\') "\\\\"
+      else c.toString
+    }
+
+    if (s.nonEmpty && s(0) == '\\') err('\\')
+    s.iterator.map(escape(_)).mkString(quote.toString, "", quote.toString)
+  }
+
+
+  /* execute process */
+
+  def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result =
+    Isabelle_System.with_tmp_file("fontforge")(script_file =>
+    {
+      File.write(script_file, script)
+      Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) +
+        " -lang=ff -script " + File.bash_path(script_file) + " " + args)
+    })
+}
diff -r 264b44dce6be -r 4646fcb59121 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Nov 22 17:34:30 2018 +0100
+++ b/src/Pure/build-jars	Thu Nov 22 17:34:37 2018 +0100
@@ -145,6 +145,7 @@
   Tools/debugger.scala
   Tools/doc.scala
   Tools/dump.scala
+  Tools/fontforge.scala
   Tools/imports.scala
   Tools/main.scala
   Tools/mkroot.scala