Hi everybody,
It is unfortunate that only the TLAPLUS source may be commented and not the TLC one. I propose
to use the syntax implemented by Literate Haskel. TLC code lines will begin by '>', an empty line
would separate any TLC code line and adjacent comments. Every line beginning by '>' will be considered
as pertaining to the same TLC code. Nothing else will be modified.
Example:
Comments and TLAPLUS code.
> The beginning ...
> ... of the TLC code.
(* Here some comments. *)
> The continuation of the TLC code
(* Some more comments. *)
> The end of the TLC code.
Continuation of comments and TLAPLUS code.
--
FL