# HG changeset patch # User wenzelm # Date 1381408161 -7200 # Node ID 41951f427ac74c569c0045508eb2c9e6979e7cf3 # Parent b8bd31c7058c61186d44666395c0e6cb5a5fe361 more documentation; diff -r b8bd31c7058c -r 41951f427ac7 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Thu Oct 10 12:02:12 2013 +0200 +++ b/src/Doc/JEdit/JEdit.thy Thu Oct 10 14:29:21 2013 +0200 @@ -8,33 +8,57 @@ section {* Concepts and terminology *} -text {* FIXME +text {* Isabelle/jEdit is a Prover IDE that integrates \emph{parallel + proof checking} \cite{Wenzel:2009,Wenzel:2013:ITP} with + \emph{asynchronous user interaction} + \cite{Wenzel:2010,Wenzel:2012:UITP-EPTCS}, based on a + document-oriented approach to \emph{continuous proof processing} + \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system + components are fit together in order to make this work. The main + building blocks are as follows: -parallel proof checking \cite{Wenzel:2009} \cite{Wenzel:2013:ITP} + \begin{description} -asynchronous user interaction \cite{Wenzel:2010}, -\cite{Wenzel:2012:UITP-EPTCS} + \item [PIDE] is a general framework for Prover IDEs based on the + Isabelle/Scala. It is built around a concept of asynchronous + document processing, which is supported natively by the parallel + proof engine that is implemented in Isabelle/ML. The prover + discontinues the traditional TTY-based command loop in favor of + direct editing of formal source text. -document-oriented proof processing and Prover IDE \cite{Wenzel:2011:CICM} -\cite{Wenzel:2012} - -\begin{description} + \item [Isabelle/ML] is the implementation and extension language of + Isabelle, see also \cite{isabelle-implementation}. It is integrated + into the formal logical context and allows to manipulate logical + entities directly. Arbitrary add-on tools may be implemented for + object-logics such as Isabelle/HOL. -\item [PIDE] is a general framework for Prover IDEs based on the -Isabelle/Scala. It is built around a concept of \emph{asynchronous document -processing}, which is supported natively by the \emph{parallel proof engine} -that is implemented in Isabelle/ML. + \item [Isabelle/Scala] is the system programming language of + Isabelle. It extends the pure logical environment of Isabelle/ML + towards the ``real world'' of graphical user interfaces, text + editors, IDE frameworks, web services etc. Special infrastructure + allows to transfer algebraic datatypes and formatted text easily + between ML and Scala, using asynchronous protocol commands. + + \item [jEdit] is a sophisticated text + editor\footnote{\url{http://www.jedit.org}} implemented in Java. It + is easily extensible by plugins written in languages that work on + the JVM, e.g.\ Scala\footnote{\url{http://www.scala-lang.org/}}. -\item [jEdit] is a sophisticated text -editor\footnote{\url{http://www.jedit.org}} implemented in Java. It is easily -extensible by plugins written in languages that work on the JVM, e.g.\ -Scala\footnote{\url{http://www.scala-lang.org/}}. + \item [Isabelle/jEdit] is the main example application of the PIDE + framework and the default user-interface for Isabelle. It is + targeted at beginners and experts alike. Technically, Isabelle/jEdit + combines a slightly modified version of the official jEdit code base + with a special plugin for Isabelle, which is then integrated as + standalone application for the main operating system platforms: + Linux, Windows, Mac OS X. -\item [Isabelle/jEdit] is the main example application of the PIDE framework -and the default user-interface for Isabelle. It is targeted at beginners and -experts alike. + \end{description} -\end{description} + The subtle differences of Isabelle/ML versus Standard ML, + Isabelle/Scala versus Scala, Isabelle/jEdit versus regular jEdit + need to be taken into account when discussing any of these PIDE + building blocks on public forums, mailing lists, or even scientific + publications. *} @@ -43,41 +67,42 @@ text {* \includegraphics[width=\textwidth]{isabelle-jedit} - Isabelle/jEdit consists of some plugins for the well-known jEdit text - editor \url{http://www.jedit.org}, according to the following + Isabelle/jEdit consists of some plugins for the well-known jEdit + text editor \url{http://www.jedit.org}, according to the following principles. \begin{itemize} - \item The original jEdit look-and-feel is generally preserved, although - some default properties have been changed to accommodate Isabelle (e.g.\ - the text area font). + \item The original jEdit look-and-feel is generally preserved, + although some default properties have been changed to accommodate + Isabelle (e.g.\ the text area font). - \item Formal Isabelle/Isar text is checked asynchronously while editing. - The user is in full command of the editor, and the prover refrains from - locking portions of the buffer. + \item Formal Isabelle/Isar text is checked asynchronously while + editing. The user is in full command of the editor, and the prover + refrains from locking portions of the buffer. \item Prover feedback works via colors, boxes, squiggly underline, - hyperlinks, popup windows, icons, clickable output, all based on semantic - markup produced by Isabelle in the background. + hyperlinks, popup windows, icons, clickable output, all based on + semantic markup produced by Isabelle in the background. - \item Using the mouse together with the modifier key @{verbatim CONTROL} - (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes additional - formal content via tooltips and/or hyperlinks. + \item Using the mouse together with the modifier key @{verbatim + CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes + additional formal content via tooltips and/or hyperlinks. - \item Dockable panels (e.g. \emph{Output}, \emph{Symbols}) are managed as - independent windows by jEdit, which also allows multiple instances. + \item Dockable windows (e.g.\ \emph{Output}, \emph{Symbols}) are + managed separately by jEdit, which also allows multiple instances. - \item Formal output (in popups etc.) may be explored recursively, using - the same techniques as in the editor source buffer. + \item Formal output (in popups etc.) may be explored recursively, + using the same techniques as in the editor source buffer. - \item The prover process and source files are managed on the editor side. - The prover operates on timeless and stateless document content via - Isabelle/Scala. + \item The prover process and source files are managed on the editor + side. The prover operates on timeless and stateless document + content via Isabelle/Scala. - \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give access - to a selection of Isabelle/Scala options and its persistence preferences, - usually with immediate effect on the prover back-end or editor front-end. + \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give + access to a selection of Isabelle/Scala options and its persistence + preferences, usually with immediate effect on the prover back-end or + editor front-end. \item The logic image of the prover session may be specified within Isabelle/jEdit, but this requires restart. The new image is provided @@ -87,8 +112,160 @@ *} +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. + + Most of the information is relevant for Isabelle/jEdit as well, but + one needs to keep in mind that defaults sometimes differ, and the + official jEdit documentation does not know about the Isabelle plugin + with its bias towards theory editing. +*} + + +subsection {* Plugins *} + +text {* The \emph{Plugin Manager} of jEdit allows to augment editor + functionality by JVM modules (jars) that are provided by the central + plugin repository, or one of various mirror sites. The main + \emph{Isabelle} plugin that is bundled with Isabelle/jEdit needs to + remain active at all times! A few additional plugins are bundled + with Isabelle/jEdit for convenience or out of necessity, notably + \emph{Console} with its Isabelle/Scala sub-plugin and + \emph{SideKick} with some Isabelle-specific parsers for tree + structure. + + Connecting to the plugin server infrastructure of the jEdit project + allows to update bundled plugins or to add further + functionality. This needs to be done with the usual care for such an + open bazaar, with contributions of very mixed quality. Arbitrary + combinations of add-on features are apt to cause problems. + + It is advisable to start with the default configuration of + Isabelle/jEdit and develop some understanding how it is supposed to + work, before loading additional plugins at a grand scale. +*} + + +subsection {* Options *} + +text {* jEdit and Isabelle have separate management of persistent + options. Regular jEdit options are accessible via the dialogs for + \emph{Global Options} and \emph{Plugin Options}. This results in an + environment of name-value properties that is stored within the + \emph{settings directory} of jEdit; see also the menu + \emph{Utilities / Settings Directory}. + + In contrast, Isabelle system options are managed by Isabelle/Scala; + see also \cite{isabelle-sys}, especially the coverage of Isabelle + sessions and build. Options that are declared as \textbf{public} + are exposed to the \emph{Plugin Options} dialog of jEdit in its + section \emph{Isabelle / General}. This provides a view on Isabelle + options and persistent preferences in @{verbatim + "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit + properties in its settings directory. + + Isabelle options are loaded once on startup and saved on shutdown. + Editing the machine-generated @{verbatim "etc/preferences"} manually + while the application is running is likely to cause a lost-update! + + Some Isabelle options that are accessible in the Isabelle/jEdit + Plugin Options dialog affect general parameters that are relevant + outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or + @{system_option parallel_proofs} for the Isabelle build tool + \cite{isabelle-sys}. +*} + + +subsection {* Keymaps *} + +text {* Keyboard shortcuts used to be managed as jEdit properties in + the past, but recent versions (2013) have a separate concept of + \emph{keymap}. The ``imported'' keymap is produced initially from + the environment of properties that is available at the first start + of the editor. + + This is relevant for Isabelle/jEdit due to various fine-tuning of + default properties, and additional keyboard shortcuts for Isabelle + specific functionality. Users may change their keymap later on, but + may need to copy important key bindings manually. +*} + + +section {* Platform look-and-feel *} + +text {* jEdit is a Java/Swing application with some ambition to + support ``native'' platform look-and-feel, within the limits of what + Oracle as Java provider and major operating system vendors and + distributors allow. + + Isabelle/jEdit uses platform-specific look-and-feel as follows: + + \begin{description} + + \item[Linux] The platform-independent \emph{Nimbus} is used by + default, but the classic \emph{Metal} also works. + + Quasi-native \emph{GTK+} works under the side-condition that the + overall GTK theme is selected in a Java/Swing friendly way: the + success rate is @{text "\"} 50\%. + + \item[Windows] Regular \emph{Windows} is used by default, but + platform-independent \emph{Nimbus} and \emph{Metal} also work. + + \item[Mac OS X] standard \emph{Apple Aqua} is used by default. + Moreover the bundled \emph{MacOSX} plugin provides various functions + that are expected from applications on that particular platform: + quit from menu or dock, preferences menu, drag-and-drop of text + files on the application, full-screen mode for main editor windows + etc. + + \end{description} + + Users may experiment with different look-and-feels, but need to keep + in mind that this extra dimension of GUI functionality is unlikely + to work in arbitrary combinations. The \emph{GTK+} look-and-feel is + particularly critical due to its additional dimension of ``themes''. + It is also important to ensure that the fonts of standard GUI + components use anti-aliasing as usual. + + After changing the look-and-feel in \emph{Global Options / + Appearance}, it is advisable to restart Isabelle/jEdit in order to + take full effect. +*} + + chapter {* Prover IDE functionality *} +section {* Main text area *} + +text {* + + Source files with \texttt{.thy} extension are treated specifically: + Isabelle/jEdit adds them to the formal document-model of Isabelle/PIDE, that + maintains semantic information provided by the prover in the background, + while the user is editing the text in the foreground. + + \medskip Physical rendering of document content draws from the + standard repertoire of known IDEs for programming languages, with + highlighting, squiggles, tooltips, hyperlinks etc. In the above + screenshot, only the bold keywords of the Isar language use + traditional syntax-highlighting in jEdit with static tables; all + other coloring is based on dynamic information from the logical + context of the prover. + + Such annotated text regions can be explored further by using the + \texttt{CONTROL} modifier key (or \texttt{COMMAND} on Mac OS X), + together with mouse hovering or clicking. It reveals tooltips and + hyperlinks, e.g.\ see \texttt{constant "Example.path"} above, and + thus explains how a certain piece of source text has been + interpreted. + *} + + section {* Isabelle symbols and fonts *} text {* @@ -167,7 +344,7 @@ \medskip \begin{tabular}{lll} - \textbf{symbol} & style & keyboard shortcure \\ + \textbf{symbol} & style & keyboard shortcut \\\hline @{verbatim "\"} & superscript & @{verbatim "C+e UP"} \\ @{verbatim "\"} & subscript & @{verbatim "C+e DOWN"} \\ @{verbatim "\"} & bold face & @{verbatim "C+e RIGHT"} \\