equal
deleted
inserted
replaced
80 File.write(script_file, script) |
80 File.write(script_file, script) |
81 Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) + |
81 Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) + |
82 " -lang=ff -script " + File.bash_path(script_file) + " " + args) |
82 " -lang=ff -script " + File.bash_path(script_file) + " " + args) |
83 }) |
83 }) |
84 |
84 |
85 def font_domain(path: Path): List[Int] = |
85 def font_domain(path: Path, strict: Boolean = false): List[Int] = |
86 { |
86 { |
87 val script = """ |
87 val script = """ |
88 i = 0 |
88 i = 0 |
89 while (i < CharCnt()) |
89 while (i < CharCnt()) |
90 if (WorthOutputting(i)); Print(i); endif |
90 if (""" + (if (strict) "DrawsSomething" else "WorthOutputting") + """(i)); Print(i); endif |
91 i = i + 1 |
91 i = i + 1 |
92 endloop |
92 endloop |
93 """ |
93 """ |
94 Library.trim_split_lines(execute(open(path) + script).check.out). |
94 Library.trim_split_lines(execute(open(path) + script).check.out). |
95 map(Value.Int.parse) |
95 map(Value.Int.parse) |
96 } |
96 } |