# HG changeset patch
# User wenzelm
# Date 1381599719 -7200
# Node ID 9e944630be0c7c35020af9d5f7b34f4dc34d9b2d
# Parent  2189d05622c4b909b64185699f7139494a32991d
more screenshots;
tuned;

diff -r 2189d05622c4 -r 9e944630be0c src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Oct 12 19:00:59 2013 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Oct 12 19:41:59 2013 +0200
@@ -64,7 +64,12 @@
 section {* The Isabelle/jEdit Prover IDE *}
 
 text {*
+  \begin{figure}[htbp]
+  \begin{center}
   \includegraphics[width=\textwidth]{isabelle-jedit}
+  \end{center}
+  \caption{The Isabelle/jEdit Prover IDE}
+  \end{figure}
 
   Isabelle/jEdit consists of some plugins for the well-known jEdit
   text editor \url{http://www.jedit.org}, according to the following
@@ -299,11 +304,25 @@
   COMMAND} on Mac OS X.  Hovering with the mouse while the modifier is
   pressed reveals \emph{tooltips} (grey box within the text with a
   yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within
-  the text).  Tooltip popups use the same rendering principles as the
+  the text).
+
+  \begin{figure}[htbp]
+  \begin{center}
+  \includegraphics[scale=0.3]{popup1}
+  \end{center}
+  \caption{Hyperlink and tooltip for some formal entity.}
+  \end{figure}
+
+  Tooltip popups use the same rendering principles as the
   main text area, and further tooltips and/or hyperlinks may be
   exposed recursively by the same mechanism.
 
-  %FIXME screenshot of term "x = x" with typing/sorting
+  \begin{figure}[htbp]
+  \begin{center}
+  \includegraphics[scale=0.3]{popup2}
+  \end{center}
+  \caption{Nested tooltips over formal entities.}
+  \end{figure}
 *}
 
 
@@ -430,7 +449,7 @@
   Raw Unicode characters within prover source files should be
   restricted to informal parts, e.g.\ to write text in non-latin
   alphabets.  Mathematical symbols should be defined via the official
-  rendering tables, to avoid problems with portability and longterm
+  rendering tables, to avoid problems with portability and long-term
   storage of formal text.
 
   \paragraph{Control symbols.} There are some special control symbols
@@ -535,8 +554,8 @@
 
   \item \textbf{Problem:} Some Linux / X11 window managers that are
   not ``re-parenting'' cause problems with additional windows opened
-  by the Java VM. This affects either historic or neo-minimalistic
-  window managers like @{verbatim awesome} or @{verbatim xmonad}.
+  by Java. This affects either historic or neo-minimalistic window
+  managers like @{verbatim awesome} or @{verbatim xmonad}.
 
   \textbf{Workaround:} Use regular re-parenting window manager.
 
diff -r 2189d05622c4 -r 9e944630be0c src/Doc/JEdit/document/popup1.png
Binary file src/Doc/JEdit/document/popup1.png has changed
diff -r 2189d05622c4 -r 9e944630be0c src/Doc/JEdit/document/popup2.png
Binary file src/Doc/JEdit/document/popup2.png has changed
diff -r 2189d05622c4 -r 9e944630be0c src/Doc/ROOT
--- a/src/Doc/ROOT	Sat Oct 12 19:00:59 2013 +0200
+++ b/src/Doc/ROOT	Sat Oct 12 19:41:59 2013 +0200
@@ -148,16 +148,19 @@
   theories
     JEdit
   files
-    "../prepare_document"
     "../IsarRef/document/style.sty"
+    "../extra.sty"
+    "../iman.sty"
+    "../isar.sty"
+    "../manual.bib"
     "../pdfsetup.sty"
-    "../iman.sty"
-    "../extra.sty"
-    "../isar.sty"
+    "../prepare_document"
     "../ttbox.sty"
     "../underscore.sty"
-    "../manual.bib"
     "document/build"
+    "document/isabelle-jedit.png"
+    "document/popup1.png"
+    "document/popup2.png"
     "document/root.tex"
 
 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +