* Makarius <makarius at sketis.net> [2017-02-08 17:58 +0100]: > On 08/02/17 10:30, Timothy Bourke wrote: > > I want to use Isabelle to better understand the Knaster-Tarski > > fixpoint theorem. So, I fire up Isabelle/jEdit and use the "Search in > > Directory..." feature to look for "Knaster-Tarski" (BTW, it would be > > great if the directory list in the dialog box automatically included > > $ISABELLE_HOME). > > Note that the regular jEdit file dialog provides various Isabelle entry > points via "Favorites". I did not know that. That is very nice. Something similar for the directory search would be great. > > Now, looking at the theorem, I want to know the exact definition of a > > complete lattice, so I COMMAND/CTRL-click on "complete_lattice". The > > Complete_Lattices.thy file opens at the correct position but is not > > processed (everything is pink) due to the error "Cannot update > > finished theory". This means, in particular, that I cannot continue > > COMMAND/CTRL-clicking to follow the definitions further. > > This is an old omission in the PIDE document model. Already loaded > sources are "dead" and cannot be explored. After so many years it is > still not properly done, but I have already quite concrete ideas how to > do it soon: using offline PIDE markup in some SQLite database that is > used as "Isabelle application file format". It will eventually replace > the old log files. I am happy to hear that it is in the grand design. Thank you. > > Thus this naive question from someone who no longer uses Isabelle > > every day (sniff): > > Maybe you can occasionally show your fellow non-Isabelle users the state > of sophistication of Isabelle at the end of 2016. From time to time, I do exactly that. Without want to gush, I still find Isabelle great. Tim.
Description: PGP signature