39 |
39 |
40 if (s.nonEmpty && s(0) == '\\') err('\\') |
40 if (s.nonEmpty && s(0) == '\\') err('\\') |
41 s.iterator.map(escape(_)).mkString(q.toString, "", q.toString) |
41 s.iterator.map(escape(_)).mkString(q.toString, "", q.toString) |
42 } |
42 } |
43 |
43 |
|
44 def file_name(path: Path): Script = string(File.standard_path(path)) |
44 |
45 |
45 /* execute process */ |
46 |
|
47 /* commands */ |
|
48 |
|
49 // fonts |
|
50 def open(path: Path): Script = "Open(" + file_name(path) +")" |
|
51 def generate(path: Path): Script = "Generate(" + file_name(path) +")" |
|
52 def set_font_names( |
|
53 fontname: String = "", |
|
54 family: String = "", |
|
55 fullname: String = "", |
|
56 weight: String = "", |
|
57 copyright: String = "", |
|
58 fontversion: String = ""): Script = |
|
59 { |
|
60 List(fontname, family, fullname, weight, copyright, fontversion).map(string(_)). |
|
61 mkString("SetFontNames(", ",", ")") |
|
62 } |
|
63 |
|
64 // selection |
|
65 def select(args: Seq[Int]): Script = "SelectSingletons(" + args.mkString(",") + ")" |
|
66 def select_all: Script = "SelectAll()" |
|
67 def select_none: Script = "SelectNone()" |
|
68 def select_invert: Script = "SelectInvert()" |
|
69 def clear: Script = "Clear()" |
|
70 def copy: Script = "Copy()" |
|
71 def paste: Script = "Paste()" |
|
72 |
|
73 |
|
74 |
|
75 /** execute fontforge program **/ |
46 |
76 |
47 def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result = |
77 def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result = |
48 Isabelle_System.with_tmp_file("fontforge")(script_file => |
78 Isabelle_System.with_tmp_file("fontforge")(script_file => |
49 { |
79 { |
50 File.write(script_file, script) |
80 File.write(script_file, script) |
51 Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) + |
81 Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) + |
52 " -lang=ff -script " + File.bash_path(script_file) + " " + args) |
82 " -lang=ff -script " + File.bash_path(script_file) + " " + args) |
53 }) |
83 }) |
|
84 |
|
85 def font_domain(path: Path): List[Int] = |
|
86 { |
|
87 val script = """ |
|
88 i = 0 |
|
89 while (i < CharCnt()) |
|
90 if (WorthOutputting(i)); Print(i); endif |
|
91 i = i + 1 |
|
92 endloop |
|
93 """ |
|
94 Library.trim_split_lines(execute(open(path) + script).check.out). |
|
95 map(Value.Int.parse) |
|
96 } |
54 } |
97 } |