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

[Peter Lammich]

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.

--
  Peter

--------------

text ‹
  ▪ Item1
%  ▪ Item2
%  ▪ Item3
  ▪ Item4
›

*** Bad Markdown structure: illegal "item"⌂


text ‹
  ▪ Item1
  ⌦‹
  ▪ Item2
  ▪ Item3
  ›
  ▪ Item4
›

*** Error in formal comment: unclosed text cartouche⌂

[Makarius]

Post by Peter Lammich
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.

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