From 19c8963abdda3abecde409d98d1caf58eb932d4c Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Sun, 21 Jul 2019 10:41:06 +0100
Subject: [PATCH] Updated lstisadof.sty.

---
 .../IsaDof_Manual/document/lstisadof.sty      | 65 ++++++++++++++-----
 1 file changed, 49 insertions(+), 16 deletions(-)

diff --git a/examples/technical_report/IsaDof_Manual/document/lstisadof.sty b/examples/technical_report/IsaDof_Manual/document/lstisadof.sty
index 49072ce..bdee962 100644
--- a/examples/technical_report/IsaDof_Manual/document/lstisadof.sty
+++ b/examples/technical_report/IsaDof_Manual/document/lstisadof.sty
@@ -60,33 +60,67 @@
     \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{_{\mbox{#1}}}}
-\newcommand{\supscr}[1]{\ensuremath{^{\mbox{#1}}}}
+\newcommand{\subscr}[1]{\ensuremath{_{\text{#1}}}}
+\newcommand{\supscr}[1]{\ensuremath{^{\text{#1}}}}
 \lstdefinestyle{ISAR}{%
   language=%
   ,basicstyle=\ttfamily%
   ,showspaces=false%
   ,showlines=false%
   ,columns=flexible%
+  ,keepspaces
+  ,mathescape=false,
   ,morecomment=[s]{(*}{*)}%
   % ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
   ,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
   ,showstringspaces=false%
-  ,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}%
+  ,moredelim=*[is][\supscr]{<bsup>}{<esup>}%
+  ,moredelim=*[is][\subscr]{<bsub>}{<esub>}%
   ,literate={%
     {...}{\,\ldots\,}3%
-    {\\<Open>}{\ensuremath{\isacartoucheopen}}1%
-    {\\at}{@}1%
-    {\\<Close>}{\ensuremath{\isacartoucheclose}}1%
+    {<Open>}{\ensuremath{\isacartoucheopen}}1%
+    {<open>}{\ensuremath{\isacartoucheopen}}1%
+    {<@>}{@}1%
+    {"}{}0%
+    {~}{\ }1%
+    {::}{:\!:}1%
+    {<Close>}{\ensuremath{\isacartoucheclose}}1%
+    {<close>}{\ensuremath{\isacartoucheclose}}1%
     {\\<Gamma>}{\ensuremath{\Gamma}}1%
     {\\<times>}{\ensuremath{\times}}1%
-    {\\<rbrakk>}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}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%
+    {\\<equiv>}{\ensuremath{\equiv}}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\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
    ,tag=**[s]{@\{}{\}}%
@@ -97,18 +131,18 @@
    % Defining 2-keywords
    ,keywordstyle=[2]{\color{Blue!60}\bfseries}%
    ,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]{<}{>}
    % Defining 3-keywords
    ,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
    ,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
    ,keywordstyle=[4]{\color{black!60}\bfseries}%
-   ,morekeywords=[4]{where, imports}%
+   ,morekeywords=[4]{where, imports, keywords}%
    % Defining 5-keywords
    ,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
    ,keywordstyle=[6]{\itshape}%
    ,morekeywords=[6]{meta-args, ref, expr, class_id}%
@@ -117,8 +151,7 @@
 %% 
 \lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
     backgroundcolor=\color{black!2},
-    frame=lines,
-    mathescape=true,
+    frame=lines,mathescape,
     basicstyle=\footnotesize\ttfamily,#1}}{}
 %%% 
 \def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}