| author | wenzelm | 
| Sun, 16 May 2021 23:22:03 +0200 | |
| changeset 73710 | 241cfa881788 | 
| parent 71601 | 97ccf48c2f0c | 
| child 75393 | 87ebf5a50283 | 
| 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 = | 
| 71163 | 27 |       error("Bad character \\u" + String.format(Locale.ROOT, "%04x", Integer.valueOf(c)) +
 | 
| 69329 | 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('\\')
 | |
| 71601 | 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: 
69333diff
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 = | |
| 71601 | 124 | List(fontname, familyname, fullname, weight, copyright, fontversion).map(string). | 
| 69335 | 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 | } |