[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Isarmathlib-devel] Hypergraph based definitions browser for IsarMathLib
From: |
Slawomir Kolodynski |
Subject: |
[Isarmathlib-devel] Hypergraph based definitions browser for IsarMathLib |
Date: |
Sat, 8 Nov 2008 07:54:34 -0800 (PST) |
I have been thinking recently about implementing a definitions browser for
IsarMathLib. The idea is to collect the dependency information from theories
parsed by tiddlyisar and create description of it in
[GraphXML](http://www.cwi.nl/ftp/CWIreports/INS/INS-R0009.pdf) which would then
be be shown by (Hypergraph)[http://hypergraph.sourceforge.net/graphxml.html] .
The nodes of the graph would reference PNG pictures generated by some LaTeX to
PNG tool from definitions (unless you have a better idea).
So, using datatypes defined in IMLP_datatypes.hs, we need a function
genGraphXML :: [Theory] -> String
that generates the graph description from parsed theories and
extractDefs :: [Theory] -> [(String,String)]
that produces the pairs (<name of definition>, <LaTeX string>) for all
definitions. The second function would be easy, the first one rather involved.
I think it would be a cool thing to have, let me know if you (anybody on this
list) are interested in working on this.
Slawekk
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Isarmathlib-devel] Hypergraph based definitions browser for IsarMathLib,
Slawomir Kolodynski <=