Re: [isabelle] Pretty-printing for trees in 2D



On 24/06/18 16:52, Makarius wrote:
> Generally, only a PIDE front-end (Isabelle/Scala) can display things,
> not the back-end (Isabelle/ML). E.g. see the @{doc} antiquotation.

Well, yes, I was thinking of something similar to what
thy_deps/code_deps does: Display some markup that one can click on to
get to the PDF file. Or some kind of jEdit popup.


> Both Graphviz and Isabelle Graphview are for DAG layout, not
> specifically for trees.

That is true, but dot attempts to keep the lexicographic ordering of
children, and in a tree, I think it always does, since there are no real
constraints that prevent it from doing that. People do use Graphviz to
visualise ordered trees a lot.


> It might be better to integrate a decent tree layout algorithm into
> Isabelle/Scala, and thus avoid the usual problems with external tools:
> manual tinkering with installation that "works for me" but not for everyone.

Yes, one could do that. But the GUI would have to support quite a few
things in order to reach the same kind of versatility w.r.t. diffferent
node shapes that Graphviz provides. I took advantage of that a lot and I
think the results speak for themselves.

In any case, I do agree that having Isabelle talk to Graphviz is a
suboptimal solution unless possibly if we want to integrate Graphviz as
a component (which we probably don't).

I do think that offering Graphviz code as one possible output format is
a good idea though; that way people can easily produce PDFs/LaTeX, e.g.
for slides.

Manuel





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.