products/sources/formale Sprachen/Isabelle/HOL/ex/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: lstdoc.sty   Sprache: Latech

%%
%% This is file `lstdoc.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% listings.dtx  (with options: `doc')
%% 
%% Please read the software license in listings.dtx or listings.pdf.
%%
%% (w)(c) 1996 -- 2003 Carsten Heinz and/or any other author
%% listed elsewhere in this file.
%%
%% This file is distributed under the terms of the LaTeX Project Public
%% License from CTAN archives in directory  macros/latex/base/lppl.txt.
%% Either version 1.0 or, at your option, any later version.
%%
%% Permission is granted to modify this file. If your changes are of
%% general interest, please contact the address below.
%%
%% Send comments and ideas on the package, error reports and additional
%% programming languages to <[email protected]>.
%%
\def\filedate{2003/06/21}
\def\fileversion{1.1}
\ProvidesPackage{lstdoc}
             [\filedate\space\fileversion\space(Carsten Heinz)]
\let\lstdoc@currversion\fileversion
\RequirePackage[writefile]{listings}[2002/04/01]
\newif\iffancyvrb \IfFileExists{fancyvrb.sty}{\fancyvrbtrue}{}
\newif\ifcolor \IfFileExists{color.sty}{\colortrue}{}
\newif\ifhyper \@ifundefined{pdfoutput}{}
    {\IfFileExists{hyperref.sty}{\hypertrue}{}}
\newif\ifalgorithmic \IfFileExists{algorithmic.sty}{\algorithmictrue}{}
\newif\iflgrind \IfFileExists{lgrind.sty}{\lgrindtrue}{}
\iffancyvrb \RequirePackage{fancyvrb}\fi
\ifhyper \RequirePackage[colorlinks]{hyperref}\else
    \def\href#1{\texttt}\fi
\ifcolor \RequirePackage{color}\fi
\ifalgorithmic \RequirePackage{algorithmic}\fi
\iflgrind \RequirePackage{lgrind}\fi
\RequirePackage{nameref}
\renewcommand\ref{\protect\T@ref}
\renewcommand\pageref{\protect\T@pageref}
\def\lst@BeginRemark#1{%
    \begin{quote}\topsep0pt\let\small\footnotesize\small#1:}
\def\lst@EndRemark{\end{quote}}
\newenvironment{TODO}
    {\lst@BeginRemark{To do}}{\lst@EndRemark}
\newenvironment{ALTERNATIVE}
    {\lst@BeginRemark{Alternative}}{\lst@EndRemark}
\newenvironment{REMOVED}
    {\lst@BeginRemark{Removed}}{\lst@EndRemark}
\newenvironment{OLDDEF}
    {\lst@BeginRemark{Old definition}}{\lst@EndRemark}
\def\advise{\par\list\labeladvise
    {\advance\linewidth\@totalleftmargin
     \@totalleftmargin\z@
     \@listi
     \let\small\footnotesize \small\sffamily
     \parsep \z@ \@plus\z@ \@minus\z@
     \topsep6\p@ \@plus1\p@\@minus2\p@
     \def\makelabel##1{\hss\llap{##1}}}}
\let\endadvise\endlist
\def\advisespace{\hbox{}\qquad}
\def\labeladvise{$\to$}
\newenvironment{syntax}
   {\list{}{\itemindent-\leftmargin
    \def\makelabel##1{\hss\lst@syntaxlabel##1,,,,\relax}}}
   {\endlist}
\def\lst@syntaxlabel#1,#2,#3,#4\relax{%
    \llap{\scriptsize\itshape#3}%
    \def\lst@temp{#2}%
    \expandafter\lst@syntaxlabel@\meaning\lst@temp\relax
    \rlap{\hskip-\itemindent\hskip\itemsep\hskip\linewidth
          \llap{\ttfamily\lst@temp}\hskip\labelwidth
          \def\lst@temp{#1}%
          \ifx\lst@temp\lstdoc@currversion#1\fi}}
\def\lst@syntaxlabel@#1>#2\relax
    {\edef\lst@temp{\zap@space#2 \@empty}}
\newcommand*\syntaxnewline{\newline\hbox{}\kern\labelwidth}
\newcommand*\syntaxor{\qquad or\qquad}
\newcommand*\syntaxbreak
    {\hfill\kern0pt\discretionary{}{\kern\labelwidth}{}}
\let\syntaxfill\hfill
\def\alternative#1{\lst@true \alternative@#1,\relax,}
\def\alternative@#1,{%
    \ifx\relax#1\@empty
        \expandafter\@gobble
    \else
        \ifx\@empty#1\@empty\else
            \lst@if \lst@false \else $\vert$\fi
            \textup{\texttt{#1}}%
        \fi
    \fi
    \alternative@}
\long\def\m@cro@#1#2#3{\endgroup \topsep\MacroTopsep \trivlist
  \edef\saved@macroname{\string#3}%
  \def\makelabel##1{\llap{##1}}%
  \if@inlabel
    \let\@tempa\@empty \count@\macro@cnt
    \loop \ifnum\count@>\z@
      \edef\@tempa{\@tempa\hbox{\strut}}\advance\count@\m@ne \repeat
    \edef\makelabel##1{\llap{\vtop to\baselineskip
                               {\@tempa\hbox{##1}\vss}}}%
    \advance \macro@cnt \@ne
  \else  \macro@cnt\@ne  \fi
  \edef\@tempa{\noexpand\item[%
     #1%
       \noexpand\PrintMacroName
     \else
       \expandafter\noexpand\csname Print#2Name\endcsname % MODIFIED
     \fi
     {\string#3}]}%
  \@tempa
  \global\advance\c@CodelineNo\@ne
   #1%
      \SpecialMainIndex{#3}\nobreak
      \DoNotIndex{#3}%
   \else
      \csname SpecialMain#2Index\endcsname{#3}\nobreak % MODIFIED
   \fi
  \global\advance\c@CodelineNo\m@ne
  \ignorespaces}
\def\macro{\begingroup
   \catcode`\\12
   \MakePrivateLetters \m@cro@ \iftrue {Macro}}% MODIFIED
\def\environment{\begingroup
   \catcode`\\12
   \MakePrivateLetters \m@cro@ \iffalse {Env}}% MODIFIED
\def\newdocenvironment#1#2#3#4{%
    \@namedef{#1}{#3\begingroup \catcode`\\12\relax
                  \MakePrivateLetters \m@cro@ \iffalse {#2}}%
    \@namedef{end#1}{#4\endmacro}%
    \@ifundefined{Print#2Name}{\expandafter
        \let\csname Print#2Name\endcsname\PrintMacroName}{}%
    \@ifundefined{SpecialMain#2Index}{\expandafter
        \let\csname SpecialMain#2Index\endcsname\SpecialMainIndex}{}}
\newdocenvironment{aspect}{Aspect}{}{}
\def\PrintAspectName#1{}
\def\SpecialMainAspectIndex#1{%
    \@bsphack
    \index{aspects:\levelchar\protect\aspectname{#1}\encapchar main}%
    \@esphack}
\newdocenvironment{lstkey}{Key}{}{}
\def\PrintKeyName#1{\strut\keyname{#1}\ }
\def\SpecialMainKeyIndex#1{%
    \@bsphack
    \index{keys\levelchar\protect\keyname{#1}\encapchar main}%
    \@esphack}
\newcounter{argcount}
\def\labelargcount{\texttt{\#\arabic{argcount}}\hskip\labelsep$=$}
\def\macroargs{\list\labelargcount
    {\usecounter{argcount}\leftmargin=2\leftmargin
     \parsep \z@ \@plus\z@ \@minus\z@
     \topsep4\p@ \@plus\p@ \@minus2\p@
     \itemsep\z@ \@plus\z@ \@minus\z@
     \def\makelabel##1{\hss\llap{##1}}}}
\def\endmacroargs{\endlist\@endparenv}
\lst@RequireAspects{writefile}
\newbox\lst@samplebox
\lstnewenvironment{lstsample}[3][]
    {\global\let\lst@intname\@empty
     \gdef\lst@sample{#2}%
     \setbox\lst@samplebox=\hbox\bgroup
         \setkeys{lst}{language={},style={},tabsize=4,gobble=5,%
             basicstyle=\small\ttfamily,basewidth=0.51em,point={#1}}
         #3%
         \lst@BeginAlsoWriteFile{\jobname.tmp}}
    {\lst@EndWriteFile\egroup
     \ifdim \wd\lst@samplebox>.5\linewidth
         \begin{center}%
             \hbox to\linewidth{\box\lst@samplebox\hss}%
         \end{center}%
         \lst@sampleInput
     \else
         \begin{center}%
         \begin{minipage}{0.45\linewidth}\lst@sampleInput\end{minipage}%
         \qquad
         \begin{minipage}{0.45\linewidth}%
             \hbox to\linewidth{\box\lst@samplebox\hss}%
         \end{minipage}%
         \end{center}%
     \fi}
\lst@InstallKeywords{p}{point}{pointstyle}\relax{keywordstyle}{}ld
\lstnewenvironment{lstxsample}[1][]
    {\begingroup
         \setkeys{lst}{belowskip=-\medskipamount,language={},style={},%
             tabsize=4,gobble=5,basicstyle=\small\ttfamily,%
             basewidth=0.51em,point={#1}}
         \lst@BeginAlsoWriteFile{\jobname.tmp}}
    {\endgroup
     \endgroup}
\def\lst@sampleInput{%
    \MakePercentComment\catcode`\^^M=10\relax
    \small\lst@sample
    {\setkeys{lst}{SelectCharTable=\lst@ReplaceInput{\^\^I}%
                                  {\lst@ProcessTabulator}}%
     \leavevmode \input{\jobname.tmp}}\MakePercentIgnore}
\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
                                      {1.25ex \@plus1ex \@minus.2ex}%
                                      {-1em}%
                                      {\normalfont\normalsize\bfseries}}
\def\lstref#1{\emph{\ref{#1} \nameref{#1}}}
\def\@part[#1]#2{\addcontentsline{toc}{part}{#1}%
    {\parindent\z@ \raggedright \interlinepenalty\@M
     \normalfont \huge \bfseries #2\markboth{}{}\par}%
    \nobreak\vskip 3ex\@afterheading}
\renewcommand*\l@section[2]{%
    \addpenalty\@secpenalty
    \addvspace{.25em \@plus\p@}%
    \setlength\@tempdima{1.5em}%
    \begingroup
      \parindent \z@ \rightskip \@pnumwidth
      \parfillskip -\@pnumwidth
      \leavevmode
      \advance\leftskip\@tempdima
      \hskip -\leftskip
      #1\nobreak\hfil \nobreak\hb@xt@\@pnumwidth{\hss #2}\par
    \endgroup}
\renewcommand*\l@subsection{\@dottedtocline{2}{0pt}{2.3em}}
\renewcommand*\l@subsubsection{\@dottedtocline{3}{0pt}{3.2em}}
\newcommand\ikeyname[1]{%
    \lstkeyindex{#1}{}%
    \lstaspectindex{#1}{}%
    \keyname{#1}}
\newcommand\ekeyname[1]{%
    \@bsphack
    \lstkeyindex{#1}{\encapchar usage}%
    \lstaspectindex{#1}{\encapchar usage}%
    \@esphack}
\newcommand\rkeyname[1]{%
    \@bsphack
    \lstkeyindex{#1}{\encapchar main}%
    \lstaspectindex{#1}{\encapchar main}%
    \@esphack{\rstyle\keyname{#1}}}
\newcommand\icmdname[1]{%
    \@bsphack
    \lstaspectindex{#1}{}%
    \@esphack\texttt{\string#1}}
\newcommand\rcmdname[1]{%
    \@bsphack
    \lstaspectindex{#1}{\encapchar main}%
    \@esphack\texttt{\rstyle\string#1}}
\def\lstaspectindex#1#2{%
    \global\@namedef{lstkandc@\string#1}{}%
    \@ifundefined{lstisaspect@\string#1}
        {\index{unknown\levelchar
                \protect\texttt{\protect\string\string#1}#2}}%
        {\index{\@nameuse{lstisaspect@\string#1}\levelchar
                \protect\texttt{\protect\string\string#1}#2}}%
}
\def\lstkeyindex#1#2{%
}
\def\lstisaspect[#1]#2{%
    \global\@namedef{lstaspect@#1}{#2}%
    \lst@AddTo\lst@allkeysandcmds{,#2}%
    \@for\lst@temp:=#2\do
    {\ifx\@empty\lst@temp\else
         \global\@namedef{lstisaspect@\lst@temp}{#1}%
     \fi}}
\gdef\lst@allkeysandcmds{}
\def\lstprintaspectkeysandcmds#1{%
    \lst@true
    \expandafter\@for\expandafter\lst@temp
    \expandafter:\expandafter=\csname lstaspect@#1\endcsname\do
    {\lst@if\lst@false\else, \fi \texttt{\lst@temp}}}
\def\lstcheckreference{%
   \@for\lst@temp:=\lst@allkeysandcmds\do
   {\ifx\lst@temp\@empty\else
        \@ifundefined{lstkandc@\lst@temp}
        {\typeout{\lst@temp\space not in reference guide?}}{}%
    \fi}}
\newcommand*\lst{\texttt{lst}}
\newcommand*\Cpp{C\texttt{++}}
\let\keyname\texttt
\let\keyvalue\texttt
\let\hookname\texttt
\newcommand*\aspectname[1]{{\normalfont\sffamily#1}}
\DeclareRobustCommand\packagename[1]{%
    {\leavevmode\text@command{#1}%
     \switchfontfamily\sfdefault\rmdefault
     \check@icl #1\check@icr
     \expandafter}}%
\renewcommand\packagename[1]{{\normalfont\sffamily#1}}
\def\switchfontfamily#1#2{%
    \begingroup\xdef\@gtempa{#1}\endgroup
    \ifx\f@family\@gtempa\fontfamily#2%
                    \else\fontfamily#1\fi
    \selectfont}
\ifcolor
    \definecolor{darkgreen}{rgb}{0,0.5,0}
    \def\rstyle{\color{darkgreen}}
\else
    \let\rstyle\empty
\fi
\gdef\lst@emails{}
\newcommand*\lstthanks[2]
    {#1\lst@AddTo\lst@emails{,#1,<#2>}%
     \ifx\@empty#2\@empty\typeout{Missing email for #1}\fi}
\newcommand*\lsthelper[3]
    {{\let~\ #1}%
     \lst@IfOneOf#1\relax\lst@emails
     {}{\typeout{^^JWarning: Unknown helper #1.^^J}}}
\lstdefinelanguage[doc]{Pascal}{%
  morekeywords={alfa,and,array,begin,boolean,byte,case,char,const,div,%
     do,downto,else,end,false,file,for,function,get,goto,if,in,%
     integer,label,maxint,mod,new,not,of,or,pack,packed,page,program,%
     procedure,put,read,readln,real,record,repeat,reset,rewrite,set,%
     text,then,to,true,type,unpack,until,var,while,with,write,writeln},%
  sensitive=false,%
  morecomment=[s]{(*}{*)},%
  morecomment=[s]{\{}{\}},%
  morestring=[d]{'}}
\lstdefinestyle{}
    {basicstyle={},%
     keywordstyle=\bfseries,identifierstyle={},%
     commentstyle=\itshape,stringstyle={},%
     numberstyle={},stepnumber=1,%
     pointstyle=\pointstyle}
\def\pointstyle{%
    {\let\lst@um\@empty \xdef\@gtempa{\the\lst@token}}%
    \expandafter\lstkeyindex\expandafter{\@gtempa}{}%
    \expandafter\lstaspectindex\expandafter{\@gtempa}{}%
    \rstyle}
\lstset{defaultdialect=[doc]Pascal,language=Pascal,style={}}
\def\lstscanlanguages#1#2#3{%
    \begingroup
        \def\lst@DefDriver@##1##2##3##4[##5]##6{%
           \lst@false
           \lst@lAddTo\lst@scan{##6(##5),}%
           \begingroup
           \@ifnextchar[{\lst@XDefDriver{##1}##3}{\lst@DefDriver@@##3}}%
        \def\lst@XXDefDriver[##1]{}%
        \lst@InputCatcodes
        \def\lst@dontinput{#3}%
        \let\lst@scan\@empty
        \lst@for{#2}\do{%
            \lst@IfOneOf##1\relax\lst@dontinput
                {}%
                {\InputIfFileExists{##1}{}{}}}%
        \global\let\@gtempa\lst@scan
    \endgroup
    \let#1\@gtempa}
\def\lstprintlanguages#1{%
    \def\do##1{\setbox\@tempboxa\hbox{##1\space\space}%
        \ifdim\wd\@tempboxa<.5\linewidth \wd\@tempboxa.5\linewidth
                                   \else \wd\@tempboxa\linewidth \fi
        \box\@tempboxa\allowbreak}%
    \begin{quote}
      \par\noindent
      \hyphenpenalty=\@M \rightskip=\z@\@plus\linewidth\relax
      \lst@BubbleSort#1%
      \expandafter\lst@NextLanguage#1\relax(\relax),%
    \end{quote}}
\def\lst@NextLanguage#1(#2),{%
    \ifx\relax#1\else
        \def\lst@language{#1}\def\lst@dialects{(#2),}%
        \expandafter\lst@NextLanguage@
    \fi}
\def\lst@NextLanguage@#1(#2),{%
    \def\lst@temp{#1}%
    \ifx\lst@temp\lst@language
        \lst@lAddTo\lst@dialects{(#2),}%
        \expandafter\lst@NextLanguage@
    \else
        \do{\lst@language
        \ifx\lst@dialects\lst@emptydialect\else
            \expandafter\lst@NormedDef\expandafter\lst@language
                \expandafter{\lst@language}%
            \space(%
            \lst@BubbleSort\lst@dialects
            \expandafter\lst@PrintDialects\lst@dialects(\relax),%
            )%
        \fi}%
        \def\lst@next{\lst@NextLanguage#1(#2),}%
        \expandafter\lst@next
    \fi}
\def\lst@emptydialect{(),}
\def\lst@PrintDialects(#1),{%
    \ifx\@empty#1\@empty empty\else
        \lst@PrintDialect{#1}%
    \fi
    \lst@PrintDialects@}
\def\lst@PrintDialects@(#1),{%
    \ifx\relax#1\else
        , \lst@PrintDialect{#1}%
        \expandafter\lst@PrintDialects@
    \fi}
\def\lst@PrintDialect#1{%
    \lst@NormedDef\lst@temp{#1}%
    \expandafter\ifx\csname\@lst dd@\lst@language\endcsname\lst@temp
        \texttt{\underbar{#1}}%
    \else
        \texttt{#1}%
    \fi}
\def\lst@IfLE#1#2\@empty#3#4\@empty{%
    \ifx #1\relax
        \let\lst@next\@firstoftwo
    \else \ifx #3\relax
        \let\lst@next\@secondoftwo
    \else
        \lowercase{\ifx#1#3}%
            \def\lst@next{\lst@IfLE#2\@empty#4\@empty}%
        \else
            \lowercase{\ifnum`#1<`#3}\relax
                \let\lst@next\@firstoftwo
            \else
                \let\lst@next\@secondoftwo
            \fi
        \fi
    \fi \fi
    \lst@next}
\def\lst@BubbleSort#1{%
    \ifx\@empty#1\else
        \lst@false
        \expandafter\lst@BubbleSort@#1\relax,\relax,%
        \expandafter\lst@BubbleSort@\expandafter,\lst@sorted
                                      \relax,\relax,%
        \let#1\lst@sorted
        \lst@if
            \def\lst@next{\lst@BubbleSort#1}%
            \expandafter\expandafter\expandafter\lst@next
        \fi
    \fi}
\def\lst@BubbleSort@#1,#2,{%
    \ifx\@empty#1\@empty
        \def\lst@sorted{#2,}%
        \def\lst@next{\lst@BubbleSort@@}%
    \else
        \let\lst@sorted\@empty
        \def\lst@next{\lst@BubbleSort@@#1,#2,}%
    \fi
    \lst@next}
\def\lst@BubbleSort@@#1,#2,{%
    \ifx\relax#1\else
        \ifx\relax#2%
            \lst@lAddTo\lst@sorted{#1,}%
            \expandafter\expandafter\expandafter\lst@BubbleSort@@@
        \else
            \lst@IfLE #1\relax\@empty #2\relax\@empty
                          {\lst@lAddTo\lst@sorted{#1,#2,}}%
                {\lst@true \lst@lAddTo\lst@sorted{#2,#1,}}%
            \expandafter\expandafter\expandafter\lst@BubbleSort@@
        \fi
    \fi}
\def\lst@BubbleSort@@@#1\relax,{}
\endinput
%%
%% End of file `lstdoc.sty'.

[ zur Elbe Produktseite wechseln0.30Quellennavigators  Analyse erneut starten  ]