Re: [isabelle] Feature request: definition on crtl+hover

On 03.01.2013 16:44, Alfio Martini wrote:
to HOL.thy   and  examining the split_if lemma I  wanted to continue
using this (Ctrl+Hover+Click) feature and jumping to the definition of the
case_split rule, for

But this feature does not seem to available any more in the file HOL.thy or
any other
theory loaded in jedit and which is part of Main. Am I doing
something wrong here [...probably...]?

No. At the moment, this information is unfortunately not available (as these theories are part of the heap image and were not processed in your jEdit session. To my knowledge, making this information available is on Makarius' list of things to do, but there are a lot of things on this list ;)

  -- Lars

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