src/Pure/Tools/fontforge.scala

--- a/src/Pure/Tools/fontforge.scala	Fri Nov 23 14:50:32 2018 +0100
+++ b/src/Pure/Tools/fontforge.scala	Fri Nov 23 16:30:12 2018 +0100
@@ -1,8 +1,8 @@
 /*  Title:      Pure/Tools/fontforge.scala
     Author:     Makarius
 
-Support for fontforge and its scripting language:
-https://github.com/fontforge/fontforge/blob/master/fontforge/scripting.c
+Support for fontforge and its scripting language: see
+/usr/share/doc/fontforge/scripting.html e.g. on Ubuntu Linux installation.
 */
 
 package isabelle
@@ -41,8 +41,38 @@
     s.iterator.map(escape(_)).mkString(q.toString, "", q.toString)
   }
 
+  def file_name(path: Path): Script = string(File.standard_path(path))
 
-  /* execute process */
+
+  /* commands */
+
+  // fonts
+  def open(path: Path): Script = "Open(" + file_name(path) +")"
+  def generate(path: Path): Script = "Generate(" + file_name(path) +")"
+  def set_font_names(
+    fontname: String = "",
+    family: String = "",
+    fullname: String = "",
+    weight: String = "",
+    copyright: String = "",
+    fontversion: String = ""): Script =
+  {
+    List(fontname, family, fullname, weight, copyright, fontversion).map(string(_)).
+      mkString("SetFontNames(", ",", ")")
+  }
+
+  // selection
+  def select(args: Seq[Int]): Script = "SelectSingletons(" + args.mkString(",") + ")"
+  def select_all: Script = "SelectAll()"
+  def select_none: Script = "SelectNone()"
+  def select_invert: Script = "SelectInvert()"
+  def clear: Script = "Clear()"
+  def copy: Script = "Copy()"
+  def paste: Script = "Paste()"
+
+
+
+  /** execute fontforge program **/
 
   def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result =
     Isabelle_System.with_tmp_file("fontforge")(script_file =>
@@ -51,4 +81,17 @@
       Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) +
         " -lang=ff -script " + File.bash_path(script_file) + " " + args)
     })
+
+  def font_domain(path: Path): List[Int] =
+  {
+    val script = """
+i = 0
+while (i < CharCnt())
+if (WorthOutputting(i)); Print(i); endif
+i = i + 1
+endloop
+"""
+    Library.trim_split_lines(execute(open(path) + script).check.out).
+      map(Value.Int.parse)
+  }
 }