# 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

--- 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
+  @{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