Re: [isabelle] returning to the original document in Isabelle/jedit



Makarius wrote:

>> However, the documentation says
>>
>>    Presently (Isabelle2013-2) there is no systematic navigation within the editor
>>    to return to the original location.
>
> Isabelle2014-RC0 now has the Navigator plugin enabled.  Please try it to
> see if this important functionality works smoothly.

I installed it. If I have

theory Dummy
imports Main

begin
lemma "x Setprod y = 2"

ctrl-left-mouse-click on Setprod brings me to Group_Big.thy. The arrow in the menu then takes me back and forth, as in a browser, that is fine, thanks for the implementation.

However, when I try to ctrl-click on _finite_ in Group_Big.thy, the constant does not grow a border and Isabelle/JEdit does not jump to Finite_Set.thy. Is this the sought behaviour?

- Gergely



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