# HG changeset patch # User wenzelm # Date 1615306521 -3600 # Node ID 48569c862eb8db340c090ef28c9385f82beeb2e1 # Parent d47c8a89c6a57a6f54bc686b62f139483782e65f proper Isabelle/Scala tool --- avoid perl; diff -r d47c8a89c6a5 -r 48569c862eb8 lib/Tools/logo --- 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,,$TEXT," "$ISABELLE_HOME/lib/logo/isabelle_any.eps" | \ - "$ISABELLE_EPSTOPDF" --filter > "$OUTPUT_FILE" diff -r d47c8a89c6a5 -r 48569c862eb8 src/Doc/System/Misc.thy --- 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 \Creating instances of the Isabelle logo\ text \ - 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] -\Usage: isabelle logo [OPTIONS] [XYZ] - - Create instance XYZ of the Isabelle logo (PDF). +\Usage: isabelle logo [OPTIONS] [NAME] Options are: - -o FILE alternative output file (default "isabelle_xyx.pdf") - -q quiet mode\} + -o FILE alternative output file + -q quiet mode + + Create variant NAME of the Isabelle logo as "isabelle_name.pdf".\} - Option \<^verbatim>\-o\ specifies an alternative output file: the default is - \<^verbatim>\isabelle_\\xyz\\<^verbatim>\.pdf\ (in lower-case). + Option \<^verbatim>\-o\ provides an alternative output file, instead of the default in + the current directory: \<^verbatim>\isabelle_\\name\\<^verbatim>\.pdf\ with the lower-case version + of the given name. + \<^medskip> Option \<^verbatim>\-q\ 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). \ diff -r d47c8a89c6a5 -r 48569c862eb8 src/Pure/System/isabelle_tool.scala --- 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, diff -r d47c8a89c6a5 -r 48569c862eb8 src/Pure/Tools/logo.scala --- /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("", 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) + }) +} diff -r d47c8a89c6a5 -r 48569c862eb8 src/Pure/build-jars --- 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