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 MHonArc.