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