more screenshots;
authorwenzelm
Sat Oct 12 19:41:59 2013 +0200 (2013-10-12)
changeset 543319e944630be0c
parent 54330 2189d05622c4
child 54332 a38160ad741c
more screenshots;
tuned;
src/Doc/JEdit/JEdit.thy
src/Doc/JEdit/document/popup1.png
src/Doc/JEdit/document/popup2.png
src/Doc/ROOT
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Sat Oct 12 19:00:59 2013 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Sat Oct 12 19:41:59 2013 +0200
     1.3 @@ -64,7 +64,12 @@
     1.4  section {* The Isabelle/jEdit Prover IDE *}
     1.5  
     1.6  text {*
     1.7 +  \begin{figure}[htbp]
     1.8 +  \begin{center}
     1.9    \includegraphics[width=\textwidth]{isabelle-jedit}
    1.10 +  \end{center}
    1.11 +  \caption{The Isabelle/jEdit Prover IDE}
    1.12 +  \end{figure}
    1.13  
    1.14    Isabelle/jEdit consists of some plugins for the well-known jEdit
    1.15    text editor \url{http://www.jedit.org}, according to the following
    1.16 @@ -299,11 +304,25 @@
    1.17    COMMAND} on Mac OS X.  Hovering with the mouse while the modifier is
    1.18    pressed reveals \emph{tooltips} (grey box within the text with a
    1.19    yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within
    1.20 -  the text).  Tooltip popups use the same rendering principles as the
    1.21 +  the text).
    1.22 +
    1.23 +  \begin{figure}[htbp]
    1.24 +  \begin{center}
    1.25 +  \includegraphics[scale=0.3]{popup1}
    1.26 +  \end{center}
    1.27 +  \caption{Hyperlink and tooltip for some formal entity.}
    1.28 +  \end{figure}
    1.29 +
    1.30 +  Tooltip popups use the same rendering principles as the
    1.31    main text area, and further tooltips and/or hyperlinks may be
    1.32    exposed recursively by the same mechanism.
    1.33  
    1.34 -  %FIXME screenshot of term "x = x" with typing/sorting
    1.35 +  \begin{figure}[htbp]
    1.36 +  \begin{center}
    1.37 +  \includegraphics[scale=0.3]{popup2}
    1.38 +  \end{center}
    1.39 +  \caption{Nested tooltips over formal entities.}
    1.40 +  \end{figure}
    1.41  *}
    1.42  
    1.43  
    1.44 @@ -430,7 +449,7 @@
    1.45    Raw Unicode characters within prover source files should be
    1.46    restricted to informal parts, e.g.\ to write text in non-latin
    1.47    alphabets.  Mathematical symbols should be defined via the official
    1.48 -  rendering tables, to avoid problems with portability and longterm
    1.49 +  rendering tables, to avoid problems with portability and long-term
    1.50    storage of formal text.
    1.51  
    1.52    \paragraph{Control symbols.} There are some special control symbols
    1.53 @@ -535,8 +554,8 @@
    1.54  
    1.55    \item \textbf{Problem:} Some Linux / X11 window managers that are
    1.56    not ``re-parenting'' cause problems with additional windows opened
    1.57 -  by the Java VM. This affects either historic or neo-minimalistic
    1.58 -  window managers like @{verbatim awesome} or @{verbatim xmonad}.
    1.59 +  by Java. This affects either historic or neo-minimalistic window
    1.60 +  managers like @{verbatim awesome} or @{verbatim xmonad}.
    1.61  
    1.62    \textbf{Workaround:} Use regular re-parenting window manager.
    1.63  
     2.1 Binary file src/Doc/JEdit/document/popup1.png has changed
     3.1 Binary file src/Doc/JEdit/document/popup2.png has changed
     4.1 --- a/src/Doc/ROOT	Sat Oct 12 19:00:59 2013 +0200
     4.2 +++ b/src/Doc/ROOT	Sat Oct 12 19:41:59 2013 +0200
     4.3 @@ -148,16 +148,19 @@
     4.4    theories
     4.5      JEdit
     4.6    files
     4.7 -    "../prepare_document"
     4.8      "../IsarRef/document/style.sty"
     4.9 +    "../extra.sty"
    4.10 +    "../iman.sty"
    4.11 +    "../isar.sty"
    4.12 +    "../manual.bib"
    4.13      "../pdfsetup.sty"
    4.14 -    "../iman.sty"
    4.15 -    "../extra.sty"
    4.16 -    "../isar.sty"
    4.17 +    "../prepare_document"
    4.18      "../ttbox.sty"
    4.19      "../underscore.sty"
    4.20 -    "../manual.bib"
    4.21      "document/build"
    4.22 +    "document/isabelle-jedit.png"
    4.23 +    "document/popup1.png"
    4.24 +    "document/popup2.png"
    4.25      "document/root.tex"
    4.26  
    4.27  session LaTeXsugar (doc) in "LaTeXsugar" = HOL +