diff -r c889afca73a5 -r 6b49700da068 src/Pure/Tools/fontforge.scala --- a/src/Pure/Tools/fontforge.scala Fri Nov 23 16:30:12 2018 +0100 +++ b/src/Pure/Tools/fontforge.scala Fri Nov 23 16:43:11 2018 +0100 @@ -82,13 +82,13 @@ " -lang=ff -script " + File.bash_path(script_file) + " " + args) }) - def font_domain(path: Path): List[Int] = + def font_domain(path: Path, strict: Boolean = false): List[Int] = { val script = """ i = 0 while (i < CharCnt()) -if (WorthOutputting(i)); Print(i); endif -i = i + 1 + if (""" + (if (strict) "DrawsSomething" else "WorthOutputting") + """(i)); Print(i); endif + i = i + 1 endloop """ Library.trim_split_lines(execute(open(path) + script).check.out).