author | wenzelm |
Fri, 23 Nov 2018 16:43:11 +0100 | |
changeset 69334 | 6b49700da068 |
parent 69333 | c889afca73a5 |
child 69335 | 76c8beaf3bab |
permissions | -rw-r--r-- |
69328 | 1 |
/* Title: Pure/Tools/fontforge.scala |
2 |
Author: Makarius |
|
3 |
||
69333 | 4 |
Support for fontforge and its scripting language: see |
5 |
/usr/share/doc/fontforge/scripting.html e.g. on Ubuntu Linux installation. |
|
69328 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
11 |
import java.io.{File => JFile} |
|
12 |
import java.util.Locale |
|
13 |
||
14 |
||
15 |
object Fontforge |
|
16 |
{ |
|
17 |
/** scripting language **/ |
|
18 |
||
19 |
type Script = String |
|
20 |
||
21 |
||
22 |
/* concrete syntax */ |
|
23 |
||
24 |
def string(s: String): Script = |
|
25 |
{ |
|
69329 | 26 |
def err(c: Char): Nothing = |
27 |
error("Bad character \\u" + String.format(Locale.ROOT, "%04x", new Integer(c)) + |
|
28 |
" in fontforge string " + quote(s)) |
|
69328 | 29 |
|
69329 | 30 |
val q = if (s.contains('"')) '\'' else '"' |
69328 | 31 |
|
32 |
def escape(c: Char): String = |
|
33 |
{ |
|
69329 | 34 |
if (c == '\u0000' || c == '\r' || c == q) err(c) |
69328 | 35 |
else if (c == '\n') "\\n" |
36 |
else if (c == '\\') "\\\\" |
|
37 |
else c.toString |
|
38 |
} |
|
39 |
||
40 |
if (s.nonEmpty && s(0) == '\\') err('\\') |
|
69329 | 41 |
s.iterator.map(escape(_)).mkString(q.toString, "", q.toString) |
69328 | 42 |
} |
43 |
||
69333 | 44 |
def file_name(path: Path): Script = string(File.standard_path(path)) |
69328 | 45 |
|
69333 | 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 **/ |
|
69328 | 76 |
|
77 |
def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result = |
|
78 |
Isabelle_System.with_tmp_file("fontforge")(script_file => |
|
79 |
{ |
|
80 |
File.write(script_file, script) |
|
81 |
Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) + |
|
82 |
" -lang=ff -script " + File.bash_path(script_file) + " " + args) |
|
83 |
}) |
|
69333 | 84 |
|
69334
6b49700da068
clarified font_domain: strict excludes e.g. space character;
wenzelm
parents:
69333
diff
changeset
|
85 |
def font_domain(path: Path, strict: Boolean = false): List[Int] = |
69333 | 86 |
{ |
87 |
val script = """ |
|
88 |
i = 0 |
|
89 |
while (i < CharCnt()) |
|
69334
6b49700da068
clarified font_domain: strict excludes e.g. space character;
wenzelm
parents:
69333
diff
changeset
|
90 |
if (""" + (if (strict) "DrawsSomething" else "WorthOutputting") + """(i)); Print(i); endif |
6b49700da068
clarified font_domain: strict excludes e.g. space character;
wenzelm
parents:
69333
diff
changeset
|
91 |
i = i + 1 |
69333 | 92 |
endloop |
93 |
""" |
|
94 |
Library.trim_split_lines(execute(open(path) + script).check.out). |
|
95 |
map(Value.Int.parse) |
|
96 |
} |
|
69328 | 97 |
} |