Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

When pretty printing with the option where model only is switched off one shall not generate \section{ClassName} #641

Closed
pglvdm opened this issue Sep 2, 2017 · 0 comments
Assignees
Labels
enhancement Not a bug, but nice to have
Milestone

Comments

@pglvdm
Copy link
Contributor

pglvdm commented Sep 2, 2017

Right now if one blends the LaTeX and VDM parts and one choose to include the latex parts one typically need to start a VDM file with a \section{The XXX Class}. The consequence is that one gets a table of contents with section N called XXX and section N+1 called "The XXX class". Thus, if one choose to not only LaTeX the model it is the users responsibility to insert the necessary \section's.

@idhugoid idhugoid added the enhancement Not a bug, but nice to have label Sep 5, 2017
@idhugoid idhugoid self-assigned this Sep 5, 2017
@idhugoid idhugoid added this to the v2.5.2 milestone Sep 5, 2017
@idhugoid idhugoid closed this as completed Sep 5, 2017
@peterwvj peterwvj modified the milestones: v2.5.4, v2.5.2 Sep 8, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement Not a bug, but nice to have
Projects
None yet
Development

No branches or pull requests

3 participants