# HG changeset patch
# User wenzelm
# Date 1621343875 -7200
# Node ID 1bbbaae6b5e346344e095372857912a06e9897aa
# Parent  9e1de6fb957964e8f8d870e6b781791edb79f35c
option document_logo;

diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 NEWS
--- 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:
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 etc/options
--- 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"
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Classes/document/build
--- 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"
-
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Classes/document/root.tex
--- 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}}
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Codegen/document/build
--- 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
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Codegen/document/root.tex
--- 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}}
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Corec/document/root.tex
--- 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 \\
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Datatypes/document/root.tex
--- 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, \\
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Eisbach/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Eisbach/document/root.tex
--- 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 \\
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/How_to_Prove_it/document/root.tex
--- 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
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Implementation/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Implementation/document/root.tex
--- 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
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Intro/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Intro/document/root.tex
--- 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] 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Isar_Ref/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Isar_Ref/document/root.tex
--- 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,
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/JEdit/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/JEdit/document/root.tex
--- 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}}
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Logics/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Logics/document/root.tex
--- 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 \\
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Logics_ZF/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Logics_ZF/document/root.tex
--- 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}\\
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Nitpick/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Nitpick/document/root.tex
--- 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{} \\
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Prog_Prove/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Prog_Prove/document/root.tex
--- 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
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/ROOT
--- 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]
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Sledgehammer/document/build
--- 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"
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Sledgehammer/document/root.tex
--- 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{} \\
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/System/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/System/document/root.tex
--- 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}}
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Tutorial/document/build
--- 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
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Tutorial/document/root.tex
--- 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]
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Typeclass_Hierarchy/document/build
--- 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"
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Doc/Typeclass_Hierarchy/document/root.tex
--- 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}}
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Pure/Thy/document_build.scala
--- 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)
 
diff -r 9e1de6fb9579 -r 1bbbaae6b5e3 src/Pure/Tools/logo.scala
--- 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)
     })
 }