73399
|
1 |
/* Title: Pure/Tools/logo.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Create variants of the Isabelle logo (PDF).
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
75393
|
10 |
object Logo {
|
73399
|
11 |
/* create logo */
|
|
12 |
|
75393
|
13 |
def make_output_file(logo_name: String): Path = {
|
73723
|
14 |
val name = if (logo_name.isEmpty) "isabelle" else "isabelle_" + Word.lowercase(logo_name)
|
|
15 |
Path.explode(name).pdf
|
|
16 |
}
|
|
17 |
|
75393
|
18 |
def create_logo(logo_name: String, output_file: Path, quiet: Boolean = false): Unit = {
|
75394
|
19 |
Isabelle_System.with_tmp_file("logo", ext = "eps") { tmp_file =>
|
73399
|
20 |
val template = File.read(Path.explode("$ISABELLE_HOME/lib/logo/isabelle_any.eps"))
|
|
21 |
File.write(tmp_file, template.replace("<any>", logo_name))
|
73723
|
22 |
|
73399
|
23 |
Isabelle_System.bash(
|
|
24 |
"\"$ISABELLE_EPSTOPDF\" --filter < " + File.bash_path(tmp_file) +
|
|
25 |
" > " + File.bash_path(output_file)).check
|
76883
|
26 |
if (!quiet) Output.writeln(File.standard_path(output_file))
|
75394
|
27 |
}
|
73399
|
28 |
}
|
|
29 |
|
|
30 |
|
|
31 |
/* Isabelle tool wrapper */
|
|
32 |
|
|
33 |
val isabelle_tool =
|
75393
|
34 |
Isabelle_Tool("logo", "create variants of the Isabelle logo (PDF)", Scala_Project.here,
|
75394
|
35 |
{ args =>
|
|
36 |
var output: Option[Path] = None
|
|
37 |
var quiet = false
|
73399
|
38 |
|
75394
|
39 |
val getopts = Getopts("""
|
73399
|
40 |
Usage: isabelle logo [OPTIONS] [NAME]
|
|
41 |
|
|
42 |
Options are:
|
|
43 |
-o FILE alternative output file
|
|
44 |
-q quiet mode
|
|
45 |
|
|
46 |
Create variant NAME of the Isabelle logo as "isabelle_name.pdf".
|
|
47 |
""",
|
75394
|
48 |
"o:" -> (arg => output = Some(Path.explode(arg))),
|
|
49 |
"q" -> (_ => quiet = true))
|
73399
|
50 |
|
75394
|
51 |
val more_args = getopts(args)
|
|
52 |
val logo_name =
|
|
53 |
more_args match {
|
|
54 |
case Nil => ""
|
|
55 |
case List(name) => name
|
|
56 |
case _ => getopts.usage()
|
|
57 |
}
|
|
58 |
create_logo(logo_name, output getOrElse make_output_file(logo_name), quiet = quiet)
|
|
59 |
})
|
73399
|
60 |
}
|