[isabelle-dev] Interpretation in arbitrary targets.

Makarius makarius at sketis.net
Tue May 21 13:59:13 CEST 2013

On Tue, 21 May 2013, Lars Noschinski wrote:

> On 21.05.2013 12:46, Makarius wrote:
>> An old idea on my list is to add some support to the Prover IDE to
>> rework theories with many consecutive "(in a)" to use just one "context
>> a begin ... end" around it -- this is also more efficient. Apart from
>> that I have occasionally considered to provide explicit fold support for
>> such contexts in the editor -- the canonical layout does not have any
>> indentation here.
> I don't know whether context blocks are an important unit for folding, 
> but something I have missed recently is a quick way to find out in what 
> context I am at a certain point in my theory.

OK, that's part of some first-class support of logical contexts within the 

I am reminded about the lack of something like that everytime I see funny 
comments like that:

   context foo


   end  (* context foo *)

Luckily such formally unchecked comments are rare.

> I do this usually by searching backwards for "context" (which means I 
> might miss contexts opened by "locale") or manually search through the 
> sidekick. To check whether I am in a local context at all, I usually 
> insert an additional "end" command and look for an error.

BTW, there is also the old-fashioned TTY command print_context to ask the 
prover.  It is more relevant in non-trivial contexts like 
'interpretation'.  On the other hand, all these things should be more 
immediate in the Prover IDE, as generated templates or similar.


More information about the isabelle-dev mailing list