How to add \newpage latex command without spurious comment box in the typeset spec ?

24 views
Skip to first unread message

dp.sim...@gmail.com

unread,
May 21, 2020, 2:15:43 AM5/21/20
to tlaplus

I want to start a new page in the typeset version of the spec. If I add the corresponding code


\* `^\newpage^'


to the source file, the new page is started, but there is also an annoying little gray empty comment box at the start of the new page (I use -shade option for tla2latex). This is obviously because there is comment that contains this \newpage latex comment. I did not find a way for tla2latex to ignore that and just start a new page.


\*`^\newpage^' Some comment


Results in non-grayed "Some comment" at the start of the new page with a little gray box below

Is there a way to start a new page cleanly ?


Some way to temporarily switch off 'graying' of the comments so that that empty space before newpage commant is not visible, or maybe some way to feed newpage command to latex not from the command ?

Reply all
Reply to author
Forward
0 new messages