Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Commenting out content in text <...>

Email Gateway (Aug 22 2022 at 18:07):

From: Peter Lammich <lammich@in.tum.de>
Hi list, 

I have the following:

text ‹
  ▪ Item1
  ▪ Item2
  ▪ Item3
  ▪ Item4
›

What is the proper way to "comment out" items 2 and 3? 
I.e. I want to leave them in for documentary purposes, but not have them in the generated latex.

I naively tried the following two, which unfortunately do not work as expected. In particular, I would have the last one expected to work.

Email Gateway (Aug 22 2022 at 18:33):

From: Makarius <makarius@sketis.net>
There is no proper way, you need to change the expectations.

The purpose of Markdown-like formats is to make the plain text appear
like the final document.

Removed material is better documented in the history of the sources
(e.g. Mercurial), instead of the sources themselves.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC