Email Gateway (Oct 29 2023 at 23:10): Email Gateway (Oct 29 2023 at 23:10):From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear Isabelle users,
In the new AFP submission on which I am currently working, I am using the
LaTeX listings package for some sample C code snippets, enclosed between
\begin{lstlisting} and \end{lstlisting} commands, and everything worked fine
up to the previous document generation, performed a couple of weeks ago.
Particularly, my manual indentation of those code snippets using simple
spaces, according to some examples found on the internet, was faithfully
rendered in my document.
Yesterday, as I generated my document again, I found out to my surprise that
those code snippets are no longer indented in the document, although I had not
changed anything either in the snippets themselves or in the \lstset command
used to configure the package, which is reported here below.
\lstset{
basicstyle = \small\ttfamily,
frame = tb,
keywordstyle = \bfseries,
language = C,
numbers = left,
numberstyle = \tiny
}
I am using MikTeX on Windows 10, so after detecting this unexpected behavior,
I launched the MikTeX console to update the LaTeX packages. However, this did
not have any effect: when I generate my document, those code snippets keep not
being indented.
Does any one of you have any hint about the possible reasons for this sudden
change in the behavior of the package, as well as about some possible solution
to this issue?
Thank you very much, best regards,
Pasquale Noce
Email Gateway (Nov 01 2023 at 15:18):From: Makarius <makarius@sketis.net>
On 30/10/2023 00:10, Pasquale Noce wrote:
In the new AFP submission on which I am currently working, I am using the
LaTeX listings package for some sample C code snippets, enclosed between
\begin{lstlisting} and \end{lstlisting} commands
[...]
Yesterday, as I generated my document again, I found out to my surprise that
those code snippets are no longer indented in the document
On 31/10/2023 12:31, Pasquale Noce wrote:
I have further investigated this unexpected behavior, and it turns out to take
place if the text command containing the code listings also contains a list
created using the markdown control symbols described in the Isabelle/jEdit
reference manual (https://isabelle.in.tum.de/dist/Isabelle2023/doc/jedit.pdf,
section 4.2).
(The latter snippet is from a private mail thread. I will answer that here to
close the isabelle-users thread properly.)
The observation about markdown already explains the situation: a paragraph is
a list of lines where initial spaces are not taken into account for document
output. Only the indentation of the first line is significant --- to determine
overall markdown structure.
The listing environment is in conflict with that. It deviates from the normal
(non-)treatment of blanks within paragraphs. Thus it may be seen as a
variation on the "verbatim" environment, and needs to be treated similarly to
the "verbatim" document antiquotation.
Here is a suitable definition in Isabelle/ML:
setup ‹
Document_Output.antiquotation_raw_embedded \<^binding>‹lstlisting›
(Scan.lift Parse.embedded)
(fn _ => fn s =>
Latex.string "\\begin{lstlisting}\n" @
Latex.string (cat_lines (trim (forall_string Symbol.is_space)
(trim_split_lines s))) @
Latex.string "\n\\end{lstlisting}")
›
And here is an example document snippet:
text ‹
List:
▪ Lorem ipsum dolor sit amet, consectetur adipiscing elit.
▪ Sed sit amet porta orci, vitae ultricies ipsum. Phasellus volutpat arcu
quam, non blandit purus cursus vitae.
Nam vehicula magna ut purus sagittis, ac vehicula nisl iaculis. Nam nec
ullamcorper mi, non tincidunt ipsum.
\<^lstlisting>‹
do
{
r = a % b;
a = b;
b = r;
} while (b);
›
Cras sit amet est rhoncus massa semper venenatis. Sed elementum diam sed mi
tempor pellentesque sit amet at justo. Aliquam vitae nunc nec massa
ultricies ullamcorper.
›
The full example is attached (and hopefully not lost).
Makarius
Last updated: Jan 04 2025 at 20:18 UTC