isarmathlib-devel
[Top][All Lists]
Advanced

[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


      




reply via email to

[Prev in Thread] Current Thread [Next in Thread]