--- a/lib/Tools/logo Tue Mar 09 11:50:21 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: create an instance of the Isabelle logo (PDF)
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [XYZ]"
- echo
- echo " Create instance XYZ of the Isabelle logo (PDF)."
- echo
- echo " Options are:"
- echo " -o FILE alternative output file (default \"isabelle_xyx.pdf\")"
- echo " -q quiet mode"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-OUTPUT_FILE=""
-QUIET=""
-
-while getopts "o:q" OPT
-do
- case "$OPT" in
- o)
- OUTPUT_FILE="$OPTARG"
- ;;
- q)
- QUIET=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-TEXT=""
-[ "$#" -ge 1 ] && { TEXT="$1"; shift; }
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-if [ -z "$OUTPUT_FILE" ]; then
- OUTPUT_NAME="$(echo "$TEXT" | tr A-Z a-z)"
- if [ -z "$OUTPUT_NAME" ]; then
- OUTPUT_FILE="isabelle.pdf"
- else
- OUTPUT_FILE="isabelle_${OUTPUT_NAME}.pdf"
- fi
-fi
-
-[ -z "$QUIET" ] && echo "$OUTPUT_FILE" >&2
-perl -p -e "s,<any>,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \
- "$ISABELLE_EPSTOPDF" --filter > "$OUTPUT_FILE"
--- a/src/Doc/System/Misc.thy Tue Mar 09 11:50:21 2021 +0100
+++ b/src/Doc/System/Misc.thy Tue Mar 09 17:15:21 2021 +0100
@@ -332,25 +332,29 @@
section \<open>Creating instances of the Isabelle logo\<close>
text \<open>
- The @{tool_def logo} tool creates instances of the generic Isabelle logo,
- for inclusion in PDF{\LaTeX} documents.
+ The @{tool_def logo} tool creates variants of the Isabelle logo, for
+ inclusion in PDF{\LaTeX} documents.
+
@{verbatim [display]
-\<open>Usage: isabelle logo [OPTIONS] [XYZ]
-
- Create instance XYZ of the Isabelle logo (PDF).
+\<open>Usage: isabelle logo [OPTIONS] [NAME]
Options are:
- -o FILE alternative output file (default "isabelle_xyx.pdf")
- -q quiet mode\<close>}
+ -o FILE alternative output file
+ -q quiet mode
+
+ Create variant NAME of the Isabelle logo as "isabelle_name.pdf".\<close>}
- Option \<^verbatim>\<open>-o\<close> specifies an alternative output file: the default is
- \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close>\<^verbatim>\<open>.pdf\<close> (in lower-case).
+ Option \<^verbatim>\<open>-o\<close> provides an alternative output file, instead of the default in
+ the current directory: \<^verbatim>\<open>isabelle_\<close>\<open>name\<close>\<^verbatim>\<open>.pdf\<close> with the lower-case version
+ of the given name.
+ \<^medskip>
Option \<^verbatim>\<open>-q\<close> omits printing of the resulting output file name.
\<^medskip>
Implementors of Isabelle tools and applications are encouraged to make
- derived Isabelle logos for their own projects using this template.
+ derived Isabelle logos for their own projects using this template. The
+ license is the same as for the regular Isabelle distribution (BSD).
\<close>
--- a/src/Pure/System/isabelle_tool.scala Tue Mar 09 11:50:21 2021 +0100
+++ b/src/Pure/System/isabelle_tool.scala Tue Mar 09 17:15:21 2021 +0100
@@ -192,6 +192,7 @@
ML_Process.isabelle_tool,
Mercurial.isabelle_tool,
Mkroot.isabelle_tool,
+ Logo.isabelle_tool,
Options.isabelle_tool,
Phabricator.isabelle_tool1,
Phabricator.isabelle_tool2,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/logo.scala Tue Mar 09 17:15:21 2021 +0100
@@ -0,0 +1,58 @@
+/* Title: Pure/Tools/logo.scala
+ Author: Makarius
+
+Create variants of the Isabelle logo (PDF).
+*/
+
+package isabelle
+
+
+object Logo
+{
+ /* create logo */
+
+ 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
+ if (!quiet) Output.writeln(output_file.expand.implode)
+ })
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("logo", "create variants of the Isabelle logo (PDF)", Scala_Project.here, args =>
+ {
+ var output: Option[Path] = None
+ var quiet = false
+
+ val getopts = Getopts("""
+Usage: isabelle logo [OPTIONS] [NAME]
+
+ Options are:
+ -o FILE alternative output file
+ -q quiet mode
+
+ Create variant NAME of the Isabelle logo as "isabelle_name.pdf".
+""",
+ "o:" -> (arg => output = Some(Path.explode(arg))),
+ "q" -> (_ => quiet = true))
+
+ val more_args = getopts(args)
+ val (logo_name, output_file) =
+ more_args match {
+ case Nil => ("", Path.explode("isabelle").pdf)
+ case List(a) => (a, output.getOrElse(Path.explode("isabelle_" + Word.lowercase(a)).pdf))
+ case _ => getopts.usage()
+ }
+
+ create_logo(logo_name, output_file, quiet = quiet)
+ })
+}
--- a/src/Pure/build-jars Tue Mar 09 11:50:21 2021 +0100
+++ b/src/Pure/build-jars Tue Mar 09 17:15:21 2021 +0100
@@ -170,6 +170,7 @@
src/Pure/Tools/dump.scala
src/Pure/Tools/fontforge.scala
src/Pure/Tools/java_monitor.scala
+ src/Pure/Tools/logo.scala
src/Pure/Tools/main.scala
src/Pure/Tools/mkroot.scala
src/Pure/Tools/phabricator.scala