further encouragement to read jEdit documentation;
authorwenzelm
Sat, 30 Nov 2013 17:51:25 +0100
changeset 54655 9e8189a841f7
parent 54654 6a35bc1ee210
child 54656 84177f8372f9
further encouragement to read jEdit documentation;
src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Nov 30 17:38:08 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sat Nov 30 17:51:25 2013 +0100
@@ -121,9 +121,12 @@
 subsection {* Documentation *}
 
 text {* Regular jEdit documentation is accessible via its @{verbatim
-  Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
-  \emph{User's Guide} and \emph{Frequently Asked Questions} for this
-  sophisticated text editor.
+  Help} menu or @{verbatim F1} keyboard shortcut.  This includes a
+  full \emph{User's Guide} and \emph{Frequently Asked Questions} for
+  this sophisticated text editor.  The same can be browsed without the
+  technical restrictions of the built-in Java HTML viewer here:
+  \url{http://www.jedit.org/index.php?page=docs} (potentially for a
+  different version of jEdit).
 
   Most of this information about jEdit is relevant for Isabelle/jEdit
   as well, but one needs to keep in mind that defaults sometimes