[isabelle-dev] Interpretation in arbitrary targets.
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:
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