[isabelle-dev] Interpretation in arbitrary targets.
noschinl at in.tum.de
Tue May 21 13:50:32 CEST 2013
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.
More information about the isabelle-dev