Isabelle_DOF/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty

\definecolor{OliveGreen}    {cmyk}{0.64,0,0.95,0.40}
\definecolor{BrickRed}      {cmyk}{0,0.89,0.94,0.28}
\definecolor{Blue}          {cmyk}{1,1,0,0}
\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0}

%%%\lst@BeginAspect[keywords]{isar}
\gdef\lst@tagtypes{s}
\gdef\lst@TagKey#1#2{%
    \lst@Delim\lst@tagstyle #2\relax
        {Tag}\lst@tagtypes #1%
                     {\lst@BeginTag\lst@EndTag}%
        \@@end\@empty{}}
\lst@Key{tag}\relax{\lst@TagKey\@empty{#1}}
\lst@Key{tagstyle}{}{\def\lst@tagstyle{#1}}
\lst@AddToHook{EmptyStyle}{\let\lst@tagstyle\@empty}
\gdef\lst@BeginTag{%
    \lst@DelimOpen
        \lst@ifextags\else
        {\let\lst@ifkeywords\iftrue
         \lst@ifmarkfirstintag \lst@firstintagtrue \fi}}
\lst@AddToHookExe{ExcludeDelims}{\let\lst@ifextags\iffalse}
\gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else}
\lst@Key{usekeywordsintag}t[t]{\lstKV@SetIf{#1}\lst@ifusekeysintag}
\lst@Key{markfirstintag}f[t]{\lstKV@SetIf{#1}\lst@ifmarkfirstintag}
\gdef\lst@firstintagtrue{\global\let\lst@iffirstintag\iftrue}
\global\let\lst@iffirstintag\iffalse
 \lst@AddToHook{PostOutput}{\lst@tagresetfirst}
 \lst@AddToHook{Output}
     {\gdef\lst@tagresetfirst{\global\let\lst@iffirstintag\iffalse}}
 \lst@AddToHook{OutputOther}{\gdef\lst@tagresetfirst{}}
\lst@AddToHook{Output}
    {\ifnum\lst@mode=\lst@tagmode
         \lst@iffirstintag \let\lst@thestyle\lst@gkeywords@sty \fi
         \lst@ifusekeysintag\else \let\lst@thestyle\lst@gkeywords@sty\fi
     \fi}
\lst@NewMode\lst@tagmode
\gdef\lst@Tag@s#1#2\@empty#3#4#5{%
    \lst@CArg #1\relax\lst@DefDelimB {}{}%
        {\ifnum\lst@mode=\lst@tagmode \expandafter\@gobblethree \fi}%
        #3\lst@tagmode{#5}%
    \lst@CArg #2\relax\lst@DefDelimE {}{}{}#4\lst@tagmode}%
\gdef\lst@BeginCDATA#1\@empty{%
    \lst@TrackNewLines \lst@PrintToken
    \lst@EnterMode\lst@GPmode{}\let\lst@ifmode\iffalse
    \lst@mode\lst@tagmode #1\lst@mode\lst@GPmode\relax\lst@modetrue}
%%\lst@EndAspect



% \gdef\lst@BeginTag{%
%     \lst@DelimOpen
%     \lst@ifextags\else
%         {\let\lst@ifkeywords\iftrue
%          \lst@ifmarkfirstintag\lst@firstintagtrue\fi\color{green}}}
% \gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else\color{green}}

\def\beginlstdelim#1#2#3%
{%
    \def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
    \ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
}
\newcommand{\subscr}[1]{\ensuremath{_{\text{#1}}}}
\newcommand{\supscr}[1]{\ensuremath{^{\text{#1}}}}
\lstdefinestyle{ISAR}{%
  language=%
  ,basicstyle=\ttfamily%
  ,showspaces=false%
  ,showlines=false%
  ,columns=flexible%
  ,keepspaces
  ,morecomment=[s]{(*}{*)}%
  % ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
  ,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
  ,showstringspaces=false%
  ,moredelim=*[is][\supscr]{<bsup>}{<esup>}%
  ,moredelim=*[is][\subscr]{<bsub>}{<esub>}%
  ,literate={%
    {...}{\,\ldots\,}3%
    {<Open>}{\ensuremath{\isacartoucheopen}}1%
    {<open>}{\ensuremath{\isacartoucheopen}}1%
    {<@>}{@}1%
    {"}{}0%
    {~}{\ }1%
    {::}{:\!:}1%
    {<Close>}{\ensuremath{\isacartoucheclose}}1%
    {<close>}{\ensuremath{\isacartoucheclose}}1%
    {\\<Gamma>}{\ensuremath{\Gamma}}1%
    {\\<theta>}{\ensuremath{\theta}}1%
    {\\<times>}{\ensuremath{\times}}1%
    {\\<equiv>}{\ensuremath{\equiv}}1%
    {\\<sigma>}{\ensuremath{\sigma}}1%
    {\\<geq>}{\ensuremath{\geq}}1%
    {level0}{level\textsubscript{0}}6%
    {\\<Rightarrow>}{\ensuremath{\Rightarrow}}1%
    {\\<rightarrow>}{\ensuremath{\rightarrow}}1%
    {\\<longrightarrow>}{\ensuremath{\rightarrow}}1%
    {\\<and>}{\ensuremath{\land}}1%  
    {\\<or>}{\ensuremath{\lor}}1%
    {\\<lfloor>}{\ensuremath{\lfloor}}1%
    {\\<rfloor>}{\ensuremath{\rfloor}}1%  
    %{\\<lparr>}{\ensuremath{\lparr}}1% 
    %{\\<rparr>}{\ensuremath{\rparr}}1%
    {\\<le>}{\ensuremath{\le}}1%
    {\\<delta>}{\ensuremath{\delta}}1%
    {\\<lambda>}{\ensuremath{\lambda}}1%
    {\\<bar>}{\ensuremath{\vert}}1%
    {\<sigma>}{\ensuremath{\sigma}}1%
    {\\<lparr>}{\ensuremath{\isasymlparr}}1%  
    {\\<rparr>}{\ensuremath{\isasymrparr}}1% 
    {\\<leftrightarrow>}{\ensuremath{\leftrightarrow}}1%
    {\{*}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
    {*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
    {\\<open>}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
    {\\<Open>}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
    {\\<close>}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
    {\\<Close>}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
    {\\<forall>}{\ensuremath{\forall}}1%
    {\\<exists>}{\ensuremath{\exists}}1%
    {\\<in>}{\ensuremath{\in}}1%
    {\\<delta>}{\ensuremath{\delta}}1%
    {\\<real>}{\ensuremath{\mathbb{R}}}1%
    {¥}{}0%
    {\\<noteq>}{\ensuremath{\neq}}1%
    {\\<exists>}{\ensuremath{\exists}}1%
    {\\<Forall>}{\ensuremath{\bigwedge\,}}1%
    {<string>}{<\ensuremath{\text{\textit{string}}}>}9%
    {\\<lbrakk>}{\ensuremath{\mathopen{\lbrack\mkern-3mu\lbrack}}}1%
    {\\<lbrace>}{\ensuremath{\mathopen{\lbrace\mkern-4.5mu\mid}}}1%
    {\\<rbrakk>}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}1%
    {\\<rbrace>}{\ensuremath{\mathclose{\mid\mkern-4.5mu\rbrace}}}1%
  }%
  % % Defining "tags" (text-antiquotations) based on 1-keywords
   ,tag=**[s]{@\{}{\}}%
   ,tagstyle=\color{CornflowerBlue}%
   ,markfirstintag=true%
   ,keywordstyle=\bfseries%
   ,keywords={}
   % Defining 2-keywords
   ,keywordstyle=[2]{\color{Blue!60}\bfseries}%
   ,alsoletter={*,-}
   ,morekeywords=[2]{case, then, show, theory, begin, end, ML,section,subsection,paragraph,chapter,text}%
   %,moredelim=[s][\textit]{<}{>}
   % Defining 3-keywords
   ,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
   ,morekeywords=[3]{doc_class,declare_reference,update_instance*,
     open_monitor*,  close_monitor*, declare_reference*,section*,text*,title*,abstract*}%
   % Defining 4-keywords
   ,keywordstyle=[4]{\color{black!60}\bfseries}%
   ,morekeywords=[4]{where, imports, keywords}%
   % Defining 5-keywords
   ,keywordstyle=[5]{\color{BrickRed!70}\bfseries}%
   ,morekeywords=[5]{datatype, by, fun, Definition*, definition, type_synonym, typedecl, consts, assumes, and, shows, proof, next, qed, lemma, theorem}%
   % Defining 6-keywords
   ,keywordstyle=[6]{\itshape}%
   ,morekeywords=[6]{meta-args, ref, expr, class_id}%
  % 
}%
%% 

\newcommand{\lstlabel}[2]{%
  \mbox{}\hfill\begin{picture}(0,0)%
    \put(-47,25){\fcolorbox{black}{#1}{\parbox{1.4cm}{\centering\footnotesize #2}}}
  \end{picture}\vspace{-5ex}%
}
\lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
    backgroundcolor=\color{blue!6},
    frame=lines,mathescape,
    basicstyle=\footnotesize\ttfamily,#1}}%
    {\lstlabel{blue!60!black}{\textcolor{white}{Isar}}}
%%% 
\def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}

\lstnewenvironment{out}[1][]{\lstset{
    backgroundcolor=\color{green!6},
    frame=lines,mathescape,breakatwhitespace=true
    ,columns=flexible%
    ,basicstyle=\footnotesize\rmfamily,#1}}
    {\lstlabel{green!60!black}{\textcolor{white}{Document}}}


%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%
\lstloadlanguages{ML}
\lstdefinestyle{sml}{basicstyle=\ttfamily,%
                     commentstyle=\itshape,%
                     keywordstyle=\bfseries\color{CornflowerBlue},%
                     ndkeywordstyle=\color{red},%
                     language=ML,
   ,keywordstyle=[6]{\itshape}%
   ,morekeywords=[6]{args_type}%
}%

\lstnewenvironment{sml}[1][]{\lstset{style=sml,
    backgroundcolor=\color{red!6},
    frame=lines,
    basicstyle=\footnotesize\ttfamily,#1}}%{}
    {\lstlabel{red!60!black}{\textcolor{white}{SML}}}
%%% 
\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}


\lstloadlanguages{TeX}
\lstdefinestyle{ltx}{language=[AlLaTeX]TeX,
  ,basicstyle=\ttfamily%
  ,showspaces=false%
  ,showlines=false%
  ,columns=flexible%
  ,morekeywords={newisadof}
 %  ,keywordstyle=\bfseries%
   % Defining 2-keywords
   ,keywordstyle=[1]{\color{BrickRed!60}\bfseries}%
   % Defining 3-keywords
   ,keywordstyle=[2]{\color{OliveGreen!60}\bfseries}%
   % Defining 4-keywords
   ,keywordstyle=[3]{\color{black!60}\bfseries}%
   % Defining 5-keywords
   ,keywordstyle=[4]{\color{Blue!70}\bfseries}%
   % Defining 6-keywords
   ,keywordstyle=[5]{\itshape}%
  % 
}
\lstdefinestyle{displayltx}{style=ltx,
                basicstyle=\ttfamily\footnotesize,
                backgroundcolor=\color{yellow!7}, frame=lines}%

\lstnewenvironment{ltx}[1][]{\lstset{style=displayltx, #1}}%
    {\lstlabel{yellow!60!black}{\textcolor{white}{\LaTeX}}}
\def\inlineltx{\lstinline[style=ltx, breaklines=true,columns=fullflexible]}





\lstloadlanguages{bash}
\lstdefinestyle{bash}{language=bash,
  ,basicstyle=\ttfamily%
  ,showspaces=false%
  ,showlines=false%
  ,columns=flexible%
 %  ,keywordstyle=\bfseries%
   % Defining 2-keywords
   ,keywordstyle=[1]{\color{BrickRed!60}\bfseries}%
   % Defining 3-keywords
   ,keywordstyle=[2]{\color{OliveGreen!60}\bfseries}%
   % Defining 4-keywords
   ,keywordstyle=[3]{\color{black!60}\bfseries}%
   % Defining 5-keywords
   ,keywordstyle=[4]{\color{Blue!70}\bfseries}%
   % Defining 6-keywords
   ,keywordstyle=[5]{\itshape}%
  % 
}
\lstdefinestyle{displaybash}{style=bash,
                basicstyle=\ttfamily\footnotesize,
                backgroundcolor=\color{black!5}, frame=lines}%

\lstnewenvironment{bash}[1][]{\lstset{style=displaybash, #1}}%{}
    {\lstlabel{black!60!white}{\textcolor{white}{Bash}}}
\def\inlinebash{\lstinline[style=bash, breaklines=true,columns=fullflexible]}