Re: [isabelle] Browsing finished theories in Isabelle/jEdit



* 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.

Attachment: signature.asc
Description: PGP signature



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