author | wenzelm |
Fri, 04 Jan 2019 21:49:06 +0100 | |
changeset 69592 | a80d8ec6c998 |
parent 69370 | 589896fe1df2 |
child 71163 | b5822f4c3fde |
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 |
||
69335 | 49 |
def command_list(cmds: List[String]): Script = cat_lines(cmds) |
50 |
def commands(cmds: String*): Script = command_list(cmds.toList) |
|
51 |
||
69333 | 52 |
// fonts |
53 |
def open(path: Path): Script = "Open(" + file_name(path) +")" |
|
69335 | 54 |
def close: Script = "Close()" |
69333 | 55 |
def generate(path: Path): Script = "Generate(" + file_name(path) +")" |
56 |
||
57 |
// selection |
|
58 |
def select_all: Script = "SelectAll()" |
|
59 |
def select_none: Script = "SelectNone()" |
|
60 |
def select_invert: Script = "SelectInvert()" |
|
69335 | 61 |
def select(args: Seq[Int]): Script = |
62 |
command_list(select_none :: args.toList.map(code => "SelectMoreSingletons(" + code + ")")) |
|
63 |
||
69333 | 64 |
def clear: Script = "Clear()" |
65 |
def copy: Script = "Copy()" |
|
66 |
def paste: Script = "Paste()" |
|
67 |
||
68 |
||
69 |
||
70 |
/** execute fontforge program **/ |
|
69328 | 71 |
|
72 |
def execute(script: Script, args: String = "", cwd: JFile = null): Process_Result = |
|
73 |
Isabelle_System.with_tmp_file("fontforge")(script_file => |
|
74 |
{ |
|
75 |
File.write(script_file, script) |
|
76 |
Isabelle_System.bash(File.bash_path(Path.explode("$ISABELLE_FONTFORGE")) + |
|
77 |
" -lang=ff -script " + File.bash_path(script_file) + " " + args) |
|
78 |
}) |
|
69333 | 79 |
|
69334
6b49700da068
clarified font_domain: strict excludes e.g. space character;
wenzelm
parents:
69333
diff
changeset
|
80 |
def font_domain(path: Path, strict: Boolean = false): List[Int] = |
69333 | 81 |
{ |
69335 | 82 |
val script = |
83 |
commands( |
|
84 |
open(path), |
|
85 |
"i = 0", |
|
69370 | 86 |
"while (i < CharCnt() && i < 0x110000)", |
69335 | 87 |
" if (" + (if (strict) "DrawsSomething" else "WorthOutputting") + "(i)); Print(i); endif", |
88 |
" i = i + 1", |
|
89 |
"endloop", |
|
90 |
close) |
|
91 |
Library.trim_split_lines(execute(script).check.out).map(Value.Int.parse) |
|
92 |
} |
|
93 |
||
94 |
||
95 |
/* font names */ |
|
96 |
||
97 |
sealed case class Font_Names( |
|
98 |
fontname: String = "", |
|
99 |
familyname: String = "", |
|
100 |
fullname: String = "", |
|
101 |
weight: String = "", |
|
102 |
copyright: String = "", |
|
103 |
fontversion: String = "") |
|
104 |
{ |
|
105 |
override def toString: String = fontname |
|
106 |
||
107 |
def ttf: Path = Path.explode(fontname).ext("ttf") |
|
108 |
||
109 |
def update(prefix: String = "", version: String = ""): Font_Names = |
|
110 |
{ |
|
111 |
val fontversion1 = proper_string(version) getOrElse fontversion |
|
112 |
if (prefix == "") copy(fontversion = fontversion1) |
|
113 |
else { |
|
114 |
copy(fontname = prefix + fontname, |
|
115 |
familyname = prefix + " " + familyname, |
|
116 |
fullname = prefix + " " + fullname, |
|
117 |
weight = weight, |
|
118 |
copyright = copyright, |
|
119 |
fontversion = fontversion1) |
|
120 |
} |
|
121 |
} |
|
122 |
||
123 |
def set: Script = |
|
124 |
List(fontname, familyname, fullname, weight, copyright, fontversion).map(string(_)). |
|
125 |
mkString("SetFontNames(", ",", ")") |
|
126 |
} |
|
127 |
||
128 |
def font_names(path: Path): Font_Names = |
|
129 |
{ |
|
130 |
val script = |
|
131 |
commands( |
|
132 |
open(path), |
|
133 |
"Print($fontname)", |
|
134 |
"Print($familyname)", |
|
135 |
"Print($fullname)", |
|
136 |
"Print($weight)", |
|
137 |
"Print($fontversion)", |
|
138 |
"Print($copyright)", |
|
139 |
close) |
|
140 |
Library.trim_split_lines(execute(script).check.out) match { |
|
141 |
case fontname :: familyname :: fullname :: weight :: fontversion :: copyright => |
|
142 |
Font_Names(fontname, familyname, fullname, weight, cat_lines(copyright), fontversion) |
|
143 |
case res => error(cat_lines("Bad font names: " :: res)) |
|
144 |
} |
|
69333 | 145 |
} |
69328 | 146 |
} |