--- a/src/Pure/Tools/logo.scala Mon May 17 23:38:16 2021 +0200
+++ b/src/Pure/Tools/logo.scala Tue May 18 15:17:55 2021 +0200
@@ -11,12 +11,19 @@
{
/* create logo */
+ def make_output_file(logo_name: String): Path =
+ {
+ val name = if (logo_name.isEmpty) "isabelle" else "isabelle_" + Word.lowercase(logo_name)
+ Path.explode(name).pdf
+ }
+
def create_logo(logo_name: String, output_file: Path, quiet: Boolean = false): Unit =
{
Isabelle_System.with_tmp_file("logo", ext = "eps")(tmp_file =>
{
val template = File.read(Path.explode("$ISABELLE_HOME/lib/logo/isabelle_any.eps"))
File.write(tmp_file, template.replace("<any>", logo_name))
+
Isabelle_System.bash(
"\"$ISABELLE_EPSTOPDF\" --filter < " + File.bash_path(tmp_file) +
" > " + File.bash_path(output_file)).check
@@ -46,13 +53,12 @@
"q" -> (_ => quiet = true))
val more_args = getopts(args)
- val (logo_name, output_file) =
+ val logo_name =
more_args match {
- case Nil => ("", Path.explode("isabelle").pdf)
- case List(a) => (a, output.getOrElse(Path.explode("isabelle_" + Word.lowercase(a)).pdf))
+ case Nil => ""
+ case List(name) => name
case _ => getopts.usage()
}
-
- create_logo(logo_name, output_file, quiet = quiet)
+ create_logo(logo_name, output getOrElse make_output_file(logo_name), quiet = quiet)
})
}