# HG changeset patch # User wenzelm # Date 1542987012 -3600 # Node ID c889afca73a5d760daf38c13c5dc0cb47fa65fe1 # Parent 85ccc983748ce6c18ccb7ad8635fb95286feafe7 proper documentation; more operations; diff -r 85ccc983748c -r c889afca73a5 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) + } }