Re: [isabelle] Excluding theories from the session_graph output
On Mon, 28 Apr 2014, Joachim Breitner wrote:
I have am preparing an AFP submission that should contain a session
graph. It also contains a theory (“Everything”) that includes everything
and will \input’ed in the introduction, so it is not visible as a Theory
to the user. Currently, it shows up in the session graph (which is
confusing, makes the graph layout less nice and pulls in the also not
interesting TaTeXsugar theory).
Can I prevent isabelle from including that theory in the session graph?
Both the graph and HTML presentation are relatively old, and awaiting
renovation for many years. The graph tool and its wrap-up within the
document preparation is particularly ancient.
One could probably play nasty tricks with some perl scripts to force the
Isabelle document to look in a certain way, but that would play against
any reform of that if / when it actually happens.
For now I recommend to let the system do its work with minimal
intervention. E.g. what is the purpose of the Everything.thy instead of
just listing all its imports in ROOT?
Suppressing LaTeXsugar.thy could work by an auxiliary base session,
although for the purpose of AFP that is probably a bit much extra weight.
Since LaTeXsigar is part of the HOL-Library session, you could use that as
a base if you don't have any other special one already.
This archive was generated by a fusion of
Pipermail (Mailman edition) and