forked from leanprover/theorem_proving_in_lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
989421d
commit be3042a
Showing
13 changed files
with
12,666 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,216 @@ | ||
| % \begin{macrocode} | ||
| %<!COPYRIGHT> | ||
| \ProvidesPackage{adjcalc}[% | ||
| %<!DATE> | ||
| %<!VERSION> | ||
| %<*DRIVER> | ||
| 2099/01/01 develop | ||
| %</DRIVER> | ||
| Provides advanced setlength with multiple back-ends (calc, etex, pgfmath)] | ||
| % \end{macrocode} | ||
| % | ||
| % | ||
| % \begin{macrocode} | ||
| \RequirePackage{xkeyval} | ||
| % \end{macrocode} | ||
| % | ||
| % | ||
| % Use e-TeX by default if available, otherwise the \pkg{calc} package. | ||
| % \begin{macrocode} | ||
| \def\adjcalc@atend{% | ||
| \begingroup | ||
| \expandafter\ifx\csname glueexpr\endcsname\relax | ||
| \endgroup | ||
| \RequirePackage{calc}% | ||
| \adjcalc@calc | ||
| \def\adjcalc@etex{\PackageError{adjcalc}{e-TeX not available for current compiler!}}% | ||
| \else | ||
| \endgroup | ||
| \adjcalc@etex | ||
| \fi | ||
| } | ||
| % \end{macrocode} | ||
| % | ||
| % Initial definitions for the package options. This macros are later redefined because the same keys | ||
| % can be used as macro options. | ||
| % \begin{macrocode} | ||
| \def\adjcalc@pgfmath{\AtEndOfPackage{\RequirePackage{pgf}}\def\adjcalc@atend{\adjcalc@pgfmath}} | ||
| \def\adjcalc@etex{\def\adjcalc@atend{\adjcalc@etex}} | ||
| \def\adjcalc@calc{\AtEndOfPackage{\RequirePackage{calc}}\def\adjcalc@atend{\adjcalc@calc}} | ||
| \def\adjcalc@overwrite{\AtEndOfPackage{\adjcalc@overwrite}} | ||
| % \end{macrocode} | ||
| % | ||
| % The initial default unit is `|bp|' like for \pkg{graphicx}. | ||
| % \begin{macrocode} | ||
| \def\adjcalc@defaultunit{bp}% | ||
| % \end{macrocode} | ||
| % | ||
| % | ||
| % Options: | ||
| % \begin{macrocode} | ||
| \DeclareOptionX<adjcalc>{pgfmath}{\adjcalc@pgfmath} | ||
| \DeclareOptionX<adjcalc>{etex}{\adjcalc@etex} | ||
| \DeclareOptionX<adjcalc>{calc}{\adjcalc@calc} | ||
| \DeclareOptionX<adjcalc>{none}{% | ||
| \let\adjcalc@atend\relax | ||
| \let\adjcalc@overwrite\relax | ||
| \def\adjsetlength{\setlength}% | ||
| \def\adjaddtolength{\addtolength}% | ||
| \def\adjsetcounter{\setcounter}% | ||
| \def\adjaddtocounter{\addtocounter}% | ||
| } | ||
| \DeclareOptionX<adjcalc>{overwrite}{\adjcalc@overwrite} | ||
| \DeclareOptionX<adjcalc>{defaultunit}[bp]{% | ||
| \begingroup | ||
| \def\@tempa{#1}% | ||
| \def\@tempb{none}% | ||
| \ifx\@tempa\@tempb% 'none': | ||
| \endgroup | ||
| \def\adjsetlengthdefault{\adjsetlength}% | ||
| \else | ||
| \ifx\@tempb\adjcalc@defaultunit | ||
| \endgroup | ||
| % was 'none' before | ||
| \let\adjsetlengthdefault\adjsetlengthdefault@ | ||
| \else | ||
| \endgroup | ||
| \fi | ||
| \fi | ||
| \def\adjcalc@defaultunit{#1}% | ||
| } | ||
| \ProcessOptionsX*<adjcalc> | ||
| \disable@keys{adjcalc}{none} | ||
| % \end{macrocode} | ||
| % | ||
| % | ||
| % \begin{macro}{\adjcalcset} | ||
| % User level settings macro. | ||
| % \begin{macrocode} | ||
| \def\adjcalcset{% | ||
| \setkeys{adjcalc}% | ||
| } | ||
| % \end{macrocode} | ||
| % \end{macro} | ||
| % | ||
| % | ||
| % \begin{macro}{\adjcalc@etex} | ||
| % \begin{macrocode} | ||
| \def\adjcalc@etex{% | ||
| \protected\def\adjsetlength##1##2{% | ||
| ##1=\glueexpr(##2)\relax | ||
| }% | ||
| \protected\def\adjaddtolength##1##2{% | ||
| \advance##1 by \glueexpr(##2)\relax | ||
| }% | ||
| \protected\def\adjsetcounter##1##2{% | ||
| \@ifundefined{c@##1}% | ||
| {\@nocounterr{##1}}% | ||
| {\global\csname c@##1\endcsname\numexpr(##2)\relax}% | ||
| }% | ||
| \protected\def\adjaddtocounter##1##2{% | ||
| \@ifundefined{c@##1}% | ||
| {\@nocounterr{##1}}% | ||
| {\global\advance\csname c@##1\endcsname\numexpr(##2)\relax}% | ||
| }% | ||
| \def\adjsetlengthdefault@##1##2{% | ||
| \@defaultunits##1=\glueexpr##2 \adjcalc@defaultunit\relax\@nnil | ||
| }% | ||
| \let\adjsetlengthdefault\adjsetlengthdefault@ | ||
| } | ||
| % \end{macrocode} | ||
| % \end{macro} | ||
| % | ||
| % \begin{macrocode} | ||
| \newif\if@adjcalc@needsdefault | ||
| % \end{macrocode} | ||
| % | ||
| % | ||
| % \begin{macro}{\adjcalc@calc} | ||
| % This uses the underlying (re-)definitions of the normal macros (\Macro\setlength, ...) done by the \pkg{calc} package. | ||
| % This allows to locally redefine \Macro\setlength to call \Macro\adjsetlength, etc., without causing an infinite loop. | ||
| % \begin{macrocode} | ||
| \def\adjcalc@calc{% | ||
| \DeclareRobustCommand\adjsetlength{\calc@assign@skip}% | ||
| \DeclareRobustCommand\adjaddtolength[1]{\calc@assign@skip{\advance ##1}}% | ||
| \DeclareRobustCommand\adjsetcounter[2]{\@ifundefined{c@##1}{\@nocounterr{##1}}{\calc@assign@count{\global\csname c@##1\endcsname}{##2}}}% | ||
| \DeclareRobustCommand\adjaddtocounter[2]{\@ifundefined{c@##1}{\@nocounterr{##1}}{\calc@assign@count{\global\advance\csname c@##1\endcsname}{##2}}}% | ||
| \def\adjsetlengthdefault@##1##2{% | ||
| \begingroup | ||
| \def\calc@post@scan####1!{% | ||
| \def\@tempa{####1}% | ||
| \ifx\@tempa\@empty | ||
| \endgroup% to end calc processing | ||
| % is number only | ||
| \global\@adjcalc@needsdefaulttrue | ||
| \else | ||
| \endgroup% to end calc processing | ||
| % full expression | ||
| \global\@adjcalc@needsdefaultfalse | ||
| \fi | ||
| }% | ||
| \calc@assign@skip{##1}{##2 \adjcalc@defaultunit}% | ||
| \endgroup | ||
| \if@adjcalc@needsdefault | ||
| ##1=##2 \adjcalc@defaultunit\relax | ||
| \else | ||
| \calc@assign@skip{##1}{##2}% | ||
| \fi | ||
| }% | ||
| \def\adjcalc@checkdefault##1\@nnil##2##3{% | ||
| \ifx\relax##1\relax\else | ||
| \calc@assign@skip{##2}{##3}% | ||
| \fi | ||
| }% | ||
| \let\adjsetlengthdefault\adjsetlengthdefault@ | ||
| } | ||
| % \end{macrocode} | ||
| % \end{macro} | ||
| % | ||
| % | ||
| % \begin{macro}{\adjcalc@pgfmath} | ||
| % \begin{macrocode} | ||
| \def\adjcalc@pgfmath{% | ||
| \DeclareRobustCommand\adjsetlength{\pgfmathsetlength}% | ||
| \DeclareRobustCommand\adjaddtolength{\pgfmathaddtolength}% | ||
| \DeclareRobustCommand\adjsetcounter{\pgfmathsetcounter}% | ||
| \DeclareRobustCommand\adjaddtocounter{\pgfmathaddtocounter}% | ||
| \def\adjsetlengthdefault@##1##2{% | ||
| \edef\pgfmathresultunitscale{1\adjcalc@defaultunit}% | ||
| \let\pgfmathpostparse\pgfmathscaleresult | ||
| \pgfmathparse{##2}% | ||
| ##1=\pgfmathresult pt\relax | ||
| }% | ||
| \let\adjsetlengthdefault\adjsetlengthdefault@ | ||
| } | ||
| % \end{macrocode} | ||
| % \end{macro} | ||
| % | ||
| % | ||
| % \begin{macro}{\adjbox@settobp} | ||
| % \begin{macrocode} | ||
| \def\adjcalc@settobp#1#2{% | ||
| \begingroup | ||
| \adjsetlength\@tempdima{#2}% | ||
| \@tempdima=0.99626\@tempdima | ||
| \edef\@tempa{\endgroup\def\noexpand#1{\strip@pt\@tempdima\space}}% | ||
| \@tempa | ||
| }% | ||
| % \end{macrocode} | ||
| % \end{macro} | ||
| % | ||
| % | ||
| % \begin{macro}{\adjcalc@overwrite} | ||
| % \begin{macrocode} | ||
| \def\adjcalc@overwrite{% | ||
| \let\setlength\adjsetlength | ||
| \let\addtolength\adjaddtolength | ||
| \let\setcounter\adjsetcounter | ||
| \let\addtocounter\adjaddtocounter | ||
| } | ||
| % \end{macrocode} | ||
| % \end{macro} | ||
| % | ||
| % Execute at-end code. | ||
| % \begin{macrocode} | ||
| \adjcalc@atend | ||
| % \end{macrocode} |
Oops, something went wrong.