[isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context



Dear Makarius,

I noticed that when I open a locale that has been defined in the image of the session and Ctrl-Click on an identifer which refers to an abbreviation in that locale, then Isabelle/jEdit jumps to the begin of the context block. I would have expected that it jumps to the declaration of the abbreviation as it does for definitions. Here's a MWE for Isabelle2013-1:

theory Scratch imports Main begin
(*1*)context partial_function_definitions begin
term "fixp_fun"
end
end

Ctrl-Click on fixp_fun jumps to (*1*), but I would prefer line 130 of Partial_Function.thy.

Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.