--- a/NEWS Mon May 17 23:38:16 2021 +0200
+++ b/NEWS Tue May 18 15:17:55 2021 +0200
@@ -34,6 +34,11 @@
*** Document preparation ***
+* Option "document_logo" determines if an instance of the Isabelle logo
+should be created in the document output directory. The given string
+specifies the name of the logo variant, while "_" (underscore) refers to
+the unnamed variant. The output file name is always "isabelle_logo.pdf".
+
* Option "document_build" determines the document build engine, as
defined in Isabelle/Scala (as system service). The subsequent engines
are provided by the Isabelle distribution:
--- a/etc/options Mon May 17 23:38:16 2021 +0200
+++ b/etc/options Tue May 18 15:17:55 2021 +0200
@@ -15,6 +15,8 @@
-- "default command tags (separated by commas)"
option document_build : string = "lualatex"
-- "document build engine (e.g. lualatex, pdflatex, build)"
+option document_logo : string = ""
+ -- "generate named instance of Isabelle logo (underscore means unnamed variant)"
option thy_output_display : bool = false
-- "indicate output as multi-line display-style material"
--- a/src/Doc/Classes/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Classes/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,4 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
-
--- a/src/Doc/Classes/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Classes/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -10,7 +10,7 @@
\hyphenation{Isar}
\isadroptag{theory}
-\title{\includegraphics[scale=0.5]{isabelle_isar}
+\title{\includegraphics[scale=0.5]{isabelle_logo}
\\[4ex] Haskell-style type classes with Isabelle/Isar}
\author{\emph{Florian Haftmann}}
--- a/src/Doc/Codegen/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Codegen/document/build Tue May 18 15:17:55 2021 +0200
@@ -8,7 +8,6 @@
# ad-hoc patching of temporary path from sources
perl -i -pe 's/\{\\isachardollar\}ISABELLE\{\\isacharunderscore\}TMP\{\\isacharslash\}examples/examples/g' *.tex
-isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
# clean up afterwards
--- a/src/Doc/Codegen/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Codegen/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -13,7 +13,7 @@
\hyphenation{Isar}
\isadroptag{theory}
-\title{\includegraphics[scale=0.5]{isabelle_isar}
+\title{\includegraphics[scale=0.5]{isabelle_logo}
\\[4ex] Code generation from Isabelle/HOL theories}
\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
--- a/src/Doc/Corec/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Corec/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -48,7 +48,7 @@
\isadroptag{theory}
-\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
+\title{%\includegraphics[scale=0.5]{isabelle_logo} \\[4ex]
Defining Nonprimitively (Co)recursive Functions in Isabelle/HOL}
\author{Jasmin Christian Blanchette, Aymeric Bouzy, \\
Andreas Lochbihler, Andrei Popescu, and \\
--- a/src/Doc/Datatypes/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Datatypes/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -48,7 +48,7 @@
\isadroptag{theory}
-\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
+\title{%\includegraphics[scale=0.5]{isabelle_logo} \\[4ex]
Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}
\author{Julian Biendarra, Jasmin Blanchette, \\
Martin Desharnais, Lorenz Panny, \\
--- a/src/Doc/Eisbach/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Eisbach/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo Eisbach
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Eisbach/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Eisbach/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -16,7 +16,7 @@
\hyphenation{Eisbach}
\isadroptag{theory}
-\title{\includegraphics[scale=0.5]{isabelle_eisbach}
+\title{\includegraphics[scale=0.5]{isabelle_logo}
\\[4ex] The Eisbach User Manual}
\author{Daniel Matichuk \\
Makarius Wenzel \\
--- a/src/Doc/How_to_Prove_it/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/How_to_Prove_it/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -5,7 +5,7 @@
\begin{document}
\title{How to Prove it in Isabelle/HOL}
-%\subtitle{\includegraphics[scale=.7]{isabelle_hol}}
+%\subtitle{\includegraphics[scale=.7]{isabelle_logo}}
\author{Tobias Nipkow}
\maketitle
--- a/src/Doc/Implementation/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Implementation/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Implementation/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Implementation/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -16,7 +16,7 @@
\hyphenation{Isar}
\isadroptag{theory}
-\title{\includegraphics[scale=0.5]{isabelle_isar}
+\title{\includegraphics[scale=0.5]{isabelle_logo}
\\[4ex] The Isabelle/Isar Implementation}
\author{\emph{Makarius Wenzel} \\[3ex]
With Contributions by
--- a/src/Doc/Intro/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Intro/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Intro/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Intro/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -6,7 +6,7 @@
%prth *(\(.*\)); \1;
%{\\out \(.*\)} {\\out val it = "\1" : thm}
-\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Introduction to Isabelle}
+\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] Old Introduction to Isabelle}
\author{{\em Lawrence C. Paulson}\\
Computer Laboratory \\ University of Cambridge \\
\texttt{lcp@cl.cam.ac.uk}\\[3ex]
--- a/src/Doc/Isar_Ref/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Isar_Ref/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,7 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo Isar
./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Isar_Ref/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -23,7 +23,7 @@
\hyphenation{Isar}
\isadroptag{theory}
-\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
+\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] The Isabelle/Isar Reference Manual}
\author{\emph{Makarius Wenzel} \\[3ex]
With Contributions by
Clemens Ballarin,
--- a/src/Doc/JEdit/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/JEdit/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo jEdit
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/JEdit/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/JEdit/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -20,7 +20,7 @@
\isabellestyle{literal}
\def\isastylett{\footnotesize\tt}
-\title{\includegraphics[scale=0.5]{isabelle_jedit} \\[4ex] Isabelle/jEdit}
+\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] Isabelle/jEdit}
\author{\emph{Makarius Wenzel}}
--- a/src/Doc/Logics/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Logics/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Logics/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Logics/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -8,7 +8,7 @@
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
%% run ../sedindex logics to prepare index file
-\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics}
+\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] Isabelle's Logics}
\author{{\em Lawrence C. Paulson}\\
Computer Laboratory \\ University of Cambridge \\
--- a/src/Doc/Logics_ZF/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Logics_ZF/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo ZF
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Logics_ZF/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Logics_ZF/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -13,7 +13,7 @@
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
-\title{\includegraphics[scale=0.5]{isabelle_zf} \\[4ex]
+\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex]
Isabelle's Logics: FOL and ZF}
\author{{\em Lawrence C. Paulson}\\
--- a/src/Doc/Nitpick/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Nitpick/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo Nitpick
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Nitpick/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Nitpick/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -48,7 +48,7 @@
%\renewcommand\labelitemi{$\bullet$}
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
-\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
+\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex]
Picking Nits \\[\smallskipamount]
\Large A User's Guide to Nitpick for Isabelle/HOL}
\author{\hbox{} \\
--- a/src/Doc/Prog_Prove/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Prog_Prove/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo HOL
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Prog_Prove/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Prog_Prove/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -7,7 +7,7 @@
\begin{document}
\title{Programming and Proving in Isabelle/HOL}
-\subtitle{\includegraphics[scale=.7]{isabelle_hol}}
+\subtitle{\includegraphics[scale=.7]{isabelle_logo}}
\author{Tobias Nipkow}
\maketitle
--- a/src/Doc/ROOT Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/ROOT Tue May 18 15:17:55 2021 +0200
@@ -1,7 +1,8 @@
chapter Doc
session Classes (doc) in "Classes" = HOL +
- options [document_build = "build", document_variants = "classes", quick_and_dirty]
+ options [document_logo = "Isar", document_build = "build",
+ document_variants = "classes", quick_and_dirty]
theories [document = false] Setup
theories Classes
document_files (in "..")
@@ -17,7 +18,8 @@
"style.sty"
session Codegen (doc) in "Codegen" = HOL +
- options [document_build = "build", document_variants = "codegen", print_mode = "no_brackets,iff"]
+ options [document_logo = "Isar", document_build = "build",
+ document_variants = "codegen", print_mode = "no_brackets,iff"]
sessions
"HOL-Library"
theories [document = false]
@@ -80,7 +82,8 @@
"style.sty"
session Eisbach (doc) in "Eisbach" = HOL +
- options [document_build = "build", document_variants = "eisbach", quick_and_dirty,
+ options [document_logo = "Eisbach", document_build = "build",
+ document_variants = "eisbach", quick_and_dirty,
print_mode = "no_brackets,iff", show_question_marks = false]
sessions
"HOL-Eisbach"
@@ -131,7 +134,7 @@
"prelude.tex"
session Intro (doc) in "Intro" = Pure +
- options [document_build = "build", document_variants = "intro"]
+ options [document_logo = "_", document_build = "build", document_variants = "intro"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -147,7 +150,8 @@
"root.tex"
session Implementation (doc) in "Implementation" = HOL +
- options [document_build = "build", document_variants = "implementation", quick_and_dirty]
+ options [document_logo = "Isar", document_build = "build",
+ document_variants = "implementation", quick_and_dirty]
theories
Eq
Integration
@@ -175,7 +179,7 @@
"style.sty"
session Isar_Ref (doc) in "Isar_Ref" = HOL +
- options [document_build = "build", document_variants = "isar-ref",
+ options [document_logo = "Isar", document_build = "build", document_variants = "isar-ref",
quick_and_dirty, thy_output_source]
sessions
"HOL-Library"
@@ -212,7 +216,8 @@
"style.sty"
session JEdit (doc) in "JEdit" = HOL +
- options [document_build = "build", document_variants = "jedit", thy_output_source]
+ options [document_logo = "jEdit", document_build = "build",
+ document_variants = "jedit", thy_output_source]
theories
JEdit
document_files (in "..")
@@ -277,7 +282,7 @@
"root.tex"
session Logics (doc) in "Logics" = Pure +
- options [document_build = "build", document_variants = "logics"]
+ options [document_logo = "_", document_build = "build", document_variants = "logics"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -296,8 +301,8 @@
"syntax.tex"
session Logics_ZF (doc) in "Logics_ZF" = ZF +
- options [document_build = "build", document_variants = "logics-ZF", print_mode = "brackets",
- thy_output_source]
+ options [document_logo = "ZF", document_build = "build",
+ document_variants = "logics-ZF", print_mode = "brackets", thy_output_source]
sessions
FOL
theories
@@ -332,7 +337,7 @@
"root.tex"
session Nitpick (doc) in "Nitpick" = Pure +
- options [document_build = "build", document_variants = "nitpick"]
+ options [document_logo = "Nitpick", document_build = "build", document_variants = "nitpick"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -343,7 +348,8 @@
"root.tex"
session Prog_Prove (doc) in "Prog_Prove" = HOL +
- options [document_build = "build", document_variants = "prog-prove", show_question_marks = false]
+ options [document_logo = "HOL", document_build = "build",
+ document_variants = "prog-prove", show_question_marks = false]
theories
Basics
Bool_nat_list
@@ -366,7 +372,7 @@
"svmono.cls"
session Sledgehammer (doc) in "Sledgehammer" = Pure +
- options [document_build = "build", document_variants = "sledgehammer"]
+ options [document_logo = "S/H", document_build = "build", document_variants = "sledgehammer"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -377,7 +383,8 @@
"root.tex"
session System (doc) in "System" = Pure +
- options [document_build = "build", document_variants = "system", thy_output_source]
+ options [document_logo = "_", document_build = "build",
+ document_variants = "system", thy_output_source]
sessions
"HOL-Library"
theories
@@ -404,8 +411,8 @@
"root.tex"
session Tutorial (doc) in "Tutorial" = HOL +
- options [document_build = "build", document_variants = "tutorial",
- print_mode = "brackets", skip_proofs = false]
+ options [document_logo = "HOL", document_build = "build",
+ document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
"Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
theories [document = false]
@@ -498,7 +505,8 @@
"types0.tex"
session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL +
- options [document_build = "build", document_variants = "typeclass_hierarchy"]
+ options [document_logo = "Isar", document_build = "build",
+ document_variants = "typeclass_hierarchy"]
sessions
"HOL-Library"
theories [document = false]
--- a/src/Doc/Sledgehammer/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Sledgehammer/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,5 +5,4 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo -o isabelle_sledgehammer.pdf "S/H"
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Sledgehammer/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -54,7 +54,7 @@
%\renewcommand\labelitemi{$\bullet$}
\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
-\title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
+\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex]
Hammering Away \\[\smallskipamount]
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
\author{\hbox{} \\
--- a/src/Doc/System/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/System/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/System/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/System/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -17,7 +17,7 @@
\isabellestyle{literal}
\def\isastylett{\footnotesize\tt}
-\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle System Manual}
+\title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] The Isabelle System Manual}
\author{\emph{Makarius Wenzel}}
--- a/src/Doc/Tutorial/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Tutorial/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,7 +5,6 @@
FORMAT="$1"
VARIANT="$2"
-isabelle logo HOL
isabelle latex -o "$FORMAT"
isabelle latex -o bbl
./isa-index root
--- a/src/Doc/Tutorial/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Tutorial/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -29,7 +29,7 @@
\begin{document}
\title{
\begin{center}
-\includegraphics[scale=.8]{isabelle_hol}
+\includegraphics[scale=.8]{isabelle_logo}
\\ \vspace{0.5cm} A Proof Assistant for Higher-Order Logic
\end{center}}
\author{Tobias Nipkow \quad Lawrence C. Paulson \quad Markus Wenzel%\\[1ex]
--- a/src/Doc/Typeclass_Hierarchy/document/build Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Typeclass_Hierarchy/document/build Tue May 18 15:17:55 2021 +0200
@@ -5,6 +5,5 @@
FORMAT="$1"
VARIANT="$2"
-"$ISABELLE_TOOL" logo Isar
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Typeclass_Hierarchy/document/root.tex Mon May 17 23:38:16 2021 +0200
+++ b/src/Doc/Typeclass_Hierarchy/document/root.tex Tue May 18 15:17:55 2021 +0200
@@ -9,7 +9,7 @@
\hyphenation{Isar}
\isadroptag{theory}
-\title{\includegraphics[scale=0.5]{isabelle_isar}
+\title{\includegraphics[scale=0.5]{isabelle_logo}
\\[4ex] The {Isabelle/HOL} type-class hierarchy}
\author{\emph{Florian Haftmann}}
--- a/src/Pure/Thy/document_build.scala Mon May 17 23:38:16 2021 +0200
+++ b/src/Pure/Thy/document_build.scala Tue May 18 15:17:55 2021 +0200
@@ -156,6 +156,13 @@
def session: String = info.name
def options: Options = info.options
+ def document_logo: Option[String] =
+ options.string("document_logo") match {
+ case "" => None
+ case "_" => Some("")
+ case name => Some(name)
+ }
+
def document_build: String = options.string("document_build")
def get_engine(): Engine =
@@ -199,6 +206,18 @@
Content(path, Bytes(text))
}
+ lazy val isabelle_logo: Option[Content] =
+ {
+ document_logo.map(logo_name =>
+ Isabelle_System.with_tmp_file("logo", ext = "pdf")(tmp_path =>
+ {
+ Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
+ val path = Path.basic("isabelle_logo.pdf")
+ val bytes = Bytes.read(tmp_path)
+ Content(path, bytes)
+ }))
+ }
+
/* document directory */
@@ -222,12 +241,14 @@
val root_name1 = "root_" + doc.name
val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
- val option_digests = List(doc.print, get_engine().name).map(SHA1.digest)
- val file_digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
- val sources = SHA1.digest_set(option_digests ::: file_digests)
+ val digests1 = List(doc.print, document_logo.toString, document_build).map(SHA1.digest)
+ val digests2 = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
+ val sources = SHA1.digest_set(digests1 ::: digests2)
- /* derived material */
+ /* derived material (without SHA1 digest) */
+
+ isabelle_logo.foreach(_.write(doc_dir))
session_graph.write(doc_dir)
--- 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)
})
}