# HG changeset patch
# User wenzelm
# Date 1615409728 -3600
# Node ID 603010a9e611ea70462c8b6e4a26ed4b380be867
# Parent  180981b879296c932be325a75d65633978f256bf# Parent  9939146b90ade8f91bf18ff2a746f4dc5f795d48
merged

diff -r 180981b87929 -r 603010a9e611 NEWS
--- a/NEWS	Tue Mar 09 14:20:27 2021 +0100
+++ b/NEWS	Wed Mar 10 21:55:28 2021 +0100
@@ -17,6 +17,13 @@
 in boundary cases.
 
 
+*** Document preparation ***
+
+* More accurate LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
+\guilsinglright. Minor INCOMPATIBILITY, use \usepackage[T1]{fontenc}
+(which is now also the default in "isabelle mkroot").
+
+
 *** HOL ***
 
 * Theory Multiset: dedicated predicate "multiset" is gone, use
diff -r 180981b87929 -r 603010a9e611 lib/Tools/components
--- a/lib/Tools/components	Tue Mar 09 14:20:27 2021 +0100
+++ b/lib/Tools/components	Wed Mar 10 21:55:28 2021 +0100
@@ -145,13 +145,12 @@
         type -p curl > /dev/null || fail "Cannot download files: missing curl"
         echo "Getting \"$REMOTE\""
         mkdir -p "$(dirname "$FULL_NAME")"
-        curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part" || \
-          fail "Failed to download \"$REMOTE\""
-        if perl -e "exit((stat('${FULL_NAME}.tar.gz.part'))[7] == 0 ? 0 : 1);"
+        if curl --fail --silent --location "$REMOTE" > "${FULL_NAME}.tar.gz.part"
         then
-          rm -f "${FULL_NAME}.tar.gz.part"
+          mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
         else
-          mv "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
+          rm -f "${FULL_NAME}.tar.gz.part"
+          fail "Failed to download \"$REMOTE\""
         fi
       fi
       if [ -e "${FULL_NAME}.tar.gz" ]; then
diff -r 180981b87929 -r 603010a9e611 lib/Tools/logo
--- a/lib/Tools/logo	Tue Mar 09 14:20:27 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"
diff -r 180981b87929 -r 603010a9e611 lib/Tools/ocaml_setup
--- a/lib/Tools/ocaml_setup	Tue Mar 09 14:20:27 2021 +0100
+++ b/lib/Tools/ocaml_setup	Wed Mar 10 21:55:28 2021 +0100
@@ -13,6 +13,8 @@
 then
   isabelle_opam switch create -y "$ISABELLE_OCAML_VERSION"
 else
+  mkdir -p "$ISABELLE_OPAM_ROOT"
+  cd "$ISABELLE_OPAM_ROOT"
   isabelle_opam init -y --disable-sandboxing --no-setup --compiler="$ISABELLE_OCAML_VERSION"
 fi
 
diff -r 180981b87929 -r 603010a9e611 lib/scripts/timestart.bash
--- a/lib/scripts/timestart.bash	Tue Mar 09 14:20:27 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Author: Makarius
-#
-# timestart - setup bash environment for timing.
-#
-
-TIMES_RESULT=""
-
-function get_times () {
-  local TMP="${TMPDIR:-/tmp}/get_times$$"
-  times > "$TMP"   # No pipe here!
-  TIMES_RESULT="$SECONDS $(echo $(cat "$TMP") | perl -pe 's,\d+m\d+\.\d+s \d+m\d+\.\d+s (\d+)m(\d+)\.\d+s +(\d+)m(\d+)\.\d+s, $1 * 60 + $2 + $3 * 60 + $4,e')"
-  rm -f "$TMP"
-}
-
-get_times  # sets TIMES_RESULT
diff -r 180981b87929 -r 603010a9e611 lib/scripts/timestop.bash
--- a/lib/scripts/timestop.bash	Tue Mar 09 14:20:27 2021 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Author: Makarius
-#
-# timestop - report timing based on environment (cf. timestart.bash)
-#
-
-TIMES_REPORT=""
-
-function show_times ()
-{
-  local TIMES_START="$TIMES_RESULT"
-  get_times
-  local TIMES_STOP="$TIMES_RESULT"
-  local TIME1
-  local TIME2
-  local KIND
-  for KIND in 1 2
-  do
-    local START=$(echo "$TIMES_START" | cut -d " " -f $KIND)
-    local STOP=$(echo "$TIMES_STOP" | cut -d " " -f $KIND)
-
-    local TIME=$(( $STOP - $START ))
-    eval "TIME${KIND}=$TIME"
-
-    local SECS=$(( $TIME % 60 ))
-    [ $SECS -lt 10 ] && SECS="0$SECS"
-    local MINUTES=$(( ($TIME / 60) % 60 ))
-    [ $MINUTES -lt 10 ] && MINUTES="0$MINUTES"
-    local HOURS=$(( $TIME / 3600 ))
-
-    local KIND_NAME
-    [ "$KIND" = 1 ] && KIND_NAME="elapsed time"
-    [ "$KIND" = 2 ] && KIND_NAME="cpu time"
-    local RESULT="${HOURS}:${MINUTES}:${SECS} ${KIND_NAME}"
-
-    if [ ${KIND} -eq 1 -o ${TIME} -ge 5 ]; then
-      if [ -z "$TIMES_REPORT" ]; then
-        TIMES_REPORT="$RESULT"
-      else
-        TIMES_REPORT="$TIMES_REPORT, $RESULT"
-      fi
-    fi
-  done
-  if let "$TIME1 >= 5 && $TIME2 >= 5"
-  then
-    local FACTOR=$(( $TIME2 * 100 / $TIME1 ))
-    local FACTOR1=$(( $FACTOR / 100 ))
-    local FACTOR2=$(( $FACTOR % 100 ))
-    if let "$FACTOR2 < 10"; then FACTOR2="0$FACTOR2"; fi
-    TIMES_REPORT="$TIMES_REPORT, factor ${FACTOR1}.${FACTOR2}"
-  fi
-}
-
-show_times  # sets TIMES_REPORT
-
-unset TIMES_RESULT get_times show_times
diff -r 180981b87929 -r 603010a9e611 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Tue Mar 09 14:20:27 2021 +0100
+++ b/lib/texinputs/isabelle.sty	Wed Mar 10 21:55:28 2021 +0100
@@ -112,8 +112,8 @@
 \chardef\isachartilde=`\~%
 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
-\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
-\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\def\isacartoucheopen{\isatext{\guilsinglleft}}%
+\def\isacartoucheclose{\isatext{\guilsinglright}}%
 }
 
 
@@ -205,8 +205,8 @@
 \def\isacharbar{\isamath{\mid}}%
 \def\isacharbraceright{\isamath{\}}}%
 \def\isachartilde{\isamath{{}\sp{\sim}}}%
-\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
-\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\def\isacharbackquoteopen{\isatext{\guilsinglleft}}%
+\def\isacharbackquoteclose{\isatext{\guilsinglright}}%
 }
 
 \newcommand{\isabellestyleliteral}{%
diff -r 180981b87929 -r 603010a9e611 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Tue Mar 09 14:20:27 2021 +0100
+++ b/lib/texinputs/isabellesym.sty	Wed Mar 10 21:55:28 2021 +0100
@@ -364,8 +364,8 @@
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
 \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
 \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
-\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
-\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
+\newcommand{\isasymopen}{\isatext{\guilsinglleft}}
+\newcommand{\isasymclose}{\isatext{\guilsinglright}}
 \newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}}  %requires wasysym
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
diff -r 180981b87929 -r 603010a9e611 src/CTT/document/root.tex
--- a/src/CTT/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/CTT/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[11pt,a4paper]{article}
-\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r 180981b87929 -r 603010a9e611 src/Doc/Classes/document/root.tex
--- a/src/Doc/Classes/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Classes/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[12pt,a4paper,fleqn]{article}
-\usepackage{latexsym,graphicx}
+\usepackage{graphicx}
 \usepackage{iman,extra,isar}
 \usepackage{isabelle,isabellesym}
 \usepackage{style}
diff -r 180981b87929 -r 603010a9e611 src/Doc/Codegen/document/root.tex
--- a/src/Doc/Codegen/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Codegen/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,7 +1,7 @@
 
 \documentclass[12pt,a4paper,fleqn]{article}
 \usepackage[T1]{fontenc}
-\usepackage{latexsym,graphicx}
+\usepackage{graphicx}
 \usepackage{tikz}\usetikzlibrary{shapes}\usetikzlibrary{arrows}
 \usepackage{multirow}
 \usepackage{iman,extra,isar}
diff -r 180981b87929 -r 603010a9e611 src/Doc/Corec/document/root.tex
--- a/src/Doc/Corec/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Corec/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -5,7 +5,6 @@
 \usepackage{cite}
 \usepackage{enumitem}
 \usepackage{footmisc}
-\usepackage{latexsym}
 \usepackage{graphicx}
 \usepackage{iman}
 \usepackage{extra}
diff -r 180981b87929 -r 603010a9e611 src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Datatypes/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -5,7 +5,6 @@
 \usepackage{cite}
 \usepackage{enumitem}
 \usepackage{footmisc}
-\usepackage{latexsym}
 \usepackage{graphicx}
 \usepackage{iman}
 \usepackage{extra}
diff -r 180981b87929 -r 603010a9e611 src/Doc/Eisbach/document/root.tex
--- a/src/Doc/Eisbach/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Eisbach/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,6 +1,6 @@
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage[T1]{fontenc}
-\usepackage{latexsym,graphicx}
+\usepackage{graphicx}
 \usepackage[refpage]{nomencl}
 \usepackage{iman,extra,isar,proof}
 \usepackage[nohyphen,strings]{underscore}
diff -r 180981b87929 -r 603010a9e611 src/Doc/Functions/document/root.tex
--- a/src/Doc/Functions/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Functions/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,7 +1,6 @@
-
 \documentclass[a4paper,fleqn]{article}
-
-\usepackage{latexsym,graphicx}
+\usepackage[T1]{fontenc}
+\usepackage{graphicx}
 \usepackage[refpage]{nomencl}
 \usepackage{iman,extra,isar}
 \usepackage{isabelle,isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/Doc/Implementation/document/root.tex
--- a/src/Doc/Implementation/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Implementation/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,6 +1,6 @@
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage[T1]{fontenc}
-\usepackage{latexsym,graphicx}
+\usepackage{graphicx}
 \usepackage[refpage]{nomencl}
 \usepackage{iman,extra,isar,proof}
 \usepackage[nohyphen,strings]{underscore}
diff -r 180981b87929 -r 603010a9e611 src/Doc/Isar_Ref/document/root.tex
--- a/src/Doc/Isar_Ref/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Isar_Ref/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,6 @@
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage[T1]{fontenc}
+\usepackage{textcomp}
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{wasysym}
@@ -7,8 +8,6 @@
 \usepackage{pifont}
 \usepackage[english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage{textcomp}
-\usepackage{latexsym}
 \usepackage{graphicx}
 \let\intorig=\int  %iman.sty redefines \int
 \usepackage{iman,extra,isar,proof}
diff -r 180981b87929 -r 603010a9e611 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/System/Misc.thy	Wed Mar 10 21:55:28 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>
 
 
diff -r 180981b87929 -r 603010a9e611 src/Doc/Tutorial/document/root.tex
--- a/src/Doc/Tutorial/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Doc/Tutorial/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,7 +1,7 @@
 \documentclass{article}
 \usepackage{cl2emono-modified,isabelle,isabellesym}
 \usepackage{proof,amsmath,amsfonts,amssymb}
-\usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,ttbox,comment}
+\usepackage{wasysym,verbatim,graphicx,tutorial,ttbox,comment}
 \usepackage{eurosym}
 \usepackage[english]{babel}
 \usepackage{pdfsetup}   
diff -r 180981b87929 -r 603010a9e611 src/FOL/document/root.tex
--- a/src/FOL/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/FOL/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r 180981b87929 -r 603010a9e611 src/FOL/ex/document/root.tex
--- a/src/FOL/ex/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/FOL/ex/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
-
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r 180981b87929 -r 603010a9e611 src/HOL/Algebra/document/root.tex
--- a/src/HOL/Algebra/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Algebra/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,9 +1,8 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}
-\usepackage{textcomp}
-\usepackage[utf8]{inputenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{amsmath}
 
diff -r 180981b87929 -r 603010a9e611 src/HOL/Analysis/document/root.tex
--- a/src/HOL/Analysis/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Analysis/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{book}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle}
 \usepackage{isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Auth/document/root.tex
--- a/src/HOL/Auth/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Auth/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[10pt,a4paper,twoside]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{amssymb}
 \usepackage{textcomp}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Bali/document/root.tex
--- a/src/HOL/Bali/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Bali/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
-
 \documentclass[11pt,a4paper]{book}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{latexsym}
 \usepackage{graphicx}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Cardinals/document/root.tex
--- a/src/HOL/Cardinals/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Cardinals/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 
 % this should be the last package used
diff -r 180981b87929 -r 603010a9e611 src/HOL/Complex_Analysis/document/root.tex
--- a/src/HOL/Complex_Analysis/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Complex_Analysis/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle}
 \usepackage{isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Data_Structures/document/root.tex
--- a/src/HOL/Data_Structures/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Data_Structures/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{latexsym}
 \usepackage{amssymb}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Examples/document/root.tex
--- a/src/HOL/Examples/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Examples/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,6 +1,5 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
-\usepackage[utf8]{inputenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 
diff -r 180981b87929 -r 603010a9e611 src/HOL/HOLCF/IMP/document/root.tex
--- a/src/HOL/HOLCF/IMP/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/HOLCF/IMP/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[11pt,a4paper]{article}
-\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{textcomp}
 \usepackage{pdfsetup}
diff -r 180981b87929 -r 603010a9e611 src/HOL/HOLCF/document/root.tex
--- a/src/HOL/HOLCF/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/HOLCF/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,7 +1,5 @@
-
-% HOLCF/document/root.tex
-
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{textcomp}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Hahn_Banach/document/root.tex
--- a/src/HOL/Hahn_Banach/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Hahn_Banach/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[10pt,a4paper,twoside]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Hoare/document/root.tex
--- a/src/HOL/Hoare/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Hoare/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage[english]{babel}
 \usepackage{isabelle,isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Homology/document/root.tex
--- a/src/HOL/Homology/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Homology/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{book}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle}
 \usepackage{isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/IMP/document/root.tex
--- a/src/HOL/IMP/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/IMP/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{latexsym}
 % this should be the last package used
diff -r 180981b87929 -r 603010a9e611 src/HOL/Induct/document/root.tex
--- a/src/HOL/Induct/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Induct/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{amssymb}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
diff -r 180981b87929 -r 603010a9e611 src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[11pt,a4paper]{article}
-\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 \isabellestyle{it}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Lattice/document/root.tex
--- a/src/HOL/Lattice/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Lattice/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym,pdfsetup}
 \usepackage[only,bigsqcap]{stmaryrd}
 
diff -r 180981b87929 -r 603010a9e611 src/HOL/Library/document/root.tex
--- a/src/HOL/Library/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Library/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,6 +1,6 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{ifthen}
-\usepackage[utf8]{inputenc}
 \usepackage[english]{babel}
 \usepackage{amsmath,amssymb,stmaryrd,textcomp,wasysym}
 \usepackage{isabelle,isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Matrix_LP/document/root.tex
--- a/src/HOL/Matrix_LP/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Matrix_LP/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 
 % this should be the last package used
diff -r 180981b87929 -r 603010a9e611 src/HOL/MicroJava/document/root.tex
--- a/src/HOL/MicroJava/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/MicroJava/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{book}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
 
 \urlstyle{rm}
diff -r 180981b87929 -r 603010a9e611 src/HOL/NanoJava/document/root.tex
--- a/src/HOL/NanoJava/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/NanoJava/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,latexsym,isabelle,isabellesym,latexsym,pdfsetup}
 
 \urlstyle{tt}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Nonstandard_Analysis/document/root.tex
--- a/src/HOL/Nonstandard_Analysis/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Nonstandard_Analysis/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage{amsmath,amssymb}
 \usepackage{stmaryrd}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Number_Theory/document/root.tex
--- a/src/HOL/Number_Theory/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Number_Theory/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Probability/document/root.tex
--- a/src/HOL/Probability/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Probability/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,10 +1,10 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{wasysym}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 \usepackage[english]{babel}
 
diff -r 180981b87929 -r 603010a9e611 src/HOL/Proofs/Extraction/document/root.tex
--- a/src/HOL/Proofs/Extraction/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Proofs/Extraction/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r 180981b87929 -r 603010a9e611 src/HOL/Proofs/Lambda/document/root.tex
--- a/src/HOL/Proofs/Lambda/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Proofs/Lambda/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage[english]{babel}
 \usepackage{amssymb}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Real_Asymp/Manual/document/root.tex
--- a/src/HOL/Real_Asymp/Manual/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Real_Asymp/Manual/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{amsfonts, amsmath, amssymb}
 \usepackage{railsetup}
 \usepackage{iman}
diff -r 180981b87929 -r 603010a9e611 src/HOL/SET_Protocol/document/root.tex
--- a/src/HOL/SET_Protocol/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/SET_Protocol/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[10pt,a4paper,twoside]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/SPARK/Manual/document/root.tex
--- a/src/HOL/SPARK/Manual/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/SPARK/Manual/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
 \documentclass[12pt,a4paper]{report}
-
+\usepackage[T1]{fontenc}
 \usepackage[a4paper,hscale=0.65,vscale=0.71]{geometry}
 
 \usepackage{isabelle,isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Statespace/document/root.tex
--- a/src/HOL/Statespace/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Statespace/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 % this should be the last package used
 \usepackage{pdfsetup}
diff -r 180981b87929 -r 603010a9e611 src/HOL/UNITY/document/root.tex
--- a/src/HOL/UNITY/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/UNITY/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[10pt,a4paper,twoside]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
diff -r 180981b87929 -r 603010a9e611 src/HOL/Unix/document/root.tex
--- a/src/HOL/Unix/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/Unix/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
-
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
 %for best-style documents ...
diff -r 180981b87929 -r 603010a9e611 src/HOL/document/root.tex
--- a/src/HOL/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/HOL/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,11 +1,11 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{textcomp}
 \usepackage[english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
-\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
diff -r 180981b87929 -r 603010a9e611 src/Pure/Examples/document/root.tex
--- a/src/Pure/Examples/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Pure/Examples/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,6 +1,5 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
-\usepackage[utf8]{inputenc}
 \usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
 
 \isabellestyle{literal}
diff -r 180981b87929 -r 603010a9e611 src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Wed Mar 10 21:55:28 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 180981b87929 -r 603010a9e611 src/Pure/Tools/logo.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/logo.scala	Wed Mar 10 21:55:28 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)
+    })
+}
diff -r 180981b87929 -r 603010a9e611 src/Pure/Tools/mkroot.scala
--- a/src/Pure/Tools/mkroot.scala	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Pure/Tools/mkroot.scala	Wed Mar 10 21:55:28 2021 +0100
@@ -71,6 +71,7 @@
 
       File.write(root_tex,
 """\documentclass[11pt,a4paper]{article}
+\""" + """usepackage[T1]{fontenc}
 \""" + """usepackage{isabelle,isabellesym}
 
 % further packages required for unusual symbols (see also
diff -r 180981b87929 -r 603010a9e611 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/Pure/build-jars	Wed Mar 10 21:55:28 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
diff -r 180981b87929 -r 603010a9e611 src/ZF/AC/document/root.tex
--- a/src/ZF/AC/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/ZF/AC/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle,amssymb,isabellesym}
 \usepackage{pdfsetup}\urlstyle{rm}
diff -r 180981b87929 -r 603010a9e611 src/ZF/Constructible/document/root.tex
--- a/src/ZF/Constructible/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/ZF/Constructible/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
 \usepackage{isabelle,amssymb,isabellesym}
 \usepackage{pdfsetup}\urlstyle{rm}
diff -r 180981b87929 -r 603010a9e611 src/ZF/IMP/document/root.tex
--- a/src/ZF/IMP/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/ZF/IMP/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,5 +1,5 @@
-
 \documentclass[a4wide]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r 180981b87929 -r 603010a9e611 src/ZF/Induct/document/root.tex
--- a/src/ZF/Induct/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/ZF/Induct/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,7 +1,7 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{isabelle,isabellesym}
 \usepackage{amssymb}
-\usepackage[utf8]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
diff -r 180981b87929 -r 603010a9e611 src/ZF/document/root.tex
--- a/src/ZF/document/root.tex	Tue Mar 09 14:20:27 2021 +0100
+++ b/src/ZF/document/root.tex	Wed Mar 10 21:55:28 2021 +0100
@@ -1,4 +1,5 @@
 \documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym}
 \usepackage{amssymb}
 \usepackage[english]{babel}