equal
deleted
inserted
replaced
62 |
62 |
63 |
63 |
64 section {* The Isabelle/jEdit Prover IDE *} |
64 section {* The Isabelle/jEdit Prover IDE *} |
65 |
65 |
66 text {* |
66 text {* |
|
67 \begin{figure}[htbp] |
|
68 \begin{center} |
67 \includegraphics[width=\textwidth]{isabelle-jedit} |
69 \includegraphics[width=\textwidth]{isabelle-jedit} |
|
70 \end{center} |
|
71 \caption{The Isabelle/jEdit Prover IDE} |
|
72 \end{figure} |
68 |
73 |
69 Isabelle/jEdit consists of some plugins for the well-known jEdit |
74 Isabelle/jEdit consists of some plugins for the well-known jEdit |
70 text editor \url{http://www.jedit.org}, according to the following |
75 text editor \url{http://www.jedit.org}, according to the following |
71 principles. |
76 principles. |
72 |
77 |
297 Such formally annotated text can be explored further by using the |
302 Such formally annotated text can be explored further by using the |
298 @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim |
303 @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim |
299 COMMAND} on Mac OS X. Hovering with the mouse while the modifier is |
304 COMMAND} on Mac OS X. Hovering with the mouse while the modifier is |
300 pressed reveals \emph{tooltips} (grey box within the text with a |
305 pressed reveals \emph{tooltips} (grey box within the text with a |
301 yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within |
306 yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within |
302 the text). Tooltip popups use the same rendering principles as the |
307 the text). |
|
308 |
|
309 \begin{figure}[htbp] |
|
310 \begin{center} |
|
311 \includegraphics[scale=0.3]{popup1} |
|
312 \end{center} |
|
313 \caption{Hyperlink and tooltip for some formal entity.} |
|
314 \end{figure} |
|
315 |
|
316 Tooltip popups use the same rendering principles as the |
303 main text area, and further tooltips and/or hyperlinks may be |
317 main text area, and further tooltips and/or hyperlinks may be |
304 exposed recursively by the same mechanism. |
318 exposed recursively by the same mechanism. |
305 |
319 |
306 %FIXME screenshot of term "x = x" with typing/sorting |
320 \begin{figure}[htbp] |
|
321 \begin{center} |
|
322 \includegraphics[scale=0.3]{popup2} |
|
323 \end{center} |
|
324 \caption{Nested tooltips over formal entities.} |
|
325 \end{figure} |
307 *} |
326 *} |
308 |
327 |
309 |
328 |
310 section {* Isabelle symbols and fonts *} |
329 section {* Isabelle symbols and fonts *} |
311 |
330 |
428 \end{enumerate} |
447 \end{enumerate} |
429 |
448 |
430 Raw Unicode characters within prover source files should be |
449 Raw Unicode characters within prover source files should be |
431 restricted to informal parts, e.g.\ to write text in non-latin |
450 restricted to informal parts, e.g.\ to write text in non-latin |
432 alphabets. Mathematical symbols should be defined via the official |
451 alphabets. Mathematical symbols should be defined via the official |
433 rendering tables, to avoid problems with portability and longterm |
452 rendering tables, to avoid problems with portability and long-term |
434 storage of formal text. |
453 storage of formal text. |
435 |
454 |
436 \paragraph{Control symbols.} There are some special control symbols |
455 \paragraph{Control symbols.} There are some special control symbols |
437 to modify the style of a single symbol (without nesting). Control |
456 to modify the style of a single symbol (without nesting). Control |
438 symbols may be applied to a region of selected text, either using |
457 symbols may be applied to a region of selected text, either using |
533 variable @{verbatim XMODIFIERS} within Isabelle settings (default in |
552 variable @{verbatim XMODIFIERS} within Isabelle settings (default in |
534 Isabelle2013-1). |
553 Isabelle2013-1). |
535 |
554 |
536 \item \textbf{Problem:} Some Linux / X11 window managers that are |
555 \item \textbf{Problem:} Some Linux / X11 window managers that are |
537 not ``re-parenting'' cause problems with additional windows opened |
556 not ``re-parenting'' cause problems with additional windows opened |
538 by the Java VM. This affects either historic or neo-minimalistic |
557 by Java. This affects either historic or neo-minimalistic window |
539 window managers like @{verbatim awesome} or @{verbatim xmonad}. |
558 managers like @{verbatim awesome} or @{verbatim xmonad}. |
540 |
559 |
541 \textbf{Workaround:} Use regular re-parenting window manager. |
560 \textbf{Workaround:} Use regular re-parenting window manager. |
542 |
561 |
543 \item \textbf{Problem:} Recent forks of Linux / X11 window managers |
562 \item \textbf{Problem:} Recent forks of Linux / X11 window managers |
544 and desktop environments (variants of Gnome) disrupt the handling of |
563 and desktop environments (variants of Gnome) disrupt the handling of |