[isabelle-dev] Interpretation in arbitrary targets.

[Makarius]

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

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

   context foo
   begin

   ...

   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.


 	Makarius