Updated lstisadof.sty.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
parent
eef387198a
commit
19c8963abd
|
@ -60,33 +60,67 @@
|
||||||
\def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
|
\def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
|
||||||
\ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
|
\ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
|
||||||
}
|
}
|
||||||
\newcommand{\subscr}[1]{\ensuremath{_{\mbox{#1}}}}
|
\newcommand{\subscr}[1]{\ensuremath{_{\text{#1}}}}
|
||||||
\newcommand{\supscr}[1]{\ensuremath{^{\mbox{#1}}}}
|
\newcommand{\supscr}[1]{\ensuremath{^{\text{#1}}}}
|
||||||
\lstdefinestyle{ISAR}{%
|
\lstdefinestyle{ISAR}{%
|
||||||
language=%
|
language=%
|
||||||
,basicstyle=\ttfamily%
|
,basicstyle=\ttfamily%
|
||||||
,showspaces=false%
|
,showspaces=false%
|
||||||
,showlines=false%
|
,showlines=false%
|
||||||
,columns=flexible%
|
,columns=flexible%
|
||||||
|
,keepspaces
|
||||||
|
,mathescape=false,
|
||||||
,morecomment=[s]{(*}{*)}%
|
,morecomment=[s]{(*}{*)}%
|
||||||
% ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
|
% ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
|
||||||
,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
|
,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
|
||||||
,showstringspaces=false%
|
,showstringspaces=false%
|
||||||
,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}%
|
,moredelim=*[is][\supscr]{<bsup>}{<esup>}%
|
||||||
|
,moredelim=*[is][\subscr]{<bsub>}{<esub>}%
|
||||||
,literate={%
|
,literate={%
|
||||||
{...}{\,\ldots\,}3%
|
{...}{\,\ldots\,}3%
|
||||||
{\\<Open>}{\ensuremath{\isacartoucheopen}}1%
|
{<Open>}{\ensuremath{\isacartoucheopen}}1%
|
||||||
{\\at}{@}1%
|
{<open>}{\ensuremath{\isacartoucheopen}}1%
|
||||||
{\\<Close>}{\ensuremath{\isacartoucheclose}}1%
|
{<@>}{@}1%
|
||||||
|
{"}{}0%
|
||||||
|
{~}{\ }1%
|
||||||
|
{::}{:\!:}1%
|
||||||
|
{<Close>}{\ensuremath{\isacartoucheclose}}1%
|
||||||
|
{<close>}{\ensuremath{\isacartoucheclose}}1%
|
||||||
{\\<Gamma>}{\ensuremath{\Gamma}}1%
|
{\\<Gamma>}{\ensuremath{\Gamma}}1%
|
||||||
{\\<times>}{\ensuremath{\times}}1%
|
{\\<times>}{\ensuremath{\times}}1%
|
||||||
{\\<rbrakk>}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}1%
|
{\\<equiv>}{\ensuremath{\equiv}}1%
|
||||||
{\\<rbrace>}{\ensuremath{\mathclose{\mid\mkern-4.5mu\rbrace}}}1%
|
|
||||||
{\\<lbrakk>}{\ensuremath{\mathopen{\lbrack\mkern-3mu\lbrack}}}1%
|
|
||||||
{\\<lbrace>}{\ensuremath{\mathopen{\lbrace\mkern-4.5mu\mid}}}1%
|
|
||||||
{\\<Rightarrow>}{\ensuremath{\Rightarrow}}1%
|
{\\<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\langle$}}1%
|
||||||
{*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
|
{*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
|
||||||
|
{\\<open>}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}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%
|
||||||
|
{\\<noteq>}{\ensuremath{\neq}}1%
|
||||||
|
{\\<Forall>}{\ensuremath{\bigwedge\,}}1%
|
||||||
|
{\\<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
|
% % Defining "tags" (text-antiquotations) based on 1-keywords
|
||||||
,tag=**[s]{@\{}{\}}%
|
,tag=**[s]{@\{}{\}}%
|
||||||
|
@ -97,18 +131,18 @@
|
||||||
% Defining 2-keywords
|
% Defining 2-keywords
|
||||||
,keywordstyle=[2]{\color{Blue!60}\bfseries}%
|
,keywordstyle=[2]{\color{Blue!60}\bfseries}%
|
||||||
,alsoletter={*,-}
|
,alsoletter={*,-}
|
||||||
,morekeywords=[2]{theory, begin, end, ML,section,subsection,paragraph,chapter,text}%
|
,morekeywords=[2]{case, then, show, theory, begin, end, ML,section,subsection,paragraph,chapter,text}%
|
||||||
%,moredelim=[s][\textit]{<}{>}
|
%,moredelim=[s][\textit]{<}{>}
|
||||||
% Defining 3-keywords
|
% Defining 3-keywords
|
||||||
,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
|
,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
|
||||||
,morekeywords=[3]{doc_class,declare_reference,update_instance*,
|
,morekeywords=[3]{doc_class,declare_reference,update_instance*,
|
||||||
open_monitor*, close_monitor*, figure*, title*, subtitle*,declare_reference*,section*,text*}%
|
open_monitor*, close_monitor*, declare_reference*,section*,text*,title*,abstract*}%
|
||||||
% Defining 4-keywords
|
% Defining 4-keywords
|
||||||
,keywordstyle=[4]{\color{black!60}\bfseries}%
|
,keywordstyle=[4]{\color{black!60}\bfseries}%
|
||||||
,morekeywords=[4]{where, imports}%
|
,morekeywords=[4]{where, imports, keywords}%
|
||||||
% Defining 5-keywords
|
% Defining 5-keywords
|
||||||
,keywordstyle=[5]{\color{BrickRed!70}\bfseries}%
|
,keywordstyle=[5]{\color{BrickRed!70}\bfseries}%
|
||||||
,morekeywords=[5]{datatype, typedecl, consts, theorem}%
|
,morekeywords=[5]{datatype, by, fun, Definition*, definition, type_synonym, typedecl, consts, assumes, and, shows, proof, next, qed, lemma, theorem}%
|
||||||
% Defining 6-keywords
|
% Defining 6-keywords
|
||||||
,keywordstyle=[6]{\itshape}%
|
,keywordstyle=[6]{\itshape}%
|
||||||
,morekeywords=[6]{meta-args, ref, expr, class_id}%
|
,morekeywords=[6]{meta-args, ref, expr, class_id}%
|
||||||
|
@ -117,8 +151,7 @@
|
||||||
%%
|
%%
|
||||||
\lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
|
\lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
|
||||||
backgroundcolor=\color{black!2},
|
backgroundcolor=\color{black!2},
|
||||||
frame=lines,
|
frame=lines,mathescape,
|
||||||
mathescape=true,
|
|
||||||
basicstyle=\footnotesize\ttfamily,#1}}{}
|
basicstyle=\footnotesize\ttfamily,#1}}{}
|
||||||
%%%
|
%%%
|
||||||
\def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}
|
\def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}
|
||||||
|
|
Loading…
Reference in New Issue