--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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}{%
--- 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---}}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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>
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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
--- 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}
--- 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}
--- 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}
--- 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}
--- 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
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}
--- 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 ...
--- 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}
--- 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}
--- 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,
--- /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)
+ })
+}
--- 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
--- 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
--- 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}
--- 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}
--- 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}
--- 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}
--- 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}