[isabelle-dev] Interpretation in arbitrary targets.

[Lars Noschinski]

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.

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.

   -- Lars