wenzelm@61656: (*:maxLineLen=78:*) wenzelm@53981: wenzelm@53769: theory JEdit wenzelm@53769: imports Base wenzelm@53769: begin wenzelm@53769: wenzelm@58618: chapter \Introduction\ wenzelm@53769: wenzelm@58618: section \Concepts and terminology\ wenzelm@53770: wenzelm@58618: text \ wenzelm@61574: Isabelle/jEdit is a Prover IDE that integrates \<^emph>\parallel proof checking\ wenzelm@61574: @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\asynchronous user wenzelm@61574: interaction\ @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and wenzelm@61574: "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented wenzelm@61574: approach to \<^emph>\continuous proof processing\ @{cite "Wenzel:2011:CICM" and wenzelm@61574: "Wenzel:2012"}. Many concepts and system components are fit together in wenzelm@61574: order to make this work. The main building blocks are as follows. wenzelm@53769: wenzelm@61574: \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle, wenzelm@61574: see also @{cite "isabelle-implementation"}. It is integrated into the wenzelm@61574: logical context of Isabelle/Isar and allows to manipulate logical entities wenzelm@61574: directly. Arbitrary add-on tools may be implemented for object-logics such wenzelm@61574: as Isabelle/HOL. wenzelm@53770: wenzelm@61574: \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It wenzelm@62183: extends the pure logical environment of Isabelle/ML towards the outer wenzelm@62183: world of graphical user interfaces, text editors, IDE frameworks, web wenzelm@61574: services etc. Special infrastructure allows to transfer algebraic wenzelm@61574: datatypes and formatted text easily between ML and Scala, using wenzelm@61574: asynchronous protocol commands. wenzelm@54321: wenzelm@62183: \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It wenzelm@62183: is built around a concept of parallel and asynchronous document wenzelm@62183: processing, which is supported natively by the parallel proof engine that wenzelm@62183: is implemented in Isabelle/ML. The traditional prover command loop is wenzelm@62183: given up; instead there is direct support for editing of source text, with wenzelm@62183: rich formal markup for GUI rendering. wenzelm@62183: wenzelm@63680: \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\\<^url>\http://www.jedit.org\\ wenzelm@63680: implemented in Java\<^footnote>\\<^url>\http://www.java.com\\. It is easily extensible by wenzelm@63680: plugins written in any language that works on the JVM. In the context of wenzelm@63680: Isabelle this is always Scala\<^footnote>\\<^url>\http://www.scala-lang.org\\. wenzelm@53770: wenzelm@62183: \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the wenzelm@62183: default user-interface for Isabelle. It targets both beginners and wenzelm@62183: experts. Technically, Isabelle/jEdit consists of the original jEdit code wenzelm@62183: base with minimal patches and a special plugin for Isabelle. This is wenzelm@62183: integrated as a desktop application for the main operating system wenzelm@62183: families: Linux, Windows, Mac OS X. wenzelm@53770: wenzelm@62183: End-users of Isabelle download and run a standalone application that exposes wenzelm@62183: jEdit as a text editor on the surface. Thus there is occasionally a tendency wenzelm@62183: to apply the name ``jEdit'' to any of the Isabelle Prover IDE aspects, wenzelm@62183: without proper differentiation. When discussing these PIDE building blocks wenzelm@62183: in public forums, mailing lists, or even scientific publications, it is wenzelm@62183: particularly important to distinguish Isabelle/ML versus Standard ML, wenzelm@62183: Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit. wenzelm@58618: \ wenzelm@53770: wenzelm@53770: wenzelm@58618: section \The Isabelle/jEdit Prover IDE\ wenzelm@53770: wenzelm@58618: text \ wenzelm@62183: \begin{figure}[!htb] wenzelm@54331: \begin{center} wenzelm@57312: \includegraphics[scale=0.333]{isabelle-jedit} wenzelm@54331: \end{center} wenzelm@54331: \caption{The Isabelle/jEdit Prover IDE} wenzelm@54357: \label{fig:isabelle-jedit} wenzelm@54331: \end{figure} wenzelm@53773: wenzelm@57337: Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for wenzelm@57337: the jEdit text editor, while preserving its general look-and-feel as far as wenzelm@57337: possible. The main plugin is called ``Isabelle'' and has its own menu wenzelm@61477: \<^emph>\Plugins~/ Isabelle\ with access to several panels (see also wenzelm@61574: \secref{sec:dockables}), as well as \<^emph>\Plugins~/ Plugin Options~/ Isabelle\ wenzelm@61574: (see also \secref{sec:options}). wenzelm@53770: wenzelm@62183: The options allow to specify a logic session name, but the same selector is wenzelm@62183: also accessible in the \<^emph>\Theories\ panel (\secref{sec:theories}). After wenzelm@62183: application startup, the selected logic session image is provided wenzelm@62183: automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is wenzelm@62183: absent or outdated wrt.\ its sources, the build process updates it while the wenzelm@62183: text editor is running. Prover IDE functionality is only activated after wenzelm@62183: successful termination of the build process. A failure may require changing wenzelm@62183: some options and restart the application. Changing the logic session, or the wenzelm@62183: underlying ML system platform (32\,bit versus 64\,bit) requires a restart of wenzelm@62183: the application to take effect. wenzelm@53769: wenzelm@61415: \<^medskip> wenzelm@61574: The main job of the Prover IDE is to manage sources and their changes, wenzelm@61574: taking the logical structure as a formal document into account (see also wenzelm@61574: \secref{sec:document-model}). The editor and the prover are connected wenzelm@57337: asynchronously in a lock-free manner. The prover is free to organize the wenzelm@57337: checking of the formal text in parallel on multiple cores, and provides wenzelm@57337: feedback via markup, which is rendered in the editor via colors, boxes, wenzelm@57420: squiggly underlines, hyperlinks, popup windows, icons, clickable output etc. wenzelm@53770: wenzelm@61574: Using the mouse together with the modifier key \<^verbatim>\CONTROL\ (Linux, Windows) wenzelm@62183: or \<^verbatim>\COMMAND\ (Mac OS X) exposes formal content via tooltips and/or wenzelm@62183: hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in popups wenzelm@62183: etc.) may be explored recursively, using the same techniques as in the wenzelm@62183: editor source buffer. wenzelm@53770: wenzelm@57337: Thus the Prover IDE gives an impression of direct access to formal content wenzelm@57337: of the prover within the editor, but in reality only certain aspects are wenzelm@62183: exposed, according to the possibilities of the prover and its add-on tools. wenzelm@58618: \ wenzelm@53769: wenzelm@53770: wenzelm@58618: subsection \Documentation\ wenzelm@54321: wenzelm@58618: text \ wenzelm@62183: The \<^emph>\Documentation\ panel of Isabelle/jEdit provides access to some example wenzelm@62183: theory files and the standard Isabelle documentation. PDF files are opened wenzelm@62183: by regular desktop operations of the underlying platform. The section wenzelm@62183: ``Original jEdit Documentation'' contains the original \<^emph>\User's Guide\ of wenzelm@62183: this sophisticated text editor. The same is accessible via the \<^verbatim>\Help\ menu wenzelm@62183: or \<^verbatim>\F1\ keyboard shortcut, using the built-in HTML viewer of Java/Swing. wenzelm@62183: The latter also includes \<^emph>\Frequently Asked Questions\ and documentation of wenzelm@62183: individual plugins. wenzelm@54321: wenzelm@62183: Most of the information about jEdit is relevant for Isabelle/jEdit as well, wenzelm@62183: but one needs to keep in mind that defaults sometimes differ, and the wenzelm@62183: official jEdit documentation does not know about the Isabelle plugin with wenzelm@62183: its support for continuous checking of formal source text: jEdit is a plain wenzelm@62183: text editor, but Isabelle/jEdit is a Prover IDE. wenzelm@58618: \ wenzelm@54321: wenzelm@54321: wenzelm@58618: subsection \Plugins\ wenzelm@54321: wenzelm@58618: text \ wenzelm@61574: The \<^emph>\Plugin Manager\ of jEdit allows to augment editor functionality by JVM wenzelm@61574: modules (jars) that are provided by the central plugin repository, which is wenzelm@61574: accessible via various mirror sites. wenzelm@54321: wenzelm@57420: Connecting to the plugin server-infrastructure of the jEdit project allows wenzelm@57420: to update bundled plugins or to add further functionality. This needs to be wenzelm@57420: done with the usual care for such an open bazaar of contributions. Arbitrary wenzelm@57420: combinations of add-on features are apt to cause problems. It is advisable wenzelm@57420: to start with the default configuration of Isabelle/jEdit and develop some wenzelm@64513: sense how it is meant to work, before loading too many other plugins. wenzelm@54321: wenzelm@61415: \<^medskip> wenzelm@61574: The main \<^emph>\Isabelle\ plugin is an integral part of Isabelle/jEdit and needs wenzelm@61574: to remain active at all times! A few additional plugins are bundled with wenzelm@61574: Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\Console\ with wenzelm@61574: its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\SideKick\ wenzelm@61574: with some Isabelle-specific parsers for document tree structure wenzelm@61574: (\secref{sec:sidekick}). The \<^emph>\Navigator\ plugin is particularly important wenzelm@61574: for hyperlinks within the formal document-model wenzelm@61574: (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\ErrorList\, wenzelm@61574: \<^emph>\Code2HTML\) are included to saturate the dependencies of bundled plugins, wenzelm@61574: but have no particular use in Isabelle/jEdit. wenzelm@58618: \ wenzelm@54321: wenzelm@54321: wenzelm@58618: subsection \Options \label{sec:options}\ wenzelm@54321: wenzelm@61574: text \ wenzelm@61574: Both jEdit and Isabelle have distinctive management of persistent options. wenzelm@54321: wenzelm@61574: Regular jEdit options are accessible via the dialogs \<^emph>\Utilities~/ Global wenzelm@61574: Options\ or \<^emph>\Plugins~/ Plugin Options\, with a second chance to flip the wenzelm@63669: two within the central options dialog. Changes are stored in @{path wenzelm@63749: "$JEDIT_SETTINGS/properties"} and @{path "$JEDIT_SETTINGS/keymaps"}. wenzelm@57310: wenzelm@57310: Isabelle system options are managed by Isabelle/Scala and changes are stored wenzelm@63669: in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of wenzelm@60270: other jEdit properties. See also @{cite "isabelle-system"}, especially the wenzelm@57310: coverage of sessions and command-line tools like @{tool build} or @{tool wenzelm@54372: options}. wenzelm@54321: wenzelm@62183: Those Isabelle options that are declared as \<^verbatim>\public\ are configurable in wenzelm@61574: Isabelle/jEdit via \<^emph>\Plugin Options~/ Isabelle~/ General\. Moreover, there wenzelm@61574: are various options for rendering of document content, which are wenzelm@61574: configurable via \<^emph>\Plugin Options~/ Isabelle~/ Rendering\. Thus \<^emph>\Plugin wenzelm@61574: Options~/ Isabelle\ in jEdit provides a view on a subset of Isabelle system wenzelm@61574: options. Note that some of these options affect general parameters that are wenzelm@61574: relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or wenzelm@61574: @{system_option parallel_proofs} for the Isabelle build tool @{cite wenzelm@61574: "isabelle-system"}, but it is possible to use the settings variable wenzelm@61574: @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds wenzelm@62183: without affecting the Prover IDE. wenzelm@54329: wenzelm@57627: The jEdit action @{action_def isabelle.options} opens the options dialog for wenzelm@57627: the Isabelle plugin; it can be mapped to editor GUI elements as usual. wenzelm@57627: wenzelm@61415: \<^medskip> wenzelm@61415: Options are usually loaded on startup and saved on shutdown of wenzelm@63669: Isabelle/jEdit. Editing the machine-generated @{path wenzelm@63749: "$JEDIT_SETTINGS/properties"} or @{path wenzelm@57310: "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is wenzelm@61574: running is likely to cause surprise due to lost update! wenzelm@61574: \ wenzelm@54321: wenzelm@54321: wenzelm@58618: subsection \Keymaps\ wenzelm@54321: wenzelm@61574: text \ wenzelm@62183: Keyboard shortcuts are managed as a separate concept of \<^emph>\keymap\ that is wenzelm@61574: configurable via \<^emph>\Global Options~/ Shortcuts\. The \<^verbatim>\imported\ keymap is wenzelm@61574: derived from the initial environment of properties that is available at the wenzelm@62183: first start of the editor; afterwards the keymap file takes precedence and wenzelm@62183: is no longer affected by change of default properties. wenzelm@54321: wenzelm@64513: Users may change their keymap later, but need to keep its content @{path wenzelm@64513: "$JEDIT_SETTINGS/keymaps"} in sync with \<^verbatim>\shortcut\ properties in wenzelm@64513: \<^file>\$JEDIT_HOME/src/jEdit.props\. wenzelm@64513: wenzelm@64513: \<^medskip> wenzelm@64513: The action @{action_def "isabelle.keymap-merge"} helps to resolve pending wenzelm@64513: Isabelle keymap changes that are in conflict with the current jEdit keymap; wenzelm@64513: non-conflicting changes are always applied implicitly. This action is wenzelm@64513: automatically invoked on Isabelle/jEdit startup. wenzelm@58618: \ wenzelm@54321: wenzelm@54321: wenzelm@58618: section \Command-line invocation \label{sec:command-line}\ wenzelm@57320: wenzelm@58618: text \ wenzelm@62183: Isabelle/jEdit is normally invoked as a single-instance desktop application, wenzelm@62183: based on platform-specific executables for Linux, Windows, Mac OS X. wenzelm@62014: wenzelm@62183: It is also possible to invoke the Prover IDE on the command-line, with some wenzelm@62183: extra options and environment settings. The command-line usage of @{tool_def wenzelm@62183: jedit} is as follows: wenzelm@61408: @{verbatim [display] wenzelm@61408: \Usage: isabelle jedit [OPTIONS] [FILES ...] wenzelm@57320: wenzelm@57320: Options are: wenzelm@62039: -D NAME=X set JVM system property wenzelm@61132: -J OPTION add JVM runtime option wenzelm@57320: -b build only wenzelm@57320: -d DIR include session directory wenzelm@57320: -f fresh build wenzelm@61132: -j OPTION add jEdit runtime option wenzelm@61132: -l NAME logic image name wenzelm@57320: -m MODE add print mode for output wenzelm@57320: -n no build of session image on startup wenzelm@63987: -p CMD ML process command prefix (process policy) wenzelm@57320: -s system build mode for session image wenzelm@57320: wenzelm@61512: Start jEdit with Isabelle plugin setup and open FILES wenzelm@61512: (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\} wenzelm@57320: wenzelm@61574: The \<^verbatim>\-l\ option specifies the session name of the logic image to be used wenzelm@61574: for proof processing. Additional session root directories may be included wenzelm@61574: via option \<^verbatim>\-d\ to augment that name space of @{tool build} @{cite wenzelm@61574: "isabelle-system"}. wenzelm@57320: wenzelm@61574: By default, the specified image is checked and built on demand. The \<^verbatim>\-s\ wenzelm@61574: option determines where to store the result session image of @{tool build}. wenzelm@61574: The \<^verbatim>\-n\ option bypasses the implicit build process for the selected wenzelm@61574: session image. wenzelm@57320: wenzelm@61574: The \<^verbatim>\-m\ option specifies additional print modes for the prover process. wenzelm@61574: Note that the system option @{system_option_ref jedit_print_mode} allows to wenzelm@61574: do the same persistently (e.g.\ via the \<^emph>\Plugin Options\ dialog of wenzelm@61574: Isabelle/jEdit), without requiring command-line invocation. wenzelm@57320: wenzelm@61574: The \<^verbatim>\-J\ and \<^verbatim>\-j\ options allow to pass additional low-level options to wenzelm@61574: the JVM or jEdit, respectively. The defaults are provided by the Isabelle wenzelm@61574: settings environment @{cite "isabelle-system"}, but note that these only wenzelm@61574: work for the command-line tool described here, and not the regular wenzelm@61574: application. wenzelm@57320: wenzelm@62039: The \<^verbatim>\-D\ option allows to define JVM system properties; this is passed wenzelm@62039: directly to the underlying \<^verbatim>\java\ process. wenzelm@62039: wenzelm@61574: The \<^verbatim>\-b\ and \<^verbatim>\-f\ options control the self-build mechanism of wenzelm@61574: Isabelle/jEdit. This is only relevant for building from sources, which also wenzelm@63680: requires an auxiliary \<^verbatim>\jedit_build\ component from wenzelm@63680: \<^url>\http://isabelle.in.tum.de/components\. The official Isabelle release wenzelm@62014: already includes a pre-built version of Isabelle/jEdit. wenzelm@62014: wenzelm@62183: \<^bigskip> wenzelm@62014: It is also possible to connect to an already running Isabelle/jEdit process wenzelm@62014: via @{tool_def jedit_client}: wenzelm@62014: @{verbatim [display] wenzelm@62014: \Usage: isabelle jedit_client [OPTIONS] [FILES ...] wenzelm@62014: wenzelm@62014: Options are: wenzelm@62014: -c only check presence of server wenzelm@62014: -n only report server name wenzelm@62014: -s NAME server name (default Isabelle) wenzelm@62014: wenzelm@62014: Connect to already running Isabelle/jEdit instance and open FILES\} wenzelm@62014: wenzelm@62014: The \<^verbatim>\-c\ option merely checks the presence of the server, producing a wenzelm@62183: process return code accordingly. wenzelm@62014: wenzelm@62014: The \<^verbatim>\-n\ option reports the server name, and the \<^verbatim>\-s\ option provides a wenzelm@62014: different server name. The default server name is the official distribution wenzelm@64513: name (e.g.\ \<^verbatim>\Isabelle2016-1\). Thus @{tool jedit_client} can connect to the wenzelm@62183: Isabelle desktop application without further options. wenzelm@62014: wenzelm@63987: The \<^verbatim>\-p\ option allows to override the implicit default of the system wenzelm@63987: option @{system_option_ref ML_process_policy} for ML processes started by wenzelm@63987: the Prover IDE, e.g. to control CPU affinity on multiprocessor systems. wenzelm@63987: wenzelm@62036: The JVM system property \<^verbatim>\isabelle.jedit_server\ provides a different server wenzelm@62183: name, e.g.\ use \<^verbatim>\isabelle jedit -Disabelle.jedit_server=\\name\ and wenzelm@62036: \<^verbatim>\isabelle jedit_client -s\~\name\ to connect later on. wenzelm@62014: \ wenzelm@57320: wenzelm@57320: wenzelm@60291: section \GUI rendering\ wenzelm@60291: wenzelm@60291: subsection \Look-and-feel \label{sec:look-and-feel}\ wenzelm@54321: wenzelm@60291: text \ wenzelm@60291: jEdit is a Java/AWT/Swing application with some ambition to support wenzelm@60291: ``native'' look-and-feel on all platforms, within the limits of what Oracle wenzelm@60291: as Java provider and major operating system distributors allow (see also wenzelm@60291: \secref{sec:problems}). wenzelm@54321: wenzelm@54329: Isabelle/jEdit enables platform-specific look-and-feel by default as wenzelm@57420: follows. wenzelm@54321: wenzelm@61574: \<^descr>[Linux:] The platform-independent \<^emph>\Metal\ is used by default. wenzelm@54321: wenzelm@62183: The Linux-specific \<^emph>\GTK+\ also works under the side-condition that the wenzelm@62183: overall GTK theme and options are selected in a way that works with Java wenzelm@62183: AWT/Swing. The JVM has no direct influence of GTK rendering. wenzelm@54321: wenzelm@62183: \<^descr>[Windows:] Regular \<^emph>\Windows\ is used by default. wenzelm@54372: wenzelm@61574: \<^descr>[Mac OS X:] Regular \<^emph>\Mac OS X\ is used by default. wenzelm@54321: wenzelm@61574: The bundled \<^emph>\MacOSX\ plugin provides various functions that are expected wenzelm@61574: from applications on that particular platform: quit from menu or dock, wenzelm@61574: preferences menu, drag-and-drop of text files on the application, wenzelm@61574: full-screen mode for main editor windows. It is advisable to have the wenzelm@61574: \<^emph>\MacOSX\ plugin enabled all the time on that platform. wenzelm@54321: wenzelm@62183: Users may experiment with different Swing look-and-feels, but need to keep wenzelm@62183: in mind that this extra variance of GUI functionality is unlikely to work in wenzelm@61574: arbitrary combinations. The platform-independent \<^emph>\Metal\ and \<^emph>\Nimbus\ wenzelm@62183: should always work on all platforms, although they are technically and wenzelm@62212: stylistically outdated. The historic \<^emph>\CDE/Motif\ should be ignored. wenzelm@54372: wenzelm@62183: After changing the look-and-feel in \<^emph>\Global Options~/ Appearance\, wenzelm@62183: Isabelle/jEdit should be restarted to take full effect. wenzelm@60291: \ wenzelm@60291: wenzelm@60291: wenzelm@60291: subsection \Displays with very high resolution \label{sec:hdpi}\ wenzelm@60291: wenzelm@60291: text \ wenzelm@62183: In distant past, displays with $1024 \times 768$ or $1280 \times 1024$ wenzelm@62183: pixels were considered ``high resolution'' and bitmap fonts with 12 or 14 wenzelm@62183: pixels as adequate for text rendering. In 2016, we routinely see much higher wenzelm@62183: resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' / wenzelm@62183: ``4K'' at $3840 \times 2160$. wenzelm@60291: wenzelm@62183: GUI frameworks are usually lagging behind, with hard-wired icon sizes and wenzelm@62183: tiny fonts. Java and jEdit do provide reasonable support for very high wenzelm@62183: resolution, but this requires manual adjustments as described below. wenzelm@60291: wenzelm@61415: \<^medskip> wenzelm@62183: The \<^bold>\operating-system\ usually provides some configuration for global wenzelm@62183: scaling of text fonts, e.g.\ $120\%$--$250\%$ on Windows. This impacts wenzelm@62183: regular GUI elements, when used with native look-and-feel: Linux \<^emph>\GTK+\, wenzelm@62183: \<^emph>\Windows\, \<^emph>\Mac OS X\, respectively. Alternatively, it is possible to use wenzelm@62183: the platform-independent \<^emph>\Metal\ look-and-feel and readjust its main font wenzelm@62183: sizes via jEdit options explained below. The Isabelle/jEdit \<^bold>\application\ wenzelm@62183: provides further options to adjust font sizes in particular GUI elements. wenzelm@62183: Here is a summary of all relevant font properties: wenzelm@60291: wenzelm@61574: \<^item> \<^emph>\Global Options / Text Area / Text font\: the main text area font, wenzelm@61574: which is also used as reference point for various derived font sizes, wenzelm@62185: e.g.\ the \<^emph>\Output\ (\secref{sec:output}) and \<^emph>\State\ wenzelm@62183: (\secref{sec:state-output}) panels. wenzelm@60291: wenzelm@61574: \<^item> \<^emph>\Global Options / Gutter / Gutter font\: the font for the gutter area wenzelm@61574: left of the main text area, e.g.\ relevant for display of line numbers wenzelm@61574: (disabled by default). wenzelm@60291: wenzelm@61574: \<^item> \<^emph>\Global Options / Appearance / Button, menu and label font\ as well as wenzelm@61574: \<^emph>\List and text field font\: this specifies the primary and secondary font wenzelm@62183: for the \<^emph>\Metal\ look-and-feel (\secref{sec:look-and-feel}). wenzelm@60291: wenzelm@61574: \<^item> \<^emph>\Plugin Options / Isabelle / General / Reset Font Size\: the main text wenzelm@61574: area font size for action @{action_ref "isabelle.reset-font-size"}, e.g.\ wenzelm@62183: relevant for quick scaling like in common web browsers. wenzelm@60291: wenzelm@61574: \<^item> \<^emph>\Plugin Options / Console / General / Font\: the console window font, wenzelm@61574: e.g.\ relevant for Isabelle/Scala command-line. wenzelm@60291: wenzelm@61574: In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\Metal\ look-and-feel is configured wenzelm@61574: with custom fonts at 30 pixels, and the main text area and console at 36 wenzelm@62183: pixels. This leads to decent rendering quality, despite the old-fashioned wenzelm@62183: appearance of \<^emph>\Metal\. wenzelm@60291: wenzelm@62183: \begin{figure}[!htb] wenzelm@60291: \begin{center} wenzelm@60291: \includegraphics[width=\textwidth]{isabelle-jedit-hdpi} wenzelm@60291: \end{center} wenzelm@60291: \caption{Metal look-and-feel with custom fonts for very high resolution} wenzelm@60291: \label{fig:isabelle-jedit-hdpi} wenzelm@60291: \end{figure} wenzelm@60291: \ wenzelm@54321: wenzelm@54321: wenzelm@62183: chapter \Augmented jEdit functionality\ wenzelm@62183: wenzelm@58618: section \Dockable windows \label{sec:dockables}\ wenzelm@57316: wenzelm@58618: text \ wenzelm@61574: In jEdit terminology, a \<^emph>\view\ is an editor window with one or more \<^emph>\text wenzelm@61574: areas\ that show the content of one or more \<^emph>\buffers\. A regular view may wenzelm@61574: be surrounded by \<^emph>\dockable windows\ that show additional information in wenzelm@61574: arbitrary format, not just text; a \<^emph>\plain view\ does not allow dockables. wenzelm@61574: The \<^emph>\dockable window manager\ of jEdit organizes these dockable windows, wenzelm@61574: either as \<^emph>\floating\ windows, or \<^emph>\docked\ panels within one of the four wenzelm@61574: margins of the view. There may be any number of floating instances of some wenzelm@61574: dockable window, but at most one docked instance; jEdit actions that address wenzelm@61574: \<^emph>\the\ dockable window of a particular kind refer to the unique docked wenzelm@61574: instance. wenzelm@57316: wenzelm@57316: Dockables are used routinely in jEdit for important functionality like wenzelm@61574: \<^emph>\HyperSearch Results\ or the \<^emph>\File System Browser\. Plugins often provide wenzelm@62184: a central dockable to access their main functionality, which may be opened wenzelm@62184: by the user on demand. The Isabelle/jEdit plugin takes this approach to the wenzelm@61574: extreme: its plugin menu provides the entry-points to many panels that are wenzelm@61574: managed as dockable windows. Some important panels are docked by default, wenzelm@62184: e.g.\ \<^emph>\Documentation\, \<^emph>\State\, \<^emph>\Theories\ \<^emph>\Output\, \<^emph>\Query\. The user wenzelm@62184: can change this arrangement easily and persistently. wenzelm@57316: wenzelm@57316: Compared to plain jEdit, dockable window management in Isabelle/jEdit is wenzelm@57316: slightly augmented according to the the following principles: wenzelm@57316: wenzelm@61477: \<^item> Floating windows are dependent on the main window as \<^emph>\dialog\ in wenzelm@57316: the sense of Java/AWT/Swing. Dialog windows always stay on top of the view, wenzelm@57316: which is particularly important in full-screen mode. The desktop environment wenzelm@57316: of the underlying platform may impose further policies on such dependent wenzelm@57316: dialogs, in contrast to fully independent windows, e.g.\ some window wenzelm@57316: management functions may be missing. wenzelm@57316: wenzelm@61415: \<^item> Keyboard focus of the main view vs.\ a dockable window is carefully wenzelm@57316: managed according to the intended semantics, as a panel mainly for output or wenzelm@62184: input. For example, activating the \<^emph>\Output\ (\secref{sec:output}) or State wenzelm@62184: (\secref{sec:state-output}) panel via the dockable window manager returns wenzelm@62184: keyboard focus to the main text area, but for \<^emph>\Query\ (\secref{sec:query}) wenzelm@62184: or \<^emph>\Sledgehammer\ \secref{sec:sledgehammer} the focus is given to the main wenzelm@62184: input field of that panel. wenzelm@57316: wenzelm@61415: \<^item> Panels that provide their own text area for output have an additional wenzelm@61477: dockable menu item \<^emph>\Detach\. This produces an independent copy of the wenzelm@61477: current output as a floating \<^emph>\Info\ window, which displays that content wenzelm@57316: independently of ongoing changes of the PIDE document-model. Note that wenzelm@57316: Isabelle/jEdit popup windows (\secref{sec:tooltips-hyperlinks}) provide a wenzelm@61477: similar \<^emph>\Detach\ operation as an icon. wenzelm@58618: \ wenzelm@57316: wenzelm@57316: wenzelm@58618: section \Isabelle symbols \label{sec:symbols}\ wenzelm@57319: wenzelm@58618: text \ wenzelm@61477: Isabelle sources consist of \<^emph>\symbols\ that extend plain ASCII to allow wenzelm@57420: infinitely many mathematical symbols within the formal sources. This works wenzelm@57420: without depending on particular encodings and varying Unicode wenzelm@61574: standards.\<^footnote>\Raw Unicode characters within formal sources would compromise wenzelm@61574: portability and reliability in the face of changing interpretation of wenzelm@61574: special features of Unicode, such as Combining Characters or Bi-directional wenzelm@62184: Text.\ See @{cite "Wenzel:2011:CICM"}. wenzelm@57319: wenzelm@57420: For the prover back-end, formal text consists of ASCII characters that are wenzelm@61574: grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\a\'' or symbolic wenzelm@61574: ``\<^verbatim>\\\''. For the editor front-end, a certain subset of symbols is rendered wenzelm@61574: physically via Unicode glyphs, in order to show ``\<^verbatim>\\\'' as ``\\\'', for wenzelm@61574: example. This symbol interpretation is specified by the Isabelle system wenzelm@63680: distribution in \<^file>\$ISABELLE_HOME/etc/symbols\ and may be augmented by the wenzelm@63680: user in @{path "$ISABELLE_HOME_USER/etc/symbols"}. wenzelm@57319: wenzelm@58554: The appendix of @{cite "isabelle-isar-ref"} gives an overview of the wenzelm@57319: standard interpretation of finitely many symbols from the infinite wenzelm@58554: collection. Uninterpreted symbols are displayed literally, e.g.\ wenzelm@61503: ``\<^verbatim>\\\''. Overlap of Unicode characters used in symbol wenzelm@58554: interpretation with informal ones (which might appear e.g.\ in comments) wenzelm@58554: needs to be avoided. Raw Unicode characters within prover source files wenzelm@58554: should be restricted to informal parts, e.g.\ to write text in non-latin wenzelm@58554: alphabets in comments. wenzelm@61506: \ wenzelm@57319: wenzelm@61506: paragraph \Encoding.\ wenzelm@62184: text \Technically, the Unicode interpretation of Isabelle symbols is an wenzelm@62184: \<^emph>\encoding\ called \<^verbatim>\UTF-8-Isabelle\ in jEdit (\<^emph>\not\ in the underlying wenzelm@62184: JVM). It is provided by the Isabelle/jEdit plugin and enabled by default for wenzelm@62184: all source files. Sometimes such defaults are reset accidentally, or wenzelm@62184: malformed UTF-8 sequences in the text force jEdit to fall back on a wenzelm@62184: different encoding like \<^verbatim>\ISO-8859-15\. In that case, verbatim ``\<^verbatim>\\\'' will wenzelm@62184: be shown in the text buffer instead of its Unicode rendering ``\\\''. The wenzelm@62184: jEdit menu operation \<^emph>\File~/ Reload with Encoding~/ UTF-8-Isabelle\ helps wenzelm@62184: to resolve such problems (after repairing malformed parts of the text). \ wenzelm@57319: wenzelm@61506: paragraph \Font.\ wenzelm@61506: text \Correct rendering via Unicode requires a font that contains glyphs for wenzelm@62184: the corresponding codepoints. There are also various unusual symbols with wenzelm@62184: particular purpose in Isabelle, e.g.\ control symbols and very long arrows. wenzelm@62184: Isabelle/jEdit prefers its own application fonts \<^verbatim>\IsabelleText\, which wenzelm@62184: ensures that standard collection of Isabelle symbols is actually shown on wenzelm@62184: the screen (or printer) as expected. wenzelm@57319: wenzelm@57420: Note that a Java/AWT/Swing application can load additional fonts only if wenzelm@57420: they are not installed on the operating system already! Some outdated wenzelm@61574: version of \<^verbatim>\IsabelleText\ that happens to be provided by the operating wenzelm@61574: system would prevent Isabelle/jEdit to use its bundled version. This could wenzelm@61574: lead to missing glyphs (black rectangles), when the system version of wenzelm@61574: \<^verbatim>\IsabelleText\ is older than the application version. This problem can be wenzelm@61574: avoided by refraining to ``install'' any version of \<^verbatim>\IsabelleText\ in the wenzelm@62184: first place, although it might be tempting to use the same font in other wenzelm@62184: applications. wenzelm@62184: wenzelm@62184: HTML pages generated by Isabelle refer to the same \<^verbatim>\IsabelleText\ font as a wenzelm@62184: server-side resource. Thus a web-browser can use that without requiring a wenzelm@62184: locally installed copy. wenzelm@61506: \ wenzelm@57319: wenzelm@61506: paragraph \Input methods.\ wenzelm@61506: text \In principle, Isabelle/jEdit could delegate the problem to produce wenzelm@61506: Isabelle symbols in their Unicode rendering to the underlying operating wenzelm@61506: system and its \<^emph>\input methods\. Regular jEdit also provides various ways to wenzelm@61506: work with \<^emph>\abbreviations\ to produce certain non-ASCII characters. Since wenzelm@61506: none of these standard input methods work satisfactorily for the wenzelm@61506: mathematical characters required for Isabelle, various specific wenzelm@61506: Isabelle/jEdit mechanisms are provided. wenzelm@57319: wenzelm@57420: This is a summary for practically relevant input methods for Isabelle wenzelm@57420: symbols. wenzelm@57319: wenzelm@61504: \<^enum> The \<^emph>\Symbols\ panel: some GUI buttons allow to insert certain symbols in wenzelm@61504: the text buffer. There are also tooltips to reveal the official Isabelle wenzelm@61504: representation with some additional information about \<^emph>\symbol wenzelm@61504: abbreviations\ (see below). wenzelm@57319: wenzelm@61504: \<^enum> Copy/paste from decoded source files: text that is rendered as Unicode wenzelm@61504: already can be re-used to produce further text. This also works between wenzelm@61504: different applications, e.g.\ Isabelle/jEdit and some web browser or mail wenzelm@62184: client, as long as the same Unicode interpretation of Isabelle symbols is wenzelm@62184: used. wenzelm@57319: wenzelm@61504: \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same principles wenzelm@61504: as for text buffers apply, but note that \<^emph>\copy\ in secondary Isabelle/jEdit wenzelm@61504: windows works via the keyboard shortcuts \<^verbatim>\C+c\ or \<^verbatim>\C+INSERT\, while jEdit wenzelm@61504: menu actions always refer to the primary text area! wenzelm@57319: wenzelm@62184: \<^enum> Completion provided by the Isabelle plugin (see \secref{sec:completion}). wenzelm@61504: Isabelle symbols have a canonical name and optional abbreviations. This can wenzelm@61504: be used with the text completion mechanism of Isabelle/jEdit, to replace a wenzelm@61504: prefix of the actual symbol like \<^verbatim>\\\, or its name preceded by backslash wenzelm@61504: \<^verbatim>\\lambda\, or its ASCII abbreviation \<^verbatim>\%\ by the Unicode rendering. wenzelm@57319: wenzelm@57319: The following table is an extract of the information provided by the wenzelm@63680: standard \<^file>\$ISABELLE_HOME/etc/symbols\ file: wenzelm@57319: wenzelm@61415: \<^medskip> wenzelm@57319: \begin{tabular}{lll} wenzelm@61477: \<^bold>\symbol\ & \<^bold>\name with backslash\ & \<^bold>\abbreviation\ \\\hline wenzelm@61503: \\\ & \<^verbatim>\\lambda\ & \<^verbatim>\%\ \\ wenzelm@61503: \\\ & \<^verbatim>\\Rightarrow\ & \<^verbatim>\=>\ \\ wenzelm@61503: \\\ & \<^verbatim>\\Longrightarrow\ & \<^verbatim>\==>\ \\[0.5ex] wenzelm@61503: \\\ & \<^verbatim>\\And\ & \<^verbatim>\!!\ \\ wenzelm@61503: \\\ & \<^verbatim>\\equiv\ & \<^verbatim>\==\ \\[0.5ex] wenzelm@61503: \\\ & \<^verbatim>\\forall\ & \<^verbatim>\!\ \\ wenzelm@61503: \\\ & \<^verbatim>\\exists\ & \<^verbatim>\?\ \\ wenzelm@61503: \\\ & \<^verbatim>\\longrightarrow\ & \<^verbatim>\-->\ \\ wenzelm@61503: \\\ & \<^verbatim>\\and\ & \<^verbatim>\&\ \\ wenzelm@61503: \\\ & \<^verbatim>\\or\ & \<^verbatim>\|\ \\ wenzelm@61503: \\\ & \<^verbatim>\\not\ & \<^verbatim>\~\ \\ wenzelm@61503: \\\ & \<^verbatim>\\noteq\ & \<^verbatim>\~=\ \\ wenzelm@61503: \\\ & \<^verbatim>\\in\ & \<^verbatim>\:\ \\ wenzelm@61503: \\\ & \<^verbatim>\\notin\ & \<^verbatim>\~:\ \\ wenzelm@57319: \end{tabular} wenzelm@61415: \<^medskip> wenzelm@61574: wenzelm@57420: Note that the above abbreviations refer to the input method. The logical wenzelm@57420: notation provides ASCII alternatives that often coincide, but sometimes wenzelm@62184: deviate. This occasionally causes user confusion with old-fashioned Isabelle wenzelm@62184: source that use ASCII replacement notation like \<^verbatim>\!\ or \<^verbatim>\ALL\ directly in wenzelm@62184: the text. wenzelm@57319: wenzelm@57319: On the other hand, coincidence of symbol abbreviations with ASCII wenzelm@61574: replacement syntax syntax helps to update old theory sources via explicit wenzelm@61574: completion (see also \<^verbatim>\C+b\ explained in \secref{sec:completion}). wenzelm@61506: \ wenzelm@57319: wenzelm@61506: paragraph \Control symbols.\ wenzelm@61506: text \There are some special control symbols to modify the display style of a wenzelm@61506: single symbol (without nesting). Control symbols may be applied to a region wenzelm@61506: of selected text, either using the \<^emph>\Symbols\ panel or keyboard shortcuts or wenzelm@61506: jEdit actions. These editor operations produce a separate control symbol for wenzelm@61506: each symbol in the text, in order to make the whole text appear in a certain wenzelm@61506: style. wenzelm@57319: wenzelm@61415: \<^medskip> wenzelm@57319: \begin{tabular}{llll} wenzelm@61477: \<^bold>\style\ & \<^bold>\symbol\ & \<^bold>\shortcut\ & \<^bold>\action\ \\\hline wenzelm@61503: superscript & \<^verbatim>\\<^sup>\ & \<^verbatim>\C+e UP\ & @{action_ref "isabelle.control-sup"} \\ wenzelm@61503: subscript & \<^verbatim>\\<^sub>\ & \<^verbatim>\C+e DOWN\ & @{action_ref "isabelle.control-sub"} \\ wenzelm@61503: bold face & \<^verbatim>\\<^bold>\ & \<^verbatim>\C+e RIGHT\ & @{action_ref "isabelle.control-bold"} \\ wenzelm@61503: emphasized & \<^verbatim>\\<^emph>\ & \<^verbatim>\C+e LEFT\ & @{action_ref "isabelle.control-emph"} \\ wenzelm@61503: reset & & \<^verbatim>\C+e BACK_SPACE\ & @{action_ref "isabelle.control-reset"} \\ wenzelm@57319: \end{tabular} wenzelm@61415: \<^medskip> wenzelm@61483: wenzelm@61483: To produce a single control symbol, it is also possible to complete on wenzelm@61504: \<^verbatim>\\sup\, \<^verbatim>\\sub\, \<^verbatim>\\bold\, \<^verbatim>\\emph\ as for regular symbols. wenzelm@61483: wenzelm@62184: The emphasized style only takes effect in document output (when used with a wenzelm@62184: cartouche), but not in the editor. wenzelm@58618: \ wenzelm@57319: wenzelm@57319: wenzelm@58618: section \Scala console \label{sec:scala-console}\ wenzelm@57319: wenzelm@58618: text \ wenzelm@61574: The \<^emph>\Console\ plugin manages various shells (command interpreters), e.g.\ wenzelm@61574: \<^emph>\BeanShell\, which is the official jEdit scripting language, and the wenzelm@61574: cross-platform \<^emph>\System\ shell. Thus the console provides similar wenzelm@61574: functionality than the Emacs buffers \<^verbatim>\*scratch*\ and \<^verbatim>\*shell*\. wenzelm@57319: wenzelm@61574: Isabelle/jEdit extends the repertoire of the console by \<^emph>\Scala\, which is wenzelm@61574: the regular Scala toplevel loop running inside the same JVM process as wenzelm@57420: Isabelle/jEdit itself. This means the Scala command interpreter has access wenzelm@57603: to the JVM name space and state of the running Prover IDE application. The wenzelm@61503: default environment imports the full content of packages \<^verbatim>\isabelle\ and wenzelm@61503: \<^verbatim>\isabelle.jedit\. wenzelm@57603: wenzelm@61574: For example, \<^verbatim>\PIDE\ refers to the Isabelle/jEdit plugin object, and \<^verbatim>\view\ wenzelm@61574: to the current editor view of jEdit. The Scala expression wenzelm@61574: \<^verbatim>\PIDE.snapshot(view)\ makes a PIDE document snapshot of the current buffer wenzelm@61574: within the current editor view. wenzelm@57319: wenzelm@57319: This helps to explore Isabelle/Scala functionality interactively. Some care wenzelm@57319: is required to avoid interference with the internals of the running wenzelm@62184: application. wenzelm@58618: \ wenzelm@57319: wenzelm@57319: wenzelm@58618: section \File-system access\ wenzelm@57318: wenzelm@58618: text \ wenzelm@57420: File specifications in jEdit follow various formats and conventions wenzelm@61477: according to \<^emph>\Virtual File Systems\, which may be also provided by wenzelm@61503: additional plugins. This allows to access remote files via the \<^verbatim>\http:\ wenzelm@61574: protocol prefix, for example. Isabelle/jEdit attempts to work with the wenzelm@61574: file-system model of jEdit as far as possible. In particular, theory sources wenzelm@61574: are passed directly from the editor to the prover, without indirection via wenzelm@61574: physical files. wenzelm@57318: wenzelm@57420: Despite the flexibility of URLs in jEdit, local files are particularly wenzelm@62184: important and are accessible without protocol prefix. The file path notation wenzelm@57420: is that of the Java Virtual Machine on the underlying platform. On Windows wenzelm@62184: the preferred form uses backslashes, but happens to accept forward slashes wenzelm@62184: like Unix/POSIX as well. Further differences arise due to Windows drive wenzelm@60257: letters and network shares. wenzelm@57318: wenzelm@57331: The Java notation for files needs to be distinguished from the one of wenzelm@61477: Isabelle, which uses POSIX notation with forward slashes on \<^emph>\all\ wenzelm@62184: platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and wenzelm@62184: driver letter representation as in Cygwin (e.g.\ \<^verbatim>\/cygdrive/c\). Moreover, wenzelm@62184: environment variables from the Isabelle process may be used freely, e.g.\ wenzelm@63680: \<^file>\$ISABELLE_HOME/etc/symbols\ or \<^file>\$POLYML_HOME/README\. There are special wenzelm@63680: shortcuts: \<^dir>\~\ for \<^dir>\$USER_HOME\ and \<^dir>\~~\ for \<^dir>\$ISABELLE_HOME\. wenzelm@57318: wenzelm@61415: \<^medskip> wenzelm@61415: Since jEdit happens to support environment variables within file wenzelm@57420: specifications as well, it is natural to use similar notation within the wenzelm@57420: editor, e.g.\ in the file-browser. This does not work in full generality, wenzelm@57420: though, due to the bias of jEdit towards platform-specific notation and of wenzelm@57420: Isabelle towards POSIX. Moreover, the Isabelle settings environment is not wenzelm@57420: yet active when starting Isabelle/jEdit via its standard application wenzelm@60257: wrapper, in contrast to @{tool jedit} run from the command line wenzelm@60257: (\secref{sec:command-line}). wenzelm@57318: wenzelm@63749: Isabelle/jEdit imitates important system settings within the Java process wenzelm@63749: environment, in order to allow easy access to these important places from wenzelm@63749: the editor: \<^verbatim>\$ISABELLE_HOME\, \<^verbatim>\$ISABELLE_HOME_USER\, \<^verbatim>\$JEDIT_HOME\, wenzelm@63749: \<^verbatim>\$JEDIT_SETTINGS\. The file browser of jEdit also includes \<^emph>\Favorites\ for wenzelm@63749: these two important locations. wenzelm@57318: wenzelm@61415: \<^medskip> wenzelm@61574: Path specifications in prover input or output usually include formal markup wenzelm@61574: that turns it into a hyperlink (see also \secref{sec:tooltips-hyperlinks}). wenzelm@61574: This allows to open the corresponding file in the text editor, independently wenzelm@62184: of the path notation. If the path refers to a directory, the jEdit file wenzelm@62184: browser is opened on it. wenzelm@57318: wenzelm@57318: Formally checked paths in prover input are subject to completion wenzelm@61574: (\secref{sec:completion}): partial specifications are resolved via directory wenzelm@61574: content and possible completions are offered in a popup. wenzelm@58618: \ wenzelm@57318: wenzelm@57318: wenzelm@62184: section \SideKick parsers \label{sec:sidekick}\ wenzelm@62184: wenzelm@62184: text \ wenzelm@62184: The \<^emph>\SideKick\ plugin provides some general services to display buffer wenzelm@62184: structure in a tree view. Isabelle/jEdit provides SideKick parsers for its wenzelm@64513: main mode for theory files, ML files, as well as some minor modes for the wenzelm@64513: \<^verbatim>\NEWS\ file (see \figref{fig:sidekick}), session \<^verbatim>\ROOT\ files, system wenzelm@64513: \<^verbatim>\options\, and Bib{\TeX} files (\secref{sec:bibtex}). wenzelm@62184: wenzelm@62184: \begin{figure}[!htb] wenzelm@62184: \begin{center} wenzelm@62184: \includegraphics[scale=0.333]{sidekick} wenzelm@62184: \end{center} wenzelm@62184: \caption{The Isabelle NEWS file with SideKick tree view} wenzelm@62184: \label{fig:sidekick} wenzelm@62184: \end{figure} wenzelm@62184: wenzelm@64513: The default SideKick parser for theory files is \<^verbatim>\isabelle\: it provides a wenzelm@64513: tree-view on the formal document structure, with section headings at the top wenzelm@64513: and formal specification elements at the bottom. The alternative parser wenzelm@64513: \<^verbatim>\isabelle-context\ shows nesting of context blocks according to \<^theory_text>\begin \ wenzelm@64513: end\ structure. wenzelm@64513: wenzelm@64513: \<^medskip> wenzelm@64513: Isabelle/ML files are structured according to semi-formal comments that are wenzelm@64513: explained in @{cite "isabelle-implementation"}. This outline is turned into wenzelm@64513: a tree-view by default, by using the \<^verbatim>\isabelle-ml\ parser. There is also a wenzelm@64513: folding mode of the same name, for hierarchic text folds within ML files. wenzelm@64513: wenzelm@64513: \<^medskip> wenzelm@62184: The special SideKick parser \<^verbatim>\isabelle-markup\ exposes the uninterpreted wenzelm@62184: markup tree of the PIDE document model of the current buffer. This is wenzelm@62184: occasionally useful for informative purposes, but the amount of displayed wenzelm@62184: information might cause problems for large buffers. wenzelm@62184: \ wenzelm@62184: wenzelm@62184: wenzelm@58618: chapter \Prover IDE functionality \label{sec:document-model}\ wenzelm@57315: wenzelm@58618: section \Document model \label{sec:document-model}\ wenzelm@57322: wenzelm@58618: text \ wenzelm@57322: The document model is central to the PIDE architecture: the editor and the wenzelm@57322: prover have a common notion of structured source text with markup, which is wenzelm@57322: produced by formal processing. The editor is responsible for edits of wenzelm@57322: document source, as produced by the user. The prover is responsible for wenzelm@57322: reports of document markup, as produced by its processing in the background. wenzelm@57322: wenzelm@57322: Isabelle/jEdit handles classic editor events of jEdit, in order to connect wenzelm@57322: the physical world of the GUI (with its singleton state) to the mathematical wenzelm@57322: world of multiple document versions (with timeless and stateless updates). wenzelm@58618: \ wenzelm@57322: wenzelm@54322: wenzelm@58618: subsection \Editor buffers and document nodes \label{sec:buffer-node}\ wenzelm@57322: wenzelm@58618: text \ wenzelm@61477: As a regular text editor, jEdit maintains a collection of \<^emph>\buffers\ to wenzelm@57322: store text files; each buffer may be associated with any number of visible wenzelm@61574: \<^emph>\text areas\. Buffers are subject to an \<^emph>\edit mode\ that is determined wenzelm@61574: from the file name extension. The following modes are treated specifically wenzelm@61574: in Isabelle/jEdit: wenzelm@57322: wenzelm@61415: \<^medskip> wenzelm@57322: \begin{tabular}{lll} wenzelm@62185: \<^bold>\mode\ & \<^bold>\file name\ & \<^bold>\content\ \\\hline wenzelm@62185: \<^verbatim>\isabelle\ & \<^verbatim>\*.thy\ & theory source \\ wenzelm@62185: \<^verbatim>\isabelle-ml\ & \<^verbatim>\*.ML\ & Isabelle/ML source \\ wenzelm@62185: \<^verbatim>\sml\ & \<^verbatim>\*.sml\ or \<^verbatim>\*.sig\ & Standard ML source \\ wenzelm@62185: \<^verbatim>\isabelle-root\ & \<^verbatim>\ROOT\ & session root \\ wenzelm@62185: \<^verbatim>\isabelle-options\ & & Isabelle options \\ wenzelm@62185: \<^verbatim>\isabelle-news\ & & Isabelle NEWS \\ wenzelm@57322: \end{tabular} wenzelm@61415: \<^medskip> wenzelm@54321: wenzelm@57322: All jEdit buffers are automatically added to the PIDE document-model as wenzelm@61574: \<^emph>\document nodes\. The overall document structure is defined by the theory wenzelm@61574: nodes in two dimensions: wenzelm@57322: wenzelm@61574: \<^enum> via \<^bold>\theory imports\ that are specified in the \<^emph>\theory header\ using wenzelm@61574: concrete syntax of the @{command_ref theory} command @{cite wenzelm@61574: "isabelle-isar-ref"}; wenzelm@57322: wenzelm@61574: \<^enum> via \<^bold>\auxiliary files\ that are loaded into a theory by special \<^emph>\load wenzelm@61574: commands\, notably @{command_ref ML_file} and @{command_ref SML_file} wenzelm@61574: @{cite "isabelle-isar-ref"}. wenzelm@54322: wenzelm@57322: In any case, source files are managed by the PIDE infrastructure: the wenzelm@57322: physical file-system only plays a subordinate role. The relevant version of wenzelm@60257: source text is passed directly from the editor to the prover, using internal wenzelm@57322: communication channels. wenzelm@58618: \ wenzelm@57322: wenzelm@57322: wenzelm@58618: subsection \Theories \label{sec:theories}\ wenzelm@57322: wenzelm@58618: text \ wenzelm@61574: The \<^emph>\Theories\ panel (see also \figref{fig:theories}) provides an overview wenzelm@61574: of the status of continuous checking of theory nodes within the document wenzelm@61574: model. Unlike batch sessions of @{tool build} @{cite "isabelle-system"}, wenzelm@61574: theory nodes are identified by full path names; this allows to work with wenzelm@61574: multiple (disjoint) Isabelle sessions simultaneously within the same editor wenzelm@61574: session. wenzelm@57322: wenzelm@62183: \begin{figure}[!htb] wenzelm@57339: \begin{center} wenzelm@57339: \includegraphics[scale=0.333]{theories} wenzelm@57339: \end{center} wenzelm@62185: \caption{Theories panel with an overview of the document-model, and jEdit wenzelm@62185: text areas as editable views on some of the document nodes} wenzelm@57339: \label{fig:theories} wenzelm@57339: \end{figure} wenzelm@57339: wenzelm@57322: Certain events to open or update editor buffers cause Isabelle/jEdit to wenzelm@57322: resolve dependencies of theory imports. The system requests to load wenzelm@57322: additional files into editor buffers, in order to be included in the wenzelm@57322: document model for further checking. It is also possible to let the system wenzelm@57420: resolve dependencies automatically, according to the system option wenzelm@57420: @{system_option jedit_auto_load}. wenzelm@54321: wenzelm@61415: \<^medskip> wenzelm@61574: The visible \<^emph>\perspective\ of Isabelle/jEdit is defined by the collective wenzelm@61574: view on theory buffers via open text areas. The perspective is taken as a wenzelm@61574: hint for document processing: the prover ensures that those parts of a wenzelm@61574: theory where the user is looking are checked, while other parts that are wenzelm@61574: presently not required are ignored. The perspective is changed by opening or wenzelm@61574: closing text area windows, or scrolling within a window. wenzelm@54322: wenzelm@61574: The \<^emph>\Theories\ panel provides some further options to influence the process wenzelm@61574: of continuous checking: it may be switched off globally to restrict the wenzelm@61574: prover to superficial processing of command syntax. It is also possible to wenzelm@61574: indicate theory nodes as \<^emph>\required\ for continuous checking: this means wenzelm@61574: such nodes and all their imports are always processed independently of the wenzelm@61574: visibility status (if continuous checking is enabled). Big theory libraries wenzelm@62185: that are marked as required can have significant impact on performance! wenzelm@54322: wenzelm@61415: \<^medskip> wenzelm@61574: Formal markup of checked theory content is turned into GUI rendering, based wenzelm@62185: on a standard repertoire known from mainstream IDEs for programming wenzelm@62185: languages: colors, icons, highlighting, squiggly underlines, tooltips, wenzelm@62185: hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional wenzelm@62185: syntax-highlighting via static keywords and tokenization within the editor; wenzelm@62185: this buffer syntax is determined from theory imports. In contrast, the wenzelm@62185: painting of inner syntax (term language etc.)\ uses semantic information wenzelm@62185: that is reported dynamically from the logical context. Thus the prover can wenzelm@62185: provide additional markup to help the user to understand the meaning of wenzelm@62185: formal text, and to produce more text with some add-on tools (e.g.\ wenzelm@62185: information messages with \<^emph>\sendback\ markup by automated provers or wenzelm@62185: disprovers in the background). \ wenzelm@57322: wenzelm@57322: wenzelm@58618: subsection \Auxiliary files \label{sec:aux-files}\ wenzelm@57322: wenzelm@58618: text \ wenzelm@57329: Special load commands like @{command_ref ML_file} and @{command_ref wenzelm@58554: SML_file} @{cite "isabelle-isar-ref"} refer to auxiliary files within some wenzelm@57329: theory. Conceptually, the file argument of the command extends the theory wenzelm@57329: source by the content of the file, but its editor buffer may be loaded~/ wenzelm@57329: changed~/ saved separately. The PIDE document model propagates changes of wenzelm@57329: auxiliary file content to the corresponding load command in the theory, to wenzelm@57329: update and process it accordingly: changes of auxiliary file content are wenzelm@57329: treated as changes of the corresponding load command. wenzelm@57323: wenzelm@61415: \<^medskip> wenzelm@61574: As a concession to the massive amount of ML files in Isabelle/HOL itself, wenzelm@61574: the content of auxiliary files is only added to the PIDE document-model on wenzelm@61574: demand, the first time when opened explicitly in the editor. There are wenzelm@61574: further tricks to manage markup of ML files, such that Isabelle/HOL may be wenzelm@61574: edited conveniently in the Prover IDE on small machines with only 8\,GB of wenzelm@61574: main memory. Using \<^verbatim>\Pure\ as logic session image, the exploration may start wenzelm@63680: at the top \<^file>\$ISABELLE_HOME/src/HOL/Main.thy\ or the bottom wenzelm@63680: \<^file>\$ISABELLE_HOME/src/HOL/HOL.thy\, for example. wenzelm@57323: wenzelm@57323: Initially, before an auxiliary file is opened in the editor, the prover wenzelm@57323: reads its content from the physical file-system. After the file is opened wenzelm@57323: for the first time in the editor, e.g.\ by following the hyperlink wenzelm@57323: (\secref{sec:tooltips-hyperlinks}) for the argument of its @{command wenzelm@57323: ML_file} command, the content is taken from the jEdit buffer. wenzelm@57323: wenzelm@57323: The change of responsibility from prover to editor counts as an update of wenzelm@57323: the document content, so subsequent theory sources need to be re-checked. wenzelm@57420: When the buffer is closed, the responsibility remains to the editor: the wenzelm@57420: file may be opened again without causing another document update. wenzelm@57323: wenzelm@57323: A file that is opened in the editor, but its theory with the load command is wenzelm@57323: not, is presently inactive in the document model. A file that is loaded via wenzelm@57323: multiple load commands is associated to an arbitrary one: this situation is wenzelm@57323: morally unsupported and might lead to confusion. wenzelm@57323: wenzelm@61415: \<^medskip> wenzelm@61574: Output that refers to an auxiliary file is combined with that of the wenzelm@61574: corresponding load command, and shown whenever the file or the command are wenzelm@61574: active (see also \secref{sec:output}). wenzelm@57323: wenzelm@57323: Warnings, errors, and other useful markup is attached directly to the wenzelm@62185: positions in the auxiliary file buffer, in the manner of standard IDEs. By wenzelm@63680: using the load command @{command SML_file} as explained in wenzelm@63680: \<^file>\$ISABELLE_HOME/src/Tools/SML/Examples.thy\, Isabelle/jEdit may be used as wenzelm@57323: fully-featured IDE for Standard ML, independently of theory or proof wenzelm@61574: development: the required theory merely serves as some kind of project file wenzelm@61574: for a collection of SML source modules. wenzelm@58618: \ wenzelm@54322: wenzelm@54352: wenzelm@58618: section \Output \label{sec:output}\ wenzelm@54353: wenzelm@58618: text \ wenzelm@61574: Prover output consists of \<^emph>\markup\ and \<^emph>\messages\. Both are directly wenzelm@61574: attached to the corresponding positions in the original source text, and wenzelm@61574: visualized in the text area, e.g.\ as text colours for free and bound wenzelm@61574: variables, or as squiggly underlines for warnings, errors etc.\ (see also wenzelm@61574: \figref{fig:output}). In the latter case, the corresponding messages are wenzelm@61574: shown by hovering with the mouse over the highlighted text --- although in wenzelm@61574: many situations the user should already get some clue by looking at the wenzelm@62185: position of the text highlighting, without seeing the message body itself. wenzelm@54357: wenzelm@62183: \begin{figure}[!htb] wenzelm@54357: \begin{center} wenzelm@57312: \includegraphics[scale=0.333]{output} wenzelm@54357: \end{center} wenzelm@62185: \caption{Multiple views on prover output: gutter with icon, text area with wenzelm@62185: popup, text overview column, \<^emph>\Theories\ panel, \<^emph>\Output\ panel} wenzelm@54357: \label{fig:output} wenzelm@54357: \end{figure} wenzelm@54353: wenzelm@62185: The ``gutter'' on the left-hand-side of the text area uses icons to wenzelm@62185: provide a summary of the messages within the adjacent text line. Message wenzelm@61574: priorities are used to prefer errors over warnings, warnings over wenzelm@62185: information messages; other output is ignored. wenzelm@54353: wenzelm@62185: The ``text overview column'' on the right-hand-side of the text area uses wenzelm@62185: similar information to paint small rectangles for the overall status of the wenzelm@62185: whole text buffer. The graphics is scaled to fit the logical buffer length wenzelm@62185: into the given window height. Mouse clicks on the overview area move the wenzelm@62185: cursor approximately to the corresponding text line in the buffer. wenzelm@54353: wenzelm@62185: The \<^emph>\Theories\ panel provides another course-grained overview, but without wenzelm@62185: direct correspondence to text positions. The coloured rectangles represent wenzelm@62185: the amount of messages of a certain kind (warnings, errors, etc.) and the wenzelm@62185: execution status of commands. A double-click on one of the theory entries wenzelm@62185: with their status overview opens the corresponding text buffer, without wenzelm@62185: moving the cursor to a specific point. wenzelm@54353: wenzelm@61415: \<^medskip> wenzelm@62185: The \<^emph>\Output\ panel displays prover messages that correspond to a given wenzelm@62185: command, within a separate window. The cursor position in the presently wenzelm@62185: active text area determines the prover command whose cumulative message wenzelm@62185: output is appended and shown in that window (in canonical order according to wenzelm@62185: the internal execution of the command). There are also control elements to wenzelm@62185: modify the update policy of the output wrt.\ continued editor movements: wenzelm@62185: \<^emph>\Auto update\ and \<^emph>\Update\. This is particularly useful for multiple wenzelm@62185: instances of the \<^emph>\Output\ panel to look at different situations. wenzelm@62185: Alternatively, the panel can be turned into a passive \<^emph>\Info\ window via the wenzelm@62185: \<^emph>\Detach\ menu item. wenzelm@54353: wenzelm@62185: Proof state is handled separately (\secref{sec:state-output}), but it is wenzelm@62185: also possible to tick the corresponding checkbox to append it to regular wenzelm@62185: output (\figref{fig:output-including-state}). This is a globally persistent wenzelm@62185: option: it affects all open panels and future editor sessions. wenzelm@54353: wenzelm@62185: \begin{figure}[!htb] wenzelm@62185: \begin{center} wenzelm@62185: \includegraphics[scale=0.333]{output-including-state} wenzelm@62185: \end{center} wenzelm@62185: \caption{Proof state display within the regular output panel} wenzelm@62185: \label{fig:output-including-state} wenzelm@62185: \end{figure} wenzelm@54353: wenzelm@61415: \<^medskip> wenzelm@62185: Following the IDE principle, regular messages are attached to the original wenzelm@62185: source in the proper place and may be inspected on demand via popups. This wenzelm@62185: excludes messages that are somehow internal to the machinery of proof wenzelm@62185: checking, notably \<^emph>\proof state\ and \<^emph>\tracing\. wenzelm@62185: wenzelm@62185: In any case, the same display technology is used for small popups and big wenzelm@62185: output windows. The formal text contains markup that may be explored wenzelm@62185: recursively via further popups and hyperlinks (see wenzelm@61574: \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain wenzelm@61574: actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}). wenzelm@61574: \ wenzelm@54353: wenzelm@54353: wenzelm@62185: section \Proof state \label{sec:state-output}\ wenzelm@62154: wenzelm@62154: text \ wenzelm@62185: The main purpose of the Prover IDE is to help the user editing proof wenzelm@62185: documents, with ongoing formal checking by the prover in the background. wenzelm@62185: This can be done to some extent in the main text area alone, especially for wenzelm@62185: well-structured Isar proofs. wenzelm@62185: wenzelm@62185: Nonetheless, internal proof state needs to be inspected in many situations wenzelm@62185: of exploration and ``debugging''. The \<^emph>\State\ panel shows exclusively such wenzelm@62185: proof state messages without further distraction, while all other messages wenzelm@62185: are displayed in \<^emph>\Output\ (\secref{sec:output}). wenzelm@62185: \Figref{fig:output-and-state} shows a typical GUI layout where both panels wenzelm@62185: are open. wenzelm@62154: wenzelm@62183: \begin{figure}[!htb] wenzelm@62154: \begin{center} wenzelm@62154: \includegraphics[scale=0.333]{output-and-state} wenzelm@62154: \end{center} wenzelm@62154: \caption{Separate proof state display (right) and other output (bottom).} wenzelm@62154: \label{fig:output-and-state} wenzelm@62154: \end{figure} wenzelm@62154: wenzelm@62185: Another typical arrangement has more than one \<^emph>\State\ panel open (as wenzelm@62185: floating windows), with \<^emph>\Auto update\ disabled to look at an old situation wenzelm@62185: while the proof text in the vicinity is changed. The \<^emph>\Update\ button wenzelm@62185: triggers an explicit one-shot update; this operation is also available via wenzelm@62185: the action @{action "isabelle.update-state"} (keyboard shortcut \<^verbatim>\S+ENTER\). wenzelm@62185: wenzelm@62185: On small screens, it is occasionally useful to have all messages wenzelm@62185: concatenated in the regular \<^emph>\Output\ panel, e.g.\ see wenzelm@62185: \figref{fig:output-including-state}. wenzelm@62185: wenzelm@62185: \<^medskip> wenzelm@62185: The mechanics of \<^emph>\Output\ versus \<^emph>\State\ are slightly different: wenzelm@62185: wenzelm@62185: \<^item> \<^emph>\Output\ shows information that is continuously produced and already wenzelm@62185: present when the GUI wants to show it. This is implicitly controlled by wenzelm@62185: the visible perspective on the text. wenzelm@62185: wenzelm@62185: \<^item> \<^emph>\State\ initiates a real-time query on demand, with a full round trip wenzelm@62185: including a fresh print operation on the prover side. This is controlled wenzelm@62185: explicitly when the cursor is moved to the next command (\<^emph>\Auto update\) wenzelm@62185: or the \<^emph>\Update\ operation is triggered. wenzelm@62185: wenzelm@62185: This can make a difference in GUI responsibility and resource usage within wenzelm@62185: the prover process. Applications with very big proof states that are only wenzelm@62185: inspected in isolation work better with the \<^emph>\State\ panel. wenzelm@62154: \ wenzelm@62154: wenzelm@62185: wenzelm@58618: section \Query \label{sec:query}\ wenzelm@57311: wenzelm@58618: text \ wenzelm@61574: The \<^emph>\Query\ panel provides various GUI forms to request extra information wenzelm@62249: from the prover, as a replacement of old-style diagnostic commands like wenzelm@62249: @{command find_theorems}. There are input fields and buttons for a wenzelm@62249: particular query command, with output in a dedicated text area. wenzelm@57311: wenzelm@62249: The main query modes are presented as separate tabs: \<^emph>\Find Theorems\, wenzelm@62249: \<^emph>\Find Constants\, \<^emph>\Print Context\, e.g.\ see \figref{fig:query}. As usual wenzelm@62249: in jEdit, multiple \<^emph>\Query\ windows may be active at the same time: any wenzelm@62249: number of floating instances, but at most one docked instance (which is used wenzelm@62249: by default). wenzelm@57313: wenzelm@62183: \begin{figure}[!htb] wenzelm@57313: \begin{center} wenzelm@57313: \includegraphics[scale=0.333]{query} wenzelm@57313: \end{center} wenzelm@62154: \caption{An instance of the Query panel: find theorems} wenzelm@57313: \label{fig:query} wenzelm@57313: \end{figure} wenzelm@57311: wenzelm@61415: \<^medskip> wenzelm@61415: The following GUI elements are common to all query modes: wenzelm@57311: wenzelm@61574: \<^item> The spinning wheel provides feedback about the status of a pending query wenzelm@61574: wrt.\ the evaluation of its context and its own operation. wenzelm@57311: wenzelm@61574: \<^item> The \<^emph>\Apply\ button attaches a fresh query invocation to the current wenzelm@61574: context of the command where the cursor is pointing in the text. wenzelm@57311: wenzelm@61574: \<^item> The \<^emph>\Search\ field allows to highlight query output according to some wenzelm@61574: regular expression, in the notation that is commonly used on the Java wenzelm@63680: platform.\<^footnote>\\<^url>\https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\\ wenzelm@61574: This may serve as an additional visual filter of the result. wenzelm@57311: wenzelm@61574: \<^item> The \<^emph>\Zoom\ box controls the font size of the output area. wenzelm@57311: wenzelm@57311: All query operations are asynchronous: there is no need to wait for the wenzelm@57311: evaluation of the document for the query context, nor for the query wenzelm@61477: operation itself. Query output may be detached as independent \<^emph>\Info\ wenzelm@57311: window, using a menu operation of the dockable window manager. The printed wenzelm@57311: result usually provides sufficient clues about the original query, with some wenzelm@57311: hyperlink to its context (via markup of its head line). wenzelm@58618: \ wenzelm@57311: wenzelm@57311: wenzelm@58618: subsection \Find theorems\ wenzelm@57311: wenzelm@58618: text \ wenzelm@61574: The \<^emph>\Query\ panel in \<^emph>\Find Theorems\ mode retrieves facts from the theory wenzelm@61574: or proof context matching all of given criteria in the \<^emph>\Find\ text field. A wenzelm@61574: single criterium has the following syntax: wenzelm@57311: wenzelm@57313: @{rail \ wenzelm@62969: ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' | wenzelm@57313: 'solves' | 'simp' ':' @{syntax term} | @{syntax term}) wenzelm@57313: \} wenzelm@57313: wenzelm@61574: See also the Isar command @{command_ref find_theorems} in @{cite wenzelm@61574: "isabelle-isar-ref"}. wenzelm@58618: \ wenzelm@57311: wenzelm@57311: wenzelm@58618: subsection \Find constants\ wenzelm@57311: wenzelm@58618: text \ wenzelm@61574: The \<^emph>\Query\ panel in \<^emph>\Find Constants\ mode prints all constants whose type wenzelm@61574: meets all of the given criteria in the \<^emph>\Find\ text field. A single wenzelm@61574: criterium has the following syntax: wenzelm@57313: wenzelm@57313: @{rail \ wenzelm@57313: ('-'?) wenzelm@62969: ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type}) wenzelm@57313: \} wenzelm@57313: wenzelm@58554: See also the Isar command @{command_ref find_consts} in @{cite wenzelm@58554: "isabelle-isar-ref"}. wenzelm@58618: \ wenzelm@57311: wenzelm@57311: wenzelm@58618: subsection \Print context\ wenzelm@57311: wenzelm@58618: text \ wenzelm@61574: The \<^emph>\Query\ panel in \<^emph>\Print Context\ mode prints information from the wenzelm@61574: theory or proof context, or proof state. See also the Isar commands wenzelm@57329: @{command_ref print_context}, @{command_ref print_cases}, @{command_ref wenzelm@62249: print_term_bindings}, @{command_ref print_theorems}, described in @{cite wenzelm@62249: "isabelle-isar-ref"}. wenzelm@58618: \ wenzelm@57311: wenzelm@57311: wenzelm@58618: section \Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\ wenzelm@54352: wenzelm@58618: text \ wenzelm@62249: Formally processed text (prover input or output) contains rich markup that wenzelm@62249: can be explored by using the \<^verbatim>\CONTROL\ modifier key on Linux and Windows, wenzelm@62249: or \<^verbatim>\COMMAND\ on Mac OS X. Hovering with the mouse while the modifier is wenzelm@62249: pressed reveals a \<^emph>\tooltip\ (grey box over the text with a yellow popup) wenzelm@62249: and/or a \<^emph>\hyperlink\ (black rectangle over the text with change of mouse wenzelm@62249: pointer); see also \figref{fig:tooltip}. wenzelm@54331: wenzelm@62183: \begin{figure}[!htb] wenzelm@54331: \begin{center} wenzelm@57312: \includegraphics[scale=0.5]{popup1} wenzelm@54331: \end{center} wenzelm@54356: \caption{Tooltip and hyperlink for some formal entity} wenzelm@54350: \label{fig:tooltip} wenzelm@54331: \end{figure} wenzelm@54331: wenzelm@62249: Tooltip popups use the same rendering technology as the main text area, and wenzelm@61574: further tooltips and/or hyperlinks may be exposed recursively by the same wenzelm@61574: mechanism; see \figref{fig:nested-tooltips}. wenzelm@54323: wenzelm@62183: \begin{figure}[!htb] wenzelm@54331: \begin{center} wenzelm@57312: \includegraphics[scale=0.5]{popup2} wenzelm@54331: \end{center} wenzelm@54356: \caption{Nested tooltips over formal entities} wenzelm@54350: \label{fig:nested-tooltips} wenzelm@54331: \end{figure} wenzelm@54350: wenzelm@61574: The tooltip popup window provides some controls to \<^emph>\close\ or \<^emph>\detach\ the wenzelm@61574: window, turning it into a separate \<^emph>\Info\ window managed by jEdit. The wenzelm@61574: \<^verbatim>\ESCAPE\ key closes \<^emph>\all\ popups, which is particularly relevant when wenzelm@61574: nested tooltips are stacking up. wenzelm@54352: wenzelm@61415: \<^medskip> wenzelm@61574: A black rectangle in the text indicates a hyperlink that may be followed by wenzelm@61574: a mouse click (while the \<^verbatim>\CONTROL\ or \<^verbatim>\COMMAND\ modifier key is still wenzelm@61574: pressed). Such jumps to other text locations are recorded by the wenzelm@61574: \<^emph>\Navigator\ plugin, which is bundled with Isabelle/jEdit and enabled by wenzelm@62249: default. There are usually navigation arrows in the main jEdit toolbar. wenzelm@54352: wenzelm@62249: Note that the link target may be a file that is itself not subject to formal wenzelm@62249: document processing of the editor session and thus prevents further wenzelm@61574: exploration: the chain of hyperlinks may end in some source file of the wenzelm@62249: underlying logic image, or within the ML bootstrap sources of Isabelle/Pure. wenzelm@61574: \ wenzelm@54321: wenzelm@54321: wenzelm@58618: section \Completion \label{sec:completion}\ wenzelm@57324: wenzelm@58618: text \ wenzelm@61477: Smart completion of partial input is the IDE functionality \<^emph>\par wenzelm@61477: excellance\. Isabelle/jEdit combines several sources of information to wenzelm@57328: achieve that. Despite its complexity, it should be possible to get some idea wenzelm@57328: how completion works by experimentation, based on the overview of completion wenzelm@57335: varieties in \secref{sec:completion-varieties}. The remaining subsections wenzelm@57335: explain concepts around completion more systematically. wenzelm@57325: wenzelm@61415: \<^medskip> wenzelm@61477: \<^emph>\Explicit completion\ is triggered by the action @{action_ref wenzelm@61574: "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\C+b\, and wenzelm@61574: thus overrides the jEdit default for @{action_ref "complete-word"}. wenzelm@57335: wenzelm@61574: \<^emph>\Implicit completion\ hooks into the regular keyboard input stream of the wenzelm@61574: editor, with some event filtering and optional delays. wenzelm@54361: wenzelm@61415: \<^medskip> wenzelm@61574: Completion options may be configured in \<^emph>\Plugin Options~/ Isabelle~/ wenzelm@61574: General~/ Completion\. These are explained in further detail below, whenever wenzelm@61574: relevant. There is also a summary of options in wenzelm@57328: \secref{sec:completion-options}. wenzelm@57328: wenzelm@57335: The asynchronous nature of PIDE interaction means that information from the wenzelm@57335: prover is delayed --- at least by a full round-trip of the document update wenzelm@57335: protocol. The default options already take this into account, with a wenzelm@57324: sufficiently long completion delay to speculate on the availability of all wenzelm@57335: relevant information from the editor and the prover, before completing text wenzelm@57335: immediately or producing a popup. Although there is an inherent danger of wenzelm@57335: non-deterministic behaviour due to such real-time parameters, the general wenzelm@57335: completion policy aims at determined results as far as possible. wenzelm@58618: \ wenzelm@57324: wenzelm@57324: wenzelm@58618: subsection \Varieties of completion \label{sec:completion-varieties}\ wenzelm@57324: wenzelm@58618: subsubsection \Built-in templates\ wenzelm@57324: wenzelm@58618: text \ wenzelm@57327: Isabelle is ultimately a framework of nested sub-languages of different wenzelm@57328: kinds and purposes. The completion mechanism supports this by the following wenzelm@57328: built-in templates: wenzelm@57328: wenzelm@64513: \<^descr> \<^verbatim>\`\ (single ASCII back-quote) or \<^verbatim>\"\ (double ASCII quote) support wenzelm@64513: \<^emph>\quotations\ via text cartouches. There are three selections, which are wenzelm@64513: always presented in the same order and do not depend on any context wenzelm@64513: information. The default choice produces a template ``\\\\\'', where the wenzelm@64513: box indicates the cursor position after insertion; the other choices help wenzelm@64513: to repair the block structure of unbalanced text cartouches. wenzelm@57324: wenzelm@61574: \<^descr> \<^verbatim>\@{\ is completed to the template ``\@{\}\'', where the box indicates wenzelm@61574: the cursor position after insertion. Here it is convenient to use the wenzelm@61574: wildcard ``\<^verbatim>\__\'' or a more specific name prefix to let semantic wenzelm@61574: completion of name-space entries propose antiquotation names. wenzelm@57335: wenzelm@57335: With some practice, input of quoted sub-languages and antiquotations of wenzelm@57335: embedded languages should work fluently. Note that national keyboard layouts wenzelm@64513: might cause problems with back-quote as dead key, but double quote can be wenzelm@64513: used instead. wenzelm@58618: \ wenzelm@57335: wenzelm@57327: wenzelm@58618: subsubsection \Syntax keywords\ wenzelm@57335: wenzelm@58618: text \ wenzelm@57335: Syntax completion tables are determined statically from the keywords of the wenzelm@57335: ``outer syntax'' of the underlying edit mode: for theory files this is the wenzelm@60257: syntax of Isar commands according to the cumulative theory imports. wenzelm@57327: wenzelm@57335: Keywords are usually plain words, which means the completion mechanism only wenzelm@57335: inserts them directly into the text for explicit completion wenzelm@57335: (\secref{sec:completion-input}), but produces a popup wenzelm@57335: (\secref{sec:completion-popup}) otherwise. wenzelm@57335: wenzelm@57335: At the point where outer syntax keywords are defined, it is possible to wenzelm@57335: specify an alternative replacement string to be inserted instead of the wenzelm@57335: keyword itself. An empty string means to suppress the keyword altogether, wenzelm@57335: which is occasionally useful to avoid confusion, e.g.\ the rare keyword wenzelm@61493: @{command simproc_setup} vs.\ the frequent name-space entry \simp\. wenzelm@58618: \ wenzelm@57324: wenzelm@57324: wenzelm@58618: subsubsection \Isabelle symbols\ wenzelm@57324: wenzelm@58618: text \ wenzelm@57325: The completion tables for Isabelle symbols (\secref{sec:symbols}) are wenzelm@63680: determined statically from \<^file>\$ISABELLE_HOME/etc/symbols\ and @{path wenzelm@63680: "$ISABELLE_HOME_USER/etc/symbols"} for each symbol specification as follows: wenzelm@57325: wenzelm@61415: \<^medskip> wenzelm@57325: \begin{tabular}{ll} wenzelm@61477: \<^bold>\completion entry\ & \<^bold>\example\ \\\hline wenzelm@61503: literal symbol & \<^verbatim>\\\ \\ wenzelm@61503: symbol name with backslash & \<^verbatim>\\\\<^verbatim>\forall\ \\ wenzelm@61503: symbol abbreviation & \<^verbatim>\ALL\ or \<^verbatim>\!\ \\ wenzelm@57325: \end{tabular} wenzelm@61415: \<^medskip> wenzelm@57325: wenzelm@57335: When inserted into the text, the above examples all produce the same Unicode wenzelm@61503: rendering \\\ of the underlying symbol \<^verbatim>\\\. wenzelm@57325: wenzelm@61574: A symbol abbreviation that is a plain word, like \<^verbatim>\ALL\, is treated like a wenzelm@61574: syntax keyword. Non-word abbreviations like \<^verbatim>\-->\ are inserted more wenzelm@61574: aggressively, except for single-character abbreviations like \<^verbatim>\!\ above. wenzelm@57324: wenzelm@62250: Completion via abbreviations like \<^verbatim>\ALL\ or \<^verbatim>\-->\ depends on the semantic wenzelm@62250: language context (\secref{sec:completion-context}). In contrast, backslash wenzelm@62250: sequences like \<^verbatim>\\forall\ \<^verbatim>\\\ are always possible, but require wenzelm@62250: additional interaction to confirm (via popup). wenzelm@62250: wenzelm@62250: The latter is important in ambiguous situations, e.g.\ for Isabelle document wenzelm@62250: source, which may contain formal symbols or informal {\LaTeX} macros. wenzelm@62250: Backslash sequences also help when input is broken, and thus escapes its wenzelm@62250: normal semantic context: e.g.\ antiquotations or string literals in ML, wenzelm@62250: which do not allow arbitrary backslash sequences. wenzelm@58618: \ wenzelm@57324: wenzelm@57324: wenzelm@64513: subsubsection \User-defined abbreviations\ wenzelm@64513: wenzelm@64513: text \ wenzelm@64513: The theory header syntax supports abbreviations via the \<^theory_text>\abbrevs\ keyword wenzelm@64513: @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in wenzelm@64513: templates and abbreviations for Isabelle symbols, as explained above. wenzelm@64513: Examples may be found in the Isabelle sources, by searching for wenzelm@64513: ``\<^verbatim>\abbrevs\'' in \<^verbatim>\*.thy\ files. wenzelm@64513: wenzelm@64513: The \<^emph>\Symbols\ panel shows the abbreviations that are available in the wenzelm@64513: current theory buffer (according to its \<^theory_text>\imports\) in the \<^verbatim>\Abbrevs\ tab. wenzelm@64513: \ wenzelm@64513: wenzelm@64513: wenzelm@58618: subsubsection \Name-space entries\ wenzelm@57324: wenzelm@58618: text \ wenzelm@57324: This is genuine semantic completion, using information from the prover, so wenzelm@61477: it requires some delay. A \<^emph>\failed name-space lookup\ produces an error wenzelm@57335: message that is annotated with a list of alternative names that are legal. wenzelm@57335: The list of results is truncated according to the system option wenzelm@57335: @{system_option_ref completion_limit}. The completion mechanism takes this wenzelm@57335: into account when collecting information on the prover side. wenzelm@57324: wenzelm@61574: Already recognized names are \<^emph>\not\ completed further, but completion may be wenzelm@61574: extended by appending a suffix of underscores. This provokes a failed wenzelm@57328: lookup, and another completion attempt while ignoring the underscores. For wenzelm@61574: example, in a name space where \<^verbatim>\foo\ and \<^verbatim>\foobar\ are known, the input wenzelm@61574: \<^verbatim>\foo\ remains unchanged, but \<^verbatim>\foo_\ may be completed to \<^verbatim>\foo\ or wenzelm@61574: \<^verbatim>\foobar\. wenzelm@57324: wenzelm@61574: The special identifier ``\<^verbatim>\__\'' serves as a wild-card for arbitrary wenzelm@61574: completion: it exposes the name-space content to the completion mechanism wenzelm@61574: (truncated according to @{system_option completion_limit}). This is wenzelm@61574: occasionally useful to explore an unknown name-space, e.g.\ in some wenzelm@57324: template. wenzelm@58618: \ wenzelm@57324: wenzelm@57324: wenzelm@58618: subsubsection \File-system paths\ wenzelm@57324: wenzelm@58618: text \ wenzelm@62250: Depending on prover markup about file-system paths in the source text, e.g.\ wenzelm@62250: for the argument of a load command (\secref{sec:aux-files}), the completion wenzelm@62250: mechanism explores the directory content and offers the result as completion wenzelm@62250: popup. Relative path specifications are understood wrt.\ the \<^emph>\master wenzelm@62250: directory\ of the document node (\secref{sec:buffer-node}) of the enclosing wenzelm@62250: editor buffer; this requires a proper theory, not an auxiliary file. wenzelm@57324: wenzelm@57324: A suffix of slashes may be used to continue the exploration of an already wenzelm@57324: recognized directory name. wenzelm@58618: \ wenzelm@57324: wenzelm@57324: wenzelm@58618: subsubsection \Spell-checking\ wenzelm@57328: wenzelm@58618: text \ wenzelm@57328: The spell-checker combines semantic markup from the prover (regions of plain wenzelm@57328: words) with static dictionaries (word lists) that are known to the editor. wenzelm@57328: wenzelm@57333: Unknown words are underlined in the text, using @{system_option_ref wenzelm@57328: spell_checker_color} (blue by default). This is not an error, but a hint to wenzelm@57335: the user that some action may be taken. The jEdit context menu provides wenzelm@57335: various actions, as far as applicable: wenzelm@57328: wenzelm@61415: \<^medskip> wenzelm@57328: \begin{tabular}{l} wenzelm@57329: @{action_ref "isabelle.complete-word"} \\ wenzelm@57329: @{action_ref "isabelle.exclude-word"} \\ wenzelm@57329: @{action_ref "isabelle.exclude-word-permanently"} \\ wenzelm@57329: @{action_ref "isabelle.include-word"} \\ wenzelm@57329: @{action_ref "isabelle.include-word-permanently"} \\ wenzelm@57328: \end{tabular} wenzelm@61415: \<^medskip> wenzelm@57328: wenzelm@57329: Instead of the specific @{action_ref "isabelle.complete-word"}, it is also wenzelm@57329: possible to use the generic @{action_ref "isabelle.complete"} with its wenzelm@61503: default keyboard shortcut \<^verbatim>\C+b\. wenzelm@57328: wenzelm@61415: \<^medskip> wenzelm@61574: Dictionary lookup uses some educated guesses about lower-case, upper-case, wenzelm@61574: and capitalized words. This is oriented on common use in English, where this wenzelm@62250: aspect is not decisive for proper spelling (in contrast to German, for wenzelm@62250: example). wenzelm@58618: \ wenzelm@57328: wenzelm@57328: wenzelm@58618: subsection \Semantic completion context \label{sec:completion-context}\ wenzelm@57325: wenzelm@58618: text \ wenzelm@57325: Completion depends on a semantic context that is provided by the prover, wenzelm@57325: although with some delay, because at least a full PIDE protocol round-trip wenzelm@57325: is required. Until that information becomes available in the PIDE wenzelm@57325: document-model, the default context is given by the outer syntax of the wenzelm@57325: editor mode (see also \secref{sec:buffer-node}). wenzelm@57325: wenzelm@61477: The semantic \<^emph>\language context\ provides information about nested wenzelm@62250: sub-languages of Isabelle: keywords are only completed for outer syntax, and wenzelm@62250: antiquotations for languages that support them. Symbol abbreviations only wenzelm@62250: work for specific sub-languages: e.g.\ ``\<^verbatim>\=>\'' is \<^emph>\not\ completed in wenzelm@62250: regular ML source, but is completed within ML strings, comments, wenzelm@62250: antiquotations. Backslash representations of symbols like ``\<^verbatim>\\foobar\'' or wenzelm@62250: ``\<^verbatim>\\\'' work in any context --- after additional confirmation. wenzelm@57325: wenzelm@61574: The prover may produce \<^emph>\no completion\ markup in exceptional situations, to wenzelm@61574: tell that some language keywords should be excluded from further completion wenzelm@62250: attempts. For example, ``\<^verbatim>\:\'' within accepted Isar syntax looses its wenzelm@62250: meaning as abbreviation for symbol ``\\\''. wenzelm@58618: \ wenzelm@57325: wenzelm@57325: wenzelm@58618: subsection \Input events \label{sec:completion-input}\ wenzelm@57324: wenzelm@58618: text \ wenzelm@57332: Completion is triggered by certain events produced by the user, with wenzelm@57332: optional delay after keyboard input according to @{system_option wenzelm@57332: jedit_completion_delay}. wenzelm@57325: wenzelm@61574: \<^descr>[Explicit completion] works via action @{action_ref "isabelle.complete"} wenzelm@61574: with keyboard shortcut \<^verbatim>\C+b\. This overrides the shortcut for @{action_ref wenzelm@61574: "complete-word"} in jEdit, but it is possible to restore the original jEdit wenzelm@61574: keyboard mapping of @{action "complete-word"} via \<^emph>\Global Options~/ wenzelm@61574: Shortcuts\ and invent a different one for @{action "isabelle.complete"}. wenzelm@57325: wenzelm@61439: \<^descr>[Explicit spell-checker completion] works via @{action_ref wenzelm@57332: "isabelle.complete-word"}, which is exposed in the jEdit context menu, if wenzelm@57332: the mouse points to a word that the spell-checker can complete. wenzelm@57332: wenzelm@61574: \<^descr>[Implicit completion] works via regular keyboard input of the editor. It wenzelm@61574: depends on further side-conditions: wenzelm@57325: wenzelm@61574: \<^enum> The system option @{system_option_ref jedit_completion} needs to be wenzelm@61574: enabled (default). wenzelm@57325: wenzelm@61574: \<^enum> Completion of syntax keywords requires at least 3 relevant characters in wenzelm@61574: the text. wenzelm@57325: wenzelm@61574: \<^enum> The system option @{system_option_ref jedit_completion_delay} determines wenzelm@61574: an additional delay (0.5 by default), before opening a completion popup. wenzelm@61574: The delay gives the prover a chance to provide semantic completion wenzelm@61458: information, notably the context (\secref{sec:completion-context}). wenzelm@57325: wenzelm@61458: \<^enum> The system option @{system_option_ref jedit_completion_immediate} wenzelm@61458: (enabled by default) controls whether replacement text should be inserted wenzelm@61458: immediately without popup, regardless of @{system_option wenzelm@61574: jedit_completion_delay}. This aggressive mode of completion is restricted wenzelm@62250: to symbol abbreviations that are not plain words (\secref{sec:symbols}). wenzelm@57325: wenzelm@61574: \<^enum> Completion of symbol abbreviations with only one relevant character in wenzelm@61574: the text always enforces an explicit popup, regardless of wenzelm@61574: @{system_option_ref jedit_completion_immediate}. wenzelm@58618: \ wenzelm@57324: wenzelm@57324: wenzelm@58618: subsection \Completion popup \label{sec:completion-popup}\ wenzelm@57324: wenzelm@58618: text \ wenzelm@61574: A \<^emph>\completion popup\ is a minimally invasive GUI component over the text wenzelm@61574: area that offers a selection of completion items to be inserted into the wenzelm@61574: text, e.g.\ by mouse clicks. Items are sorted dynamically, according to the wenzelm@61574: frequency of selection, with persistent history. The popup may interpret wenzelm@61574: special keys \<^verbatim>\ENTER\, \<^verbatim>\TAB\, \<^verbatim>\ESCAPE\, \<^verbatim>\UP\, \<^verbatim>\DOWN\, \<^verbatim>\PAGE_UP\, wenzelm@61574: \<^verbatim>\PAGE_DOWN\, but all other key events are passed to the underlying text wenzelm@61574: area. This allows to ignore unwanted completions most of the time and wenzelm@61574: continue typing quickly. Thus the popup serves as a mechanism of wenzelm@62250: confirmation of proposed items, while the default is to continue without wenzelm@61574: completion. wenzelm@57324: wenzelm@57324: The meaning of special keys is as follows: wenzelm@57324: wenzelm@61415: \<^medskip> wenzelm@57324: \begin{tabular}{ll} wenzelm@61477: \<^bold>\key\ & \<^bold>\action\ \\\hline wenzelm@61503: \<^verbatim>\ENTER\ & select completion (if @{system_option jedit_completion_select_enter}) \\ wenzelm@61503: \<^verbatim>\TAB\ & select completion (if @{system_option jedit_completion_select_tab}) \\ wenzelm@61503: \<^verbatim>\ESCAPE\ & dismiss popup \\ wenzelm@61503: \<^verbatim>\UP\ & move up one item \\ wenzelm@61503: \<^verbatim>\DOWN\ & move down one item \\ wenzelm@61503: \<^verbatim>\PAGE_UP\ & move up one page of items \\ wenzelm@61503: \<^verbatim>\PAGE_DOWN\ & move down one page of items \\ wenzelm@57324: \end{tabular} wenzelm@61415: \<^medskip> wenzelm@57324: wenzelm@61574: Movement within the popup is only active for multiple items. Otherwise the wenzelm@61574: corresponding key event retains its standard meaning within the underlying wenzelm@61574: text area. wenzelm@58618: \ wenzelm@57324: wenzelm@57324: wenzelm@58618: subsection \Insertion \label{sec:completion-insert}\ wenzelm@57324: wenzelm@58618: text \ wenzelm@57333: Completion may first propose replacements to be selected (via a popup), or wenzelm@57333: replace text immediately in certain situations and depending on certain wenzelm@57333: options like @{system_option jedit_completion_immediate}. In any case, wenzelm@57420: insertion works uniformly, by imitating normal jEdit text insertion, wenzelm@61477: depending on the state of the \<^emph>\text selection\. Isabelle/jEdit tries to wenzelm@57420: accommodate the most common forms of advanced selections in jEdit, but not wenzelm@57420: all combinations make sense. At least the following important cases are wenzelm@57420: well-defined: wenzelm@57333: wenzelm@61574: \<^descr>[No selection.] The original is removed and the replacement inserted, wenzelm@61574: depending on the caret position. wenzelm@57324: wenzelm@61574: \<^descr>[Rectangular selection of zero width.] This special case is treated by wenzelm@61574: jEdit as ``tall caret'' and insertion of completion imitates its normal wenzelm@61574: behaviour: separate copies of the replacement are inserted for each line wenzelm@61574: of the selection. wenzelm@57333: wenzelm@61574: \<^descr>[Other rectangular selection or multiple selections.] Here the original wenzelm@61574: is removed and the replacement is inserted for each line (or segment) of wenzelm@61574: the selection. wenzelm@57333: wenzelm@61574: Support for multiple selections is particularly useful for \<^emph>\HyperSearch\: wenzelm@61574: clicking on one of the items in the \<^emph>\HyperSearch Results\ window makes wenzelm@61574: jEdit select all its occurrences in the corresponding line of text. Then wenzelm@61574: explicit completion can be invoked via \<^verbatim>\C+b\, e.g.\ to replace occurrences wenzelm@61574: of \<^verbatim>\-->\ by \\\. wenzelm@57333: wenzelm@61415: \<^medskip> wenzelm@61574: Insertion works by removing and inserting pieces of text from the buffer. wenzelm@61574: This counts as one atomic operation on the jEdit history. Thus unintended wenzelm@61574: completions may be reverted by the regular @{action undo} action of jEdit. wenzelm@61574: According to normal jEdit policies, the recovered text after @{action undo} wenzelm@61574: is selected: \<^verbatim>\ESCAPE\ is required to reset the selection and to continue wenzelm@61574: typing more text. wenzelm@58618: \ wenzelm@57324: wenzelm@57324: wenzelm@58618: subsection \Options \label{sec:completion-options}\ wenzelm@57324: wenzelm@58618: text \ wenzelm@57324: This is a summary of Isabelle/Scala system options that are relevant for wenzelm@61574: completion. They may be configured in \<^emph>\Plugin Options~/ Isabelle~/ General\ wenzelm@61574: as usual. wenzelm@57332: wenzelm@61415: \<^item> @{system_option_def completion_limit} specifies the maximum number of wenzelm@60257: items for various semantic completion operations (name-space entries etc.) wenzelm@57332: wenzelm@61415: \<^item> @{system_option_def jedit_completion} guards implicit completion via wenzelm@57335: regular jEdit key events (\secref{sec:completion-input}): it allows to wenzelm@57335: disable implicit completion altogether. wenzelm@57324: wenzelm@61574: \<^item> @{system_option_def jedit_completion_select_enter} and @{system_option_def wenzelm@61574: jedit_completion_select_tab} enable keys to select a completion item from wenzelm@61574: the popup (\secref{sec:completion-popup}). Note that a regular mouse click wenzelm@61574: on the list of items is always possible. wenzelm@57833: wenzelm@61415: \<^item> @{system_option_def jedit_completion_context} specifies whether the wenzelm@57335: language context provided by the prover should be used at all. Disabling wenzelm@57335: that option makes completion less ``semantic''. Note that incomplete or wenzelm@57335: severely broken input may cause some disagreement of the prover and the user wenzelm@57335: about the intended language context. wenzelm@57332: wenzelm@61415: \<^item> @{system_option_def jedit_completion_delay} and @{system_option_def wenzelm@57333: jedit_completion_immediate} determine the handling of keyboard events for wenzelm@57333: implicit completion (\secref{sec:completion-input}). wenzelm@57332: wenzelm@61574: A @{system_option jedit_completion_delay}~\<^verbatim>\> 0\ postpones the processing of wenzelm@61574: key events, until after the user has stopped typing for the given time span, wenzelm@62250: but @{system_option jedit_completion_immediate}~\<^verbatim>\= true\ means that wenzelm@61574: abbreviations of Isabelle symbols are handled nonetheless. wenzelm@57332: wenzelm@61415: \<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob'' wenzelm@57335: patterns to ignore in file-system path completion (separated by colons), wenzelm@57335: e.g.\ backup files ending with tilde. wenzelm@57332: wenzelm@61574: \<^item> @{system_option_def spell_checker} is a global guard for all spell-checker wenzelm@61574: operations: it allows to disable that mechanism altogether. wenzelm@57332: wenzelm@61415: \<^item> @{system_option_def spell_checker_dictionary} determines the current wenzelm@57335: dictionary, taken from the colon-separated list in the settings variable wenzelm@57333: @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local wenzelm@57333: updates to a dictionary, by including or excluding words. The result of wenzelm@63669: permanent dictionary updates is stored in the directory @{path wenzelm@57335: "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary. wenzelm@57332: wenzelm@61574: \<^item> @{system_option_def spell_checker_elements} specifies a comma-separated wenzelm@61574: list of markup elements that delimit words in the source that is subject to wenzelm@61574: spell-checking, including various forms of comments. wenzelm@58618: \ wenzelm@54361: wenzelm@54361: wenzelm@58618: section \Automatically tried tools \label{sec:auto-tools}\ wenzelm@54353: wenzelm@58618: text \ wenzelm@57325: Continuous document processing works asynchronously in the background. wenzelm@57325: Visible document source that has been evaluated may get augmented by wenzelm@62251: additional results of \<^emph>\asynchronous print functions\. An example for that wenzelm@62251: is proof state output, if that is enabled in the Output panel wenzelm@62251: (\secref{sec:output}). More heavy-weight print functions may be applied as wenzelm@62251: well, e.g.\ to prove or disprove parts of the formal text by other means. wenzelm@54354: wenzelm@61574: Isabelle/HOL provides various automatically tried tools that operate on wenzelm@61574: outermost goal statements (e.g.\ @{command lemma}, @{command theorem}), wenzelm@61574: independently of the state of the current proof attempt. They work wenzelm@61574: implicitly without any arguments. Results are output as \<^emph>\information wenzelm@61574: messages\, which are indicated in the text area by blue squiggles and a blue wenzelm@61574: information sign in the gutter (see \figref{fig:auto-tools}). The message wenzelm@61574: content may be shown as for other output (see also \secref{sec:output}). wenzelm@61574: Some tools produce output with \<^emph>\sendback\ markup, which means that clicking wenzelm@62251: on certain parts of the text inserts that into the source in the proper wenzelm@62251: place. wenzelm@54356: wenzelm@62183: \begin{figure}[!htb] wenzelm@54356: \begin{center} wenzelm@57312: \includegraphics[scale=0.333]{auto-tools} wenzelm@54356: \end{center} wenzelm@57312: \caption{Result of automatically tried tools} wenzelm@54356: \label{fig:auto-tools} wenzelm@54356: \end{figure} wenzelm@54354: wenzelm@61415: \<^medskip> wenzelm@61574: The following Isabelle system options control the behavior of automatically wenzelm@61574: tried tools (see also the jEdit dialog window \<^emph>\Plugin Options~/ Isabelle~/ wenzelm@61574: General~/ Automatically tried tools\): wenzelm@54354: wenzelm@61574: \<^item> @{system_option_ref auto_methods} controls automatic use of a combination wenzelm@61574: of standard proof methods (@{method auto}, @{method simp}, @{method blast}, wenzelm@61574: etc.). This corresponds to the Isar command @{command_ref "try0"} @{cite wenzelm@61574: "isabelle-isar-ref"}. wenzelm@54354: wenzelm@54354: The tool is disabled by default, since unparameterized invocation of wenzelm@61574: standard proof methods often consumes substantial CPU resources without wenzelm@61574: leading to success. wenzelm@54354: wenzelm@61574: \<^item> @{system_option_ref auto_nitpick} controls a slightly reduced version of wenzelm@61574: @{command_ref nitpick}, which tests for counterexamples using first-order wenzelm@61574: relational logic. See also the Nitpick manual @{cite "isabelle-nitpick"}. wenzelm@54354: wenzelm@61574: This tool is disabled by default, due to the extra overhead of invoking an wenzelm@61574: external Java process for each attempt to disprove a subgoal. wenzelm@54354: wenzelm@61415: \<^item> @{system_option_ref auto_quickcheck} controls automatic use of wenzelm@61574: @{command_ref quickcheck}, which tests for counterexamples using a series of wenzelm@61574: assignments for free variables of a subgoal. wenzelm@54354: wenzelm@61574: This tool is \<^emph>\enabled\ by default. It requires little overhead, but is a wenzelm@61574: bit weaker than @{command nitpick}. wenzelm@54354: wenzelm@61574: \<^item> @{system_option_ref auto_sledgehammer} controls a significantly reduced wenzelm@61574: version of @{command_ref sledgehammer}, which attempts to prove a subgoal wenzelm@61574: using external automatic provers. See also the Sledgehammer manual @{cite wenzelm@61574: "isabelle-sledgehammer"}. wenzelm@54354: wenzelm@61574: This tool is disabled by default, due to the relatively heavy nature of wenzelm@61574: Sledgehammer. wenzelm@54354: wenzelm@61415: \<^item> @{system_option_ref auto_solve_direct} controls automatic use of wenzelm@61574: @{command_ref solve_direct}, which checks whether the current subgoals can wenzelm@61574: be solved directly by an existing theorem. This also helps to detect wenzelm@61574: duplicate lemmas. wenzelm@54354: wenzelm@61477: This tool is \<^emph>\enabled\ by default. wenzelm@54354: wenzelm@54354: wenzelm@61574: Invocation of automatically tried tools is subject to some global policies wenzelm@61574: of parallel execution, which may be configured as follows: wenzelm@54354: wenzelm@61574: \<^item> @{system_option_ref auto_time_limit} (default 2.0) determines the timeout wenzelm@61574: (in seconds) for each tool execution. wenzelm@54354: wenzelm@61574: \<^item> @{system_option_ref auto_time_start} (default 1.0) determines the start wenzelm@61574: delay (in seconds) for automatically tried tools, after the main command wenzelm@61574: evaluation is finished. wenzelm@54354: wenzelm@54354: wenzelm@61574: Each tool is submitted independently to the pool of parallel execution tasks wenzelm@61574: in Isabelle/ML, using hardwired priorities according to its relative wenzelm@61574: ``heaviness''. The main stages of evaluation and printing of proof states wenzelm@61574: take precedence, but an already running tool is not canceled and may thus wenzelm@61574: reduce reactivity of proof document processing. wenzelm@54354: wenzelm@61574: Users should experiment how the available CPU resources (number of cores) wenzelm@61574: are best invested to get additional feedback from prover in the background, wenzelm@61574: by using a selection of weaker or stronger tools. wenzelm@58618: \ wenzelm@54353: wenzelm@54353: wenzelm@58618: section \Sledgehammer \label{sec:sledgehammer}\ wenzelm@54353: wenzelm@61574: text \ wenzelm@61574: The \<^emph>\Sledgehammer\ panel (\figref{fig:sledgehammer}) provides a view on wenzelm@61574: some independent execution of the Isar command @{command_ref sledgehammer}, wenzelm@61574: with process indicator (spinning wheel) and GUI elements for important wenzelm@61574: Sledgehammer arguments and options. Any number of Sledgehammer panels may be wenzelm@61574: active, according to the standard policies of Dockable Window Management in wenzelm@61574: jEdit. Closing such windows also cancels the corresponding prover tasks. wenzelm@54356: wenzelm@62183: \begin{figure}[!htb] wenzelm@54356: \begin{center} wenzelm@57312: \includegraphics[scale=0.333]{sledgehammer} wenzelm@54356: \end{center} wenzelm@54356: \caption{An instance of the Sledgehammer panel} wenzelm@54356: \label{fig:sledgehammer} wenzelm@54356: \end{figure} wenzelm@54355: wenzelm@61574: The \<^emph>\Apply\ button attaches a fresh invocation of @{command sledgehammer} wenzelm@61574: to the command where the cursor is pointing in the text --- this should be wenzelm@61574: some pending proof problem. Further buttons like \<^emph>\Cancel\ and \<^emph>\Locate\ wenzelm@61574: help to manage the running process. wenzelm@54355: wenzelm@61574: Results appear incrementally in the output window of the panel. Proposed wenzelm@61574: proof snippets are marked-up as \<^emph>\sendback\, which means a single mouse wenzelm@61574: click inserts the text into a suitable place of the original source. Some wenzelm@61574: manual editing may be required nonetheless, say to remove earlier proof wenzelm@61574: attempts. wenzelm@61574: \ wenzelm@54353: wenzelm@54353: wenzelm@60255: chapter \Isabelle document preparation\ wenzelm@60255: wenzelm@61574: text \ wenzelm@61574: The ultimate purpose of Isabelle is to produce nicely rendered documents wenzelm@60255: with the Isabelle document preparation system, which is based on {\LaTeX}; wenzelm@60270: see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit wenzelm@61574: provides some additional support for document editing. wenzelm@61574: \ wenzelm@60255: wenzelm@60255: wenzelm@60255: section \Document outline\ wenzelm@60255: wenzelm@61574: text \ wenzelm@61574: Theory sources may contain document markup commands, such as @{command_ref wenzelm@61574: chapter}, @{command_ref section}, @{command subsection}. The Isabelle wenzelm@61574: SideKick parser (\secref{sec:sidekick}) represents this document outline as wenzelm@61574: structured tree view, with formal statements and proofs nested inside; see wenzelm@61574: \figref{fig:sidekick-document}. wenzelm@60255: wenzelm@62183: \begin{figure}[!htb] wenzelm@60255: \begin{center} wenzelm@60255: \includegraphics[scale=0.333]{sidekick-document} wenzelm@60255: \end{center} wenzelm@60255: \caption{Isabelle document outline via SideKick tree view} wenzelm@60255: \label{fig:sidekick-document} wenzelm@60255: \end{figure} wenzelm@60264: wenzelm@60264: It is also possible to use text folding according to this structure, by wenzelm@61574: adjusting \<^emph>\Utilities / Buffer Options / Folding mode\ of jEdit. The default wenzelm@61574: mode \<^verbatim>\isabelle\ uses the structure of formal definitions, statements, and wenzelm@61574: proofs. The alternative mode \<^verbatim>\sidekick\ uses the document structure of the wenzelm@61574: SideKick parser, as explained above. wenzelm@61574: \ wenzelm@60264: wenzelm@60255: wenzelm@62154: section \Markdown structure\ wenzelm@62154: wenzelm@62154: text \ wenzelm@62251: Document text is internally structured in paragraphs and nested lists, using wenzelm@63680: notation that is similar to Markdown\<^footnote>\\<^url>\http://commonmark.org\\. There are wenzelm@63680: special control symbols for items of different kinds of lists, corresponding wenzelm@63680: to \<^verbatim>\itemize\, \<^verbatim>\enumerate\, \<^verbatim>\description\ in {\LaTeX}. This is illustrated wenzelm@63680: in for \<^verbatim>\itemize\ in \figref{fig:markdown-document}. wenzelm@62154: wenzelm@62183: \begin{figure}[!htb] wenzelm@62154: \begin{center} wenzelm@62154: \includegraphics[scale=0.333]{markdown-document} wenzelm@62154: \end{center} wenzelm@62154: \caption{Markdown structure within document text} wenzelm@62154: \label{fig:markdown-document} wenzelm@62154: \end{figure} wenzelm@62251: wenzelm@62251: Items take colour according to the depth of nested lists. This helps to wenzelm@62251: explore the implicit rules for list structure interactively. There is also wenzelm@62251: markup for individual paragraphs in the text: it may be explored via mouse wenzelm@62251: hovering with \<^verbatim>\CONTROL\ / \<^verbatim>\COMMAND\ as usual wenzelm@62251: (\secref{sec:tooltips-hyperlinks}). wenzelm@62154: \ wenzelm@62154: wenzelm@62154: wenzelm@62184: section \Citations and Bib{\TeX} entries \label{sec:bibtex}\ wenzelm@60255: wenzelm@61574: text \ wenzelm@61574: Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\.bib\ files. The wenzelm@61574: Isabelle session build process and the @{tool latex} tool @{cite wenzelm@60270: "isabelle-system"} are smart enough to assemble the result, based on the wenzelm@60257: session directory layout. wenzelm@60255: wenzelm@61493: The document antiquotation \@{cite}\ is described in @{cite wenzelm@60255: "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for wenzelm@60255: tooltips, hyperlinks, and completion for Bib{\TeX} database entries. wenzelm@61574: Isabelle/jEdit does \<^emph>\not\ know about the actual Bib{\TeX} environment used wenzelm@61574: in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\.bib\ files wenzelm@61574: that happen to be open in the editor; see \figref{fig:cite-completion}. wenzelm@60255: wenzelm@62183: \begin{figure}[!htb] wenzelm@60255: \begin{center} wenzelm@60255: \includegraphics[scale=0.333]{cite-completion} wenzelm@60255: \end{center} wenzelm@60255: \caption{Semantic completion of citations from open Bib{\TeX} files} wenzelm@60255: \label{fig:cite-completion} wenzelm@60255: \end{figure} wenzelm@60255: wenzelm@61574: Isabelle/jEdit also provides some support for editing \<^verbatim>\.bib\ files wenzelm@61574: themselves. There is syntax highlighting based on entry types (according to wenzelm@61574: standard Bib{\TeX} styles), a context-menu to compose entries wenzelm@60255: systematically, and a SideKick tree view of the overall content; see wenzelm@60255: \figref{fig:bibtex-mode}. wenzelm@60255: wenzelm@62183: \begin{figure}[!htb] wenzelm@60255: \begin{center} wenzelm@60255: \includegraphics[scale=0.333]{bibtex-mode} wenzelm@60255: \end{center} wenzelm@60255: \caption{Bib{\TeX} mode with context menu and SideKick tree view} wenzelm@60255: \label{fig:bibtex-mode} wenzelm@60255: \end{figure} wenzelm@60255: \ wenzelm@60255: wenzelm@60255: wenzelm@62253: chapter \ML debugging within the Prover IDE\ wenzelm@62154: wenzelm@62154: text \ wenzelm@63680: Isabelle/ML is based on Poly/ML\<^footnote>\\<^url>\http://www.polyml.org\\ and thus wenzelm@62253: benefits from the source-level debugger of that implementation of Standard wenzelm@62253: ML. The Prover IDE provides the \<^emph>\Debugger\ dockable to connect to running wenzelm@62253: ML threads, inspect the stack frame with local ML bindings, and evaluate ML wenzelm@62253: expressions in a particular run-time context. A typical debugger session is wenzelm@62253: shown in \figref{fig:ml-debugger}. wenzelm@62253: wenzelm@62253: ML debugging depends on the following pre-requisites. wenzelm@62253: wenzelm@62253: \<^enum> ML source needs to be compiled with debugging enabled. This may be wenzelm@62253: controlled for particular chunks of ML sources using any of the subsequent wenzelm@62253: facilities. wenzelm@62253: wenzelm@62253: \<^enum> The system option @{system_option_ref ML_debugger} as implicit state wenzelm@62253: of the Isabelle process. It may be changed in the menu \<^emph>\Plugins / wenzelm@62253: Plugin Options / Isabelle / General\. ML modules need to be reloaded and wenzelm@62253: recompiled to pick up that option as intended. wenzelm@62253: wenzelm@62253: \<^enum> The configuration option @{attribute_ref ML_debugger}, with an wenzelm@62253: attribute of the same name, to update a global or local context (e.g.\ wenzelm@62253: with the @{command declare} command). wenzelm@62253: wenzelm@62253: \<^enum> Commands that modify @{attribute ML_debugger} state for individual wenzelm@62253: files: @{command_ref ML_file_debug}, @{command_ref ML_file_no_debug}, wenzelm@62253: @{command_ref SML_file_debug}, @{command_ref SML_file_no_debug}. wenzelm@62253: wenzelm@62253: The instrumentation of ML code for debugging causes minor run-time wenzelm@62253: overhead. ML modules that implement critical system infrastructure may wenzelm@62253: lead to deadlocks or other undefined behaviour, when put under debugger wenzelm@62253: control! wenzelm@62253: wenzelm@62253: \<^enum> The \<^emph>\Debugger\ panel needs to be active, otherwise the program ignores wenzelm@62253: debugger instrumentation of the compiler and runs unmanaged. It is also wenzelm@62253: possible to start debugging with the panel open, and later undock it, to wenzelm@62253: let the program continue unhindered. wenzelm@62253: wenzelm@62253: \<^enum> The ML program needs to be stopped at a suitable breakpoint, which may wenzelm@62253: be activated individually or globally as follows. wenzelm@62253: wenzelm@62253: For ML sources that have been compiled with debugger support, the IDE wenzelm@62253: visualizes possible breakpoints in the text. A breakpoint may be toggled wenzelm@62253: by pointing accurately with the mouse, with a right-click to activate wenzelm@62253: jEdit's context menu and its \<^emph>\Toggle Breakpoint\ item. Alternatively, the wenzelm@62253: \<^emph>\Break\ checkbox in the \<^emph>\Debugger\ panel may be enabled to stop ML wenzelm@62253: threads always at the next possible breakpoint. wenzelm@62253: wenzelm@62253: Note that the state of individual breakpoints \<^emph>\gets lost\ when the wenzelm@62253: coresponding ML source is re-compiled! This may happen unintentionally, wenzelm@62253: e.g.\ when following hyperlinks into ML modules that have not been loaded wenzelm@62253: into the IDE before. wenzelm@62154: wenzelm@62183: \begin{figure}[!htb] wenzelm@62154: \begin{center} wenzelm@62154: \includegraphics[scale=0.333]{ml-debugger} wenzelm@62154: \end{center} wenzelm@62253: \caption{ML debugger session} wenzelm@62154: \label{fig:ml-debugger} wenzelm@62154: \end{figure} wenzelm@62253: wenzelm@62253: The debugger panel (\figref{fig:ml-debugger}) shows a list of all threads wenzelm@62253: that are presently stopped. Each thread shows a stack of all function wenzelm@62253: invocations that lead to the current breakpoint at the top. wenzelm@62253: wenzelm@62253: It is possible to jump between stack positions freely, by clicking on this wenzelm@62253: list. The current situation is displayed in the big output window, as a wenzelm@62253: local ML environment with names and printed values. wenzelm@62253: wenzelm@62253: ML expressions may be evaluated in the current context by entering snippets wenzelm@62253: of source into the text fields labeled \Context\ and \ML\, and pushing the wenzelm@62253: \Eval\ button. By default, the source is interpreted as Isabelle/ML with the wenzelm@62253: usual support for antiquotations (like @{command ML}, @{command ML_file}). wenzelm@62253: Alternatively, strict Standard ML may be enforced via the \<^emph>\SML\ checkbox wenzelm@62253: (like @{command SML_file}). wenzelm@62253: wenzelm@62253: The context for Isabelle/ML is optional, it may evaluate to a value of type wenzelm@62253: @{ML_type theory}, @{ML_type Proof.context}, or @{ML_type Context.generic}. wenzelm@62253: Thus the given ML expression (with its antiquotations) may be subject to the wenzelm@62253: intended dynamic run-time context, instead of the static compile-time wenzelm@62253: context. wenzelm@62253: wenzelm@62253: \<^medskip> wenzelm@62253: The buttons labeled \<^emph>\Continue\, \<^emph>\Step\, \<^emph>\Step over\, \<^emph>\Step out\ wenzelm@62253: recommence execution of the program, with different policies concerning wenzelm@62253: nested function invocations. The debugger always moves the cursor within the wenzelm@62253: ML source to the next breakpoint position, and offers new stack frames as wenzelm@62253: before. wenzelm@62154: \ wenzelm@62154: wenzelm@62154: wenzelm@58618: chapter \Miscellaneous tools\ wenzelm@54358: wenzelm@58618: section \Timing\ wenzelm@54359: wenzelm@61574: text \ wenzelm@61574: Managed evaluation of commands within PIDE documents includes timing wenzelm@61574: information, which consists of elapsed (wall-clock) time, CPU time, and GC wenzelm@61574: (garbage collection) time. Note that in a multithreaded system it is wenzelm@61574: difficult to measure execution time precisely: elapsed time is closer to the wenzelm@61574: real requirements of runtime resources than CPU or GC time, which are both wenzelm@61574: subject to influences from the parallel environment that are outside the wenzelm@61574: scope of the current command transaction. wenzelm@54359: wenzelm@61574: The \<^emph>\Timing\ panel provides an overview of cumulative command timings for wenzelm@61574: each document node. Commands with elapsed time below the given threshold are wenzelm@61574: ignored in the grand total. Nodes are sorted according to their overall wenzelm@61574: timing. For the document node that corresponds to the current buffer, wenzelm@61574: individual command timings are shown as well. A double-click on a theory wenzelm@61574: node or command moves the editor focus to that particular source position. wenzelm@54359: wenzelm@61574: It is also possible to reveal individual timing information via some tooltip wenzelm@61574: for the corresponding command keyword, using the technique of mouse hovering wenzelm@62251: with \<^verbatim>\CONTROL\~/ \<^verbatim>\COMMAND\ modifier (\secref{sec:tooltips-hyperlinks}). wenzelm@62251: Actual display of timing depends on the global option @{system_option_ref wenzelm@62251: jedit_timing_threshold}, which can be configured in \<^emph>\Plugin Options~/ wenzelm@62251: Isabelle~/ General\. wenzelm@54360: wenzelm@61415: \<^medskip> wenzelm@61574: The \<^emph>\Monitor\ panel visualizes various data collections about recent wenzelm@61574: activity of the Isabelle/ML task farm and the underlying ML runtime system. wenzelm@61574: The display is continuously updated according to @{system_option_ref wenzelm@57869: editor_chart_delay}. Note that the painting of the chart takes considerable wenzelm@57869: runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not wenzelm@61503: Isabelle/ML. Internally, the Isabelle/Scala module \<^verbatim>\isabelle.ML_Statistics\ wenzelm@61503: provides further access to statistics of Isabelle/ML. wenzelm@61503: \ wenzelm@54359: wenzelm@54359: wenzelm@58618: section \Low-level output\ wenzelm@54358: wenzelm@61574: text \ wenzelm@62251: Prover output is normally shown directly in the main text area or specific wenzelm@62251: panels like \<^emph>\Output\ (\secref{sec:output}) or \<^emph>\State\ wenzelm@62251: (\secref{sec:state-output}). Beyond this, it is occasionally useful to wenzelm@62251: inspect low-level output channels via some of the following additional wenzelm@62251: panels: wenzelm@54358: wenzelm@61574: \<^item> \<^emph>\Protocol\ shows internal messages between the Isabelle/Scala and wenzelm@61574: Isabelle/ML side of the PIDE document editing protocol. Recording of wenzelm@61574: messages starts with the first activation of the corresponding dockable wenzelm@61574: window; earlier messages are lost. wenzelm@54358: wenzelm@61574: Actual display of protocol messages causes considerable slowdown, so it is wenzelm@61574: important to undock all \<^emph>\Protocol\ panels for production work. wenzelm@54358: wenzelm@61503: \<^item> \<^emph>\Raw Output\ shows chunks of text from the \<^verbatim>\stdout\ and \<^verbatim>\stderr\ wenzelm@61574: channels of the prover process. Recording of output starts with the first wenzelm@61574: activation of the corresponding dockable window; earlier output is lost. wenzelm@54358: wenzelm@61574: The implicit stateful nature of physical I/O channels makes it difficult to wenzelm@61574: relate raw output to the actual command from where it was originating. wenzelm@61574: Parallel execution may add to the confusion. Peeking at physical process I/O wenzelm@61574: is only the last resort to diagnose problems with tools that are not PIDE wenzelm@61574: compliant. wenzelm@54358: wenzelm@57310: Under normal circumstances, prover output always works via managed message wenzelm@57310: channels (corresponding to @{ML writeln}, @{ML warning}, @{ML wenzelm@57420: Output.error_message} in Isabelle/ML), which are displayed by regular means wenzelm@60257: within the document model (\secref{sec:output}). Unhandled Isabelle/ML wenzelm@60257: exceptions are printed by the system via @{ML Output.error_message}. wenzelm@54358: wenzelm@61477: \<^item> \<^emph>\Syslog\ shows system messages that might be relevant to diagnose wenzelm@60257: problems with the startup or shutdown phase of the prover process; this also wenzelm@61574: includes raw output on \<^verbatim>\stderr\. Isabelle/ML also provides an explicit @{ML wenzelm@61574: Output.system_message} operation, which is occasionally useful for wenzelm@61574: diagnostic purposes within the system infrastructure itself. wenzelm@54358: wenzelm@61574: A limited amount of syslog messages are buffered, independently of the wenzelm@61574: docking state of the \<^emph>\Syslog\ panel. This allows to diagnose serious wenzelm@61574: problems with Isabelle/PIDE process management, outside of the actual wenzelm@61574: protocol layer. wenzelm@54358: wenzelm@61574: Under normal situations, such low-level system output can be ignored. wenzelm@58618: \ wenzelm@54358: wenzelm@54358: wenzelm@58618: chapter \Known problems and workarounds \label{sec:problems}\ wenzelm@53770: wenzelm@58618: text \ wenzelm@61574: \<^item> \<^bold>\Problem:\ Odd behavior of some diagnostic commands with global wenzelm@61574: side-effects, like writing a physical file. wenzelm@53770: wenzelm@61574: \<^bold>\Workaround:\ Copy/paste complete command text from elsewhere, or disable wenzelm@61574: continuous checking temporarily. wenzelm@53770: wenzelm@61574: \<^item> \<^bold>\Problem:\ No direct support to remove document nodes from the collection wenzelm@61574: of theories. wenzelm@53770: wenzelm@61574: \<^bold>\Workaround:\ Clear the buffer content of unused files and close \<^emph>\without\ wenzelm@61574: saving changes. wenzelm@54330: wenzelm@61574: \<^item> \<^bold>\Problem:\ Keyboard shortcuts \<^verbatim>\C+PLUS\ and \<^verbatim>\C+MINUS\ for adjusting the wenzelm@61574: editor font size depend on platform details and national keyboards. wenzelm@61574: wenzelm@61574: \<^bold>\Workaround:\ Rebind keys via \<^emph>\Global Options~/ Shortcuts\. wenzelm@54330: wenzelm@61503: \<^item> \<^bold>\Problem:\ The Mac OS X key sequence \<^verbatim>\COMMAND+COMMA\ for application wenzelm@61574: \<^emph>\Preferences\ is in conflict with the jEdit default keyboard shortcut for wenzelm@61574: \<^emph>\Incremental Search Bar\ (action @{action_ref "quick-search"}). wenzelm@53770: wenzelm@61574: \<^bold>\Workaround:\ Rebind key via \<^emph>\Global Options~/ Shortcuts\ according to wenzelm@61574: national keyboard, e.g.\ \<^verbatim>\COMMAND+SLASH\ on English ones. wenzelm@53770: wenzelm@61522: \<^item> \<^bold>\Problem:\ On Mac OS X with native Apple look-and-feel, some exotic wenzelm@61522: national keyboards may cause a conflict of menu accelerator keys with wenzelm@61522: regular jEdit key bindings. This leads to duplicate execution of the wenzelm@61522: corresponding jEdit action. wenzelm@61522: wenzelm@61522: \<^bold>\Workaround:\ Disable the native Apple menu bar via Java runtime option wenzelm@61522: \<^verbatim>\-Dapple.laf.useScreenMenuBar=false\. wenzelm@61522: wenzelm@61574: \<^item> \<^bold>\Problem:\ Mac OS X system fonts sometimes lead to character drop-outs in wenzelm@61574: the main text area. wenzelm@54349: wenzelm@62265: \<^bold>\Workaround:\ Use the default \<^verbatim>\IsabelleText\ font. wenzelm@62265: wenzelm@62265: \<^item> \<^bold>\Problem:\ Mac OS X with Retina display has problems to determine the wenzelm@62265: font metrics of \<^verbatim>\IsabelleText\ accurately, notably in plain Swing text wenzelm@62265: fields (e.g.\ in the \<^emph>\Search and Replace\ dialog). wenzelm@62265: wenzelm@62265: \<^bold>\Workaround:\ Install \<^verbatim>\IsabelleText\ and \<^verbatim>\IsabelleTextBold\ on the system wenzelm@62265: with \<^emph>\Font Book\, despite the warnings in \secref{sec:symbols} against wenzelm@63669: that! The \<^verbatim>\.ttf\ font files reside in some directory @{path wenzelm@62265: "$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}. wenzelm@53770: wenzelm@61574: \<^item> \<^bold>\Problem:\ Some Linux/X11 input methods such as IBus tend to disrupt key wenzelm@61574: event handling of Java/AWT/Swing. wenzelm@54329: wenzelm@61574: \<^bold>\Workaround:\ Do not use X11 input methods. Note that environment variable wenzelm@61574: \<^verbatim>\XMODIFIERS\ is reset by default within Isabelle settings. wenzelm@61574: wenzelm@61574: \<^item> \<^bold>\Problem:\ Some Linux/X11 window managers that are not ``re-parenting'' wenzelm@61574: cause problems with additional windows opened by Java. This affects either wenzelm@61574: historic or neo-minimalistic window managers like \<^verbatim>\awesome\ or \<^verbatim>\xmonad\. wenzelm@54329: wenzelm@61477: \<^bold>\Workaround:\ Use a regular re-parenting X11 window manager. wenzelm@54329: wenzelm@61574: \<^item> \<^bold>\Problem:\ Various forks of Linux/X11 window managers and desktop wenzelm@61574: environments (like Gnome) disrupt the handling of menu popups and mouse wenzelm@61574: positions of Java/AWT/Swing. wenzelm@54329: wenzelm@62183: \<^bold>\Workaround:\ Use suitable version of Linux desktops. wenzelm@60291: wenzelm@61477: \<^item> \<^bold>\Problem:\ Full-screen mode via jEdit action @{action_ref wenzelm@61574: "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\F11\) works on Windows, wenzelm@61574: but not on Mac OS X or various Linux/X11 window managers. wenzelm@54349: wenzelm@61574: \<^bold>\Workaround:\ Use native full-screen control of the window manager (notably wenzelm@61574: on Mac OS X). wenzelm@64512: wenzelm@64512: \<^item> \<^bold>\Problem:\ Heap space of the JVM may fill up and render the Prover IDE wenzelm@64512: unresponsive, e.g.\ when editing big Isabelle sessions with many theories. wenzelm@64512: wenzelm@64512: \<^bold>\Workaround:\ On a 64bit platform, ensure that the JVM runs in 64bit mode, wenzelm@64512: but the Isabelle/ML process remains in 32bit mode! Do not switch Isabelle/ML wenzelm@64512: into 64bit mode in the expectation to be ``more efficient'' --- this wenzelm@64512: requires approx.\ 32\,GB to make sense. wenzelm@64512: wenzelm@64512: For the JVM, always use the 64bit version. That is the default on all wenzelm@64512: platforms, except for Windows: the standard download is for win32, but there wenzelm@64512: is a separate download for win64. This implicitly provides a larger default wenzelm@64512: heap for the JVM. wenzelm@64512: wenzelm@64512: Moreover, it is possible to increase JVM heap parameters explicitly, by wenzelm@64512: editing platform-specific files (for ``properties'' or ``options'') that are wenzelm@64512: associated with the main app bundle. wenzelm@64512: wenzelm@64512: Also note that jEdit provides a heap space monitor in the status line wenzelm@64512: (bottom-right). Double-clicking on that causes full garbage-collection, wenzelm@64512: which sometimes helps in low-memory situations. wenzelm@58618: \ wenzelm@53770: wenzelm@53769: end