From 59083458c8e167b928b6c6866532567e8c345d47 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 28 Mar 2023 08:50:19 +0200
Subject: [PATCH] [doc] more dune keywords + use logs in some places

---
 doc/developer/advance.tex | 26 +++++++++++++-------------
 doc/frama-c-book.cls      | 24 +++++++++++++-----------
 2 files changed, 26 insertions(+), 24 deletions(-)

diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index a04757d570c..3b057633b8b 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -4209,9 +4209,9 @@ For quick usage of the library:
 \item install the instrumented \framac: \texttt{make install DUNE\_WS=bench}.
 \item enable instrumentation {\em during execution} of \framac, using the
   \texttt{OCAML\_LANDMARKS} environment variable:
-\begin{lstlisting}
+\begin{logs}
 OCAML_LANDMARKS=<options> frama-c [files] [options]
-\end{lstlisting}
+\end{logs}
   The easiest setup is \texttt{OCAML\_LANDMARKS=auto}, which will instrument
   everything and output timing information to \texttt{stderr} after
   program termination.
@@ -4219,10 +4219,10 @@ OCAML_LANDMARKS=<options> frama-c [files] [options]
   output the timing information to file \texttt{landmarks.log}.
 \item you can also run the instrumented \framac without installing it, via
   \texttt{dune exec}:
-\begin{shell}
+\begin{logs}
 OCAML_LANDMARKS=auto dune exec --workspace dev/dune-workspace.bench \
   --context bench -- frama-c [files] [options]
-\end{shell}
+\end{logs}
   The \verb+--workspace dev/dune-workspace.bench+ argument tells Dune to use
   the workspace in which Landmarks is configured.
 
@@ -4238,9 +4238,9 @@ of the file.
 To instrument a single function: add \verb+[@landmark]+ after the \texttt{let},
 e.g.:
 
-\begin{lstlisting}
+\begin{ocamlcode}
   let[@landmark] add_visitor vis =
-\end{lstlisting}
+\end{ocamlcode}
 
 Check \url{https://github.com/LexiFi/landmarks} for its documentation.
 
@@ -4257,7 +4257,7 @@ To profile your own plug-in using Landmarks, do the following:
    (public_name frama-c-my-plug-in.core)
    ...
    (libraries frama-c.kernel)
-   (instrumentation (backend landmarks)) ;<<< ADD THIS LINE
+   (instrumentation (backend landmarks)) ; <<< ADD THIS LINE
  )
 \end{dunecode}
 \item Create a \verb|dune-workspace.bench| file in your plugin's top-level
@@ -4266,21 +4266,21 @@ To profile your own plug-in using Landmarks, do the following:
   \duneinput{dune-workspace.bench}
 \item Add \verb|--workspace=dune-workspace.bench| to the \verb|dune build|
   and \verb|dune install| commands that you run, e.g.:
-\begin{lstlisting}
+\begin{logs}
 dune build --workspace=dune-workspace.bench @install
 dune install --workspace=dune-workspace.bench
-\end{lstlisting}
+\end{logs}
 This will compile and install the plug-in with Landmarks instrumentation
 enabled. Then you just need to set \verb|OCAML_LANDMARKS| as described in the
 previous section, e.g.:
-\begin{lstlisting}
+\begin{logs}
 OCAML_LANDMARKS=auto frama-c [my-plugin-options]
-\end{lstlisting}
+\end{logs}
 \item For \verb|dune exec|, you need to add the \verb|--workspace| option
   as well as \verb|--context bench|. Combined with \verb|OCAML_LANDMARKS|,
   the command-line will resemble the following:
-\begin{lstlisting}
+\begin{logs}
 OCAML_LANDMARKS=auto dune exec --workspace dev/dune-workspace.bench \
   --context bench -- frama-c [files] [options]
-\end{lstlisting}
+\end{logs}
 \end{enumerate}
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index 93ad4c82df9..3436b3c0c26 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -432,6 +432,7 @@
 \definecolor{lstmodule}{rgb}{0.3,0.6,0.2}
 \definecolor{lstspecial}{rgb}{0.2,0.6,0.0}
 \definecolor{lstfile}{gray}{0.85}
+\definecolor{lstcomments}{rgb}{0.35,0.35,0.35}
 
 \newcommand{\lstbrk}{\mbox{$\color{blue}\scriptstyle\cdots$}}
 
@@ -439,7 +440,7 @@
 \def\lp@inline{\ifmmode\normalfont\mathtt\scriptstyle\else\normalfont\ttfamily\mdseries\normalsize\fi}
 \def\lp@keyword{}
 \def\lp@special{\color{frama-c-dark-orange}}
-\def\lp@comment{\normalfont\ttfamily\mdseries}
+\def\lp@comment{\normalfont\ttfamily\mdseries\color{lstcomments}}
 \def\lp@string{\color{frama-c-dark-green}}
 \def\lp@ident{}
 \def\lp@number{\rmfamily\tiny\color{lstnum}\noncopynumber}
@@ -614,17 +615,18 @@
     {é}{{\'e}}1%
   ,
   style=frama-c-style,%
-  morekeywords={
-    action, alias, as, deps, dune, executable, files, flags, from,
-    generate_opam_files, install, lang, libraries, library, name, optional,
-    package, plugin, progn, public_name, rule, section, select, site,
-    targets, using
+  alsoletter=:-,%
+  keywords={%
+    action,alias,as,backend,context,default,deps,dune,executable,%
+    env,env-vars,files,flags,from,generate_opam_files,install,%
+    instrument_with,instrumentation,lang,libraries,library,name,optional,%
+    package,plugin,profile,progn,public_name,rule,section,select,site,%
+    targets,using%
   },%
-  alsoletter=:,
-  morekeywords=[2]{
-    :standard
-  },
-  morecomment=[l]{;},
+  morekeywords=[2]{%
+    :standard%
+  },%
+  morecomment=[l]{;},%
 }
 
 \lstdefinestyle{dune-basic}{%
-- 
GitLab