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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
