Re: [Isarmathlib-devel] Symbolic links

[Slawomir Kolodynski]

> There are symbolic links in the repository under the
> directory
> tiddlyisar. And they point to /home/slawek/... 

This is fixed now, replaced by relative links.

> What do you think about modifying tiddlyisar/ROOT.ML to do
> use_thy
> "../IsarMathLib/Introduction", etc.?

That's one way of fixing it. It is quite a lot of work though, you would have 
to modify the extractTheoryName function in tiddlyisar.hs to deal with the 
change and other things as theory names are used as the part of the magic 
string that gets replaced with TiddlyWiki markup in the formalmath_empty.html , 
so the software would have to understand the difference between ``theory file 
name`` and ``theory path``.  The original idea was to just use IsarMathLib's 
ROOT.ML here, but tiddlyisar can not parse all theories yet, thus need for a 
shorter one. 

Slawek