--- 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)
+ }
}