Re: [isabelle] Error when Importing Theories from Library



On Mon, 2 Dec 2013, Alfio Martini wrote:

I have often encountered problems when importing thy files from
Library using jEdit/Isabelle (Windows). For instance, when
I type

"~~/src/HOL/Library/OptionalSugar"

the output windows gives the error "Bad Theory Name".
It took me a while to find a simple workaround: save
the file and reload it.

As far as I can tell this is the standard way up to and including Isabelle2013-2.

Before getting side-tracked on this second round of a really stable release, I was actually working towards more smooth file management in Isabelle/jEdit, but there are remaining problems with its physical buffer management. The editor uses old-school stateful implementations with mutable data structures everywhere, and it is hard to work with that efficiently and reliably.


	Makarius




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