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



Thanks it worked. 

Working with 

http://isabelle.in.tum.de/repos/isabelle/raw-file/79c92e2dc359/src/Doc/JEdit/JEdit.thy

I created a small patch so that the Isabelle/JEdit documentation would write about this feature:

--- JEdit.thy   2014-01-21 16:58:04.555705621 +0100
+++ JEdit-mod.thy       2014-01-21 17:02:50.450960114 +0100
@@ -480,9 +480,9 @@

   \medskip A black rectangle in the text indicates a hyperlink that
   may be followed by a mouse click (while the @{verbatim CONTROL} or
-  @{verbatim COMMAND} modifier key is still pressed). Presently
-  (Isabelle2013-2) there is no systematic navigation within the
-  editor to return to the original location.
+  @{verbatim COMMAND} modifier key is still pressed). It is possible
+  to go back to the original document by pressing @{verbatim CONTROL}
+  or @{verbatim COMMAND} and a backtick.

   Also note that the link target may be a file that is itself not
   subject to formal document processing of the editor session and thus
@@ -1138,4 +1138,4 @@
   \end{itemize}
 *}

- Gergely

-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Lawrence Paulson
Sent: Tuesday, January 21, 2014 4:32 PM
To: Buday Gergely
Cc: cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] returning to the original document in Isabelle/jedit

You mean, to go back to where you started from? Use ctrl-` (CMD-` on a Mac).

To allow navigation within a single document, use the Marks menu. It would be great if there were some sort of global bookmark system, but I don't know of anything.

Larry

On 21 Jan 2014, at 14:39, Buday Gergely <gbuday at karolyrobert.hu> wrote:

> Hi,
> 
> holding down ctrl and clicking on a name makes Isabelle/jedit to jump to the definition of that name.
> 
> However, the documentation says
> 
>    Presently (Isabelle2013-2) there is no systematic navigation within the editor
>    to return to the original location.
> 
> Would implementing this be technically difficult or obviously there are more important things to do?
> 
> - Gergely
> 






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