[isabelle-dev] Interpretation in arbitrary targets.

[Lars Noschinski]

On 21.05.2013 13:59, Makarius wrote:
>> 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.

I did not know about print_context, which solves my immediate use case.

This command is not documented in the reference manual (at least not in 
the index), though. Also, it only seems to work half-way for unnamed 
contexts:

   - If I open an unnamed context with some fixes, assumes in the theory
     context, print_context ignores this, i.e. in

        theory Foo imports Main begin
        context fixes P assumes P begin

     print_context outputs only "theory Foo".

   - This is different inside a named context:

        theory Foo imports Main begin
        locale A begin
        context fixes P assumes P begin

     yields

        theory Foo
        locale A =
          fixes P :: "bool"
          assumes "P"

     as output of print_context. Although this might also be considered
     slightly irritating, as those elements are not part of the locale,
     so something like

        theory Foo
        locale A
        context
          fixes P :: "bool"
          assumes "P"

     would be better.

How is interpretation related to print_context? It seems that neither 
interpret nor interpretation extends the context as displayed by 
print_context?

   -- Lars