
wenzelm@61656: (*:maxLineLen=78:*)
wenzelm@53981: 
wenzelm@53769: theory JEdit
wenzelm@53769: imports Base
wenzelm@53769: begin
wenzelm@53769: 
wenzelm@58618: chapter \<open>Introduction\<close>
wenzelm@53769: 
wenzelm@58618: section \<open>Concepts and terminology\<close>
wenzelm@53770: 
wenzelm@58618: text \<open>
wenzelm@61574:   Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close>
wenzelm@61574:   @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\<open>asynchronous user
wenzelm@61574:   interaction\<close> @{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>\<open>continuous proof processing\<close> @{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@66683:     services, SSH servers, SQL databases etc. Special infrastructure allows to
wenzelm@66683:     transfer algebraic datatypes and formatted text easily between ML and
wenzelm@66683:     Scala, using 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>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
wenzelm@68224:     implemented in Java\<^footnote>\<open>\<^url>\<open>https://www.java.com\<close>\<close>. It is easily extensible by
wenzelm@63680:     plugins written in any language that works on the JVM. In the context of
wenzelm@68224:     Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>.
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: \<close>
wenzelm@53770: 
wenzelm@53770: 
wenzelm@58618: section \<open>The Isabelle/jEdit Prover IDE\<close>
wenzelm@53770: 
wenzelm@58618: text \<open>
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@68067:   \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several actions and add-on panels (see
wenzelm@68067:   also \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/
wenzelm@68067:   Isabelle\<close> (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>\<open>Theories\<close> panel (\secref{sec:theories}). After
wenzelm@66683:   startup of the Isabelle plugin, the selected logic session image is provided
wenzelm@62183:   automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
wenzelm@66683:   absent or outdated wrt.\ its sources, the build process updates it within
wenzelm@66683:   the running text editor. Prover IDE functionality is fully activated after
wenzelm@62183:   successful termination of the build process. A failure may require changing
wenzelm@66683:   some options and restart of the Isabelle plugin or application. Changing the
wenzelm@66683:   logic session, or the underlying ML system platform (32\,bit versus 64\,bit)
wenzelm@66683:   requires a restart of the whole 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>\<open>CONTROL\<close> (Linux, Windows)
wenzelm@62183:   or \<^verbatim>\<open>COMMAND\<close> (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: \<close>
wenzelm@53769: 
wenzelm@53770: 
wenzelm@58618: subsection \<open>Documentation\<close>
wenzelm@54321: 
wenzelm@58618: text \<open>
wenzelm@62183:   The \<^emph>\<open>Documentation\<close> 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>\<open>User's Guide\<close> of
wenzelm@62183:   this sophisticated text editor. The same is accessible via the \<^verbatim>\<open>Help\<close> menu
wenzelm@62183:   or \<^verbatim>\<open>F1\<close> keyboard shortcut, using the built-in HTML viewer of Java/Swing.
wenzelm@62183:   The latter also includes \<^emph>\<open>Frequently Asked Questions\<close> 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@66683:   but users need 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: \<close>
wenzelm@54321: 
wenzelm@54321: 
wenzelm@58618: subsection \<open>Plugins\<close>
wenzelm@54321: 
wenzelm@58618: text \<open>
wenzelm@61574:   The \<^emph>\<open>Plugin Manager\<close> 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@66683:   The \<^emph>\<open>Isabelle\<close> plugin is responsible for the main Prover IDE functionality
wenzelm@66683:   of Isabelle/jEdit: it manages the prover session in the background. A few
wenzelm@66462:   additional plugins are bundled with Isabelle/jEdit for convenience or out of
wenzelm@66683:   necessity, notably \<^emph>\<open>Console\<close> with its \<^emph>\<open>Scala\<close> sub-plugin
wenzelm@66462:   (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
wenzelm@66462:   parsers for document tree structure (\secref{sec:sidekick}). The
wenzelm@66462:   \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
wenzelm@66462:   formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
wenzelm@66462:   (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
wenzelm@66683:   of bundled plugins, but have no particular use in Isabelle/jEdit.
wenzelm@66683: \<close>
wenzelm@54321: 
wenzelm@54321: 
wenzelm@58618: subsection \<open>Options \label{sec:options}\<close>
wenzelm@54321: 
wenzelm@61574: text \<open>
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>\<open>Utilities~/ Global
wenzelm@61574:   Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
wenzelm@69597:   two within the central options dialog. Changes are stored in \<^path>\<open>$JEDIT_SETTINGS/properties\<close> and \<^path>\<open>$JEDIT_SETTINGS/keymaps\<close>.
wenzelm@57310: 
wenzelm@57310:   Isabelle system options are managed by Isabelle/Scala and changes are stored
wenzelm@69597:   in \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close>, 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>\<open>public\<close> are configurable in
wenzelm@61574:   Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there
wenzelm@66683:   are various options for rendering document content, which are configurable
wenzelm@66683:   via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin Options~/
wenzelm@66683:   Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options.
wenzelm@66683:   Note that some of these options affect general parameters that are relevant
wenzelm@66683:   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@69597:   Isabelle/jEdit. Editing the generated \<^path>\<open>$JEDIT_SETTINGS/properties\<close>
wenzelm@69597:   or \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> manually while the
wenzelm@66683:   application is running may cause surprise due to lost updates!
wenzelm@61574: \<close>
wenzelm@54321: 
wenzelm@54321: 
wenzelm@58618: subsection \<open>Keymaps\<close>
wenzelm@54321: 
wenzelm@61574: text \<open>
wenzelm@62183:   Keyboard shortcuts are managed as a separate concept of \<^emph>\<open>keymap\<close> that is
wenzelm@61574:   configurable via \<^emph>\<open>Global Options~/ Shortcuts\<close>. The \<^verbatim>\<open>imported\<close> 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@66683:   Users may change their keymap later, but this may lead to conflicts with
wenzelm@66683:   \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
wenzelm@64513: 
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@66683:   while non-conflicting changes are applied implicitly. This action is
wenzelm@64513:   automatically invoked on Isabelle/jEdit startup.
wenzelm@58618: \<close>
wenzelm@54321: 
wenzelm@54321: 
wenzelm@58618: section \<open>Command-line invocation \label{sec:command-line}\<close>
wenzelm@57320: 
wenzelm@58618: text \<open>
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: \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
wenzelm@57320: 
wenzelm@57320:   Options are:
wenzelm@68370:     -A NAME      ancestor session for options -R and -S (default: parent)
wenzelm@62039:     -D NAME=X    set JVM system property
wenzelm@61132:     -J OPTION    add JVM runtime option
wenzelm@66683:                  (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
wenzelm@68370:     -R NAME      build image with requirements from other sessions
wenzelm@68370:     -S NAME      like option -R, with focus on selected session
wenzelm@57320:     -b           build only
wenzelm@57320:     -d DIR       include session directory
wenzelm@57320:     -f           fresh build
wenzelm@68541:     -i NAME      include session in name-space of theories
wenzelm@61132:     -j OPTION    add jEdit runtime option
wenzelm@66683:                  (default $JEDIT_OPTIONS)
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@69854:     -s           system build mode for session image (system_heaps=true)
wenzelm@69854:     -u           user build mode for session image (system_heaps=false)
wenzelm@57320: 
wenzelm@61512:   Start jEdit with Isabelle plugin setup and open FILES
wenzelm@61512:   (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}
wenzelm@57320: 
wenzelm@61574:   The \<^verbatim>\<open>-l\<close> 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@66683:   via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
wenzelm@68472:   "isabelle-system"}). By default, the specified image is checked and built on
wenzelm@69854:   demand, but option \<^verbatim>\<open>-n\<close> bypasses the implicit build process for the
wenzelm@69854:   selected session image. Options \<^verbatim>\<open>-s\<close> and \<^verbatim>\<open>-u\<close> override the default system
wenzelm@69854:   option @{system_option system_heaps}: this determines where to store the
wenzelm@69854:   session image of @{tool build}.
wenzelm@57320: 
wenzelm@68472:   The \<^verbatim>\<open>-R\<close> option builds an auxiliary logic image with all theories from
wenzelm@68472:   other sessions that are not already present in its parent; it also opens the
wenzelm@68472:   session \<^verbatim>\<open>ROOT\<close> entry in the editor to facilitate editing of the main
wenzelm@68472:   session. The \<^verbatim>\<open>-S\<close> option is like \<^verbatim>\<open>-R\<close>, with a focus on the selected
wenzelm@68472:   session and its descendants: the namespace of accessible theories is
wenzelm@68472:   restricted accordingly. This reduces startup time for big projects, notably
wenzelm@68472:   the ``Archive of Formal Proofs''. The \<^verbatim>\<open>-A\<close> option specifies and alternative
wenzelm@68472:   ancestor session for options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-S\<close>: this allows to restructure the
wenzelm@68472:   hierarchy of session images on the spot.
wenzelm@66987: 
wenzelm@68541:   The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of
wenzelm@68541:   theories: multiple occurrences are possible.
wenzelm@68541: 
wenzelm@61574:   The \<^verbatim>\<open>-m\<close> 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>\<open>Plugin Options\<close> dialog of
wenzelm@61574:   Isabelle/jEdit), without requiring command-line invocation.
wenzelm@57320: 
wenzelm@66683:   The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or
wenzelm@66683:   jEdit, respectively. The defaults are provided by the Isabelle settings
wenzelm@66683:   environment @{cite "isabelle-system"}, but note that these only work for the
wenzelm@66683:   command-line tool described here, and not the regular application.
wenzelm@57320: 
wenzelm@62039:   The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
wenzelm@62039:   directly to the underlying \<^verbatim>\<open>java\<close> process.
wenzelm@62039: 
wenzelm@61574:   The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> 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>\<open>jedit_build\<close> component from
wenzelm@68224:   \<^url>\<open>https://isabelle.in.tum.de/components\<close>. 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: \<open>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\<close>}
wenzelm@62014: 
wenzelm@62014:   The \<^verbatim>\<open>-c\<close> option merely checks the presence of the server, producing a
wenzelm@62183:   process return code accordingly.
wenzelm@62014: 
wenzelm@62014:   The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
wenzelm@62014:   different server name. The default server name is the official distribution
wenzelm@68394:   name (e.g.\ \<^verbatim>\<open>Isabelle2018\<close>). Thus @{tool jedit_client} can connect to the
wenzelm@62183:   Isabelle desktop application without further options.
wenzelm@62014: 
wenzelm@63987:   The \<^verbatim>\<open>-p\<close> 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>\<open>isabelle.jedit_server\<close> provides a different server
wenzelm@62183:   name, e.g.\ use \<^verbatim>\<open>isabelle jedit -Disabelle.jedit_server=\<close>\<open>name\<close> and
wenzelm@62036:   \<^verbatim>\<open>isabelle jedit_client -s\<close>~\<open>name\<close> to connect later on.
wenzelm@62014: \<close>
wenzelm@57320: 
wenzelm@57320: 
wenzelm@60291: section \<open>GUI rendering\<close>
wenzelm@60291: 
wenzelm@60291: subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close>
wenzelm@54321: 
wenzelm@60291: text \<open>
wenzelm@66683:   jEdit is a Java/AWT/Swing application with the 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>\<open>Metal\<close> is used by default.
wenzelm@54321: 
wenzelm@66683:     The Linux-specific \<^emph>\<open>GTK+\<close> often works as well, but the overall GTK theme
wenzelm@66683:     and options need to be selected to suite Java/AWT/Swing. Note that Java
wenzelm@66683:     Virtual Machine has no direct influence of GTK rendering.
wenzelm@54321: 
wenzelm@62183:     \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
wenzelm@54372: 
wenzelm@61574:     \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
wenzelm@54321: 
wenzelm@61574:     The bundled \<^emph>\<open>MacOSX\<close> 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>\<open>MacOSX\<close> 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@66683:   in mind that this extra variance of GUI functionality often causes problems.
wenzelm@66683:   The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work on all
wenzelm@66683:   platforms, although they are technically and stylistically outdated. The
wenzelm@66683:   historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
wenzelm@54372: 
wenzelm@66683:   Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the
wenzelm@66683:   GUI only partially: proper restart of Isabelle/jEdit is usually required.
wenzelm@60291: \<close>
wenzelm@60291: 
wenzelm@60291: 
wenzelm@60291: subsection \<open>Displays with very high resolution \label{sec:hdpi}\<close>
wenzelm@60291: 
wenzelm@60291: text \<open>
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@68736:   pixels as adequate for text rendering. After 2016, we have routinely seen
wenzelm@68736:   much higher resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or
wenzelm@68736:   ``Ultra HD'' / ``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>\<open>operating-system\<close> 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>\<open>GTK+\<close>,
wenzelm@62183:   \<^emph>\<open>Windows\<close>, \<^emph>\<open>Mac OS X\<close>, respectively. Alternatively, it is possible to use
wenzelm@62183:   the platform-independent \<^emph>\<open>Metal\<close> look-and-feel and readjust its main font
wenzelm@62183:   sizes via jEdit options explained below. The Isabelle/jEdit \<^bold>\<open>application\<close>
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>\<open>Global Options / Text Area / Text font\<close>: 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>\<open>Output\<close> (\secref{sec:output}) and \<^emph>\<open>State\<close>
wenzelm@62183:     (\secref{sec:state-output}) panels.
wenzelm@60291: 
wenzelm@61574:     \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: 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>\<open>Global Options / Appearance / Button, menu and label font\<close> as well as
wenzelm@61574:     \<^emph>\<open>List and text field font\<close>: this specifies the primary and secondary font
wenzelm@62183:     for the \<^emph>\<open>Metal\<close> look-and-feel (\secref{sec:look-and-feel}).
wenzelm@60291: 
wenzelm@61574:     \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: 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>\<open>Plugin Options / Console / General / Font\<close>: 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>\<open>Metal\<close> 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>\<open>Metal\<close>.
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: \<close>
wenzelm@54321: 
wenzelm@54321: 
wenzelm@62183: chapter \<open>Augmented jEdit functionality\<close>
wenzelm@62183: 
wenzelm@58618: section \<open>Dockable windows \label{sec:dockables}\<close>
wenzelm@57316: 
wenzelm@58618: text \<open>
wenzelm@61574:   In jEdit terminology, a \<^emph>\<open>view\<close> is an editor window with one or more \<^emph>\<open>text
wenzelm@61574:   areas\<close> that show the content of one or more \<^emph>\<open>buffers\<close>. A regular view may
wenzelm@61574:   be surrounded by \<^emph>\<open>dockable windows\<close> that show additional information in
wenzelm@61574:   arbitrary format, not just text; a \<^emph>\<open>plain view\<close> does not allow dockables.
wenzelm@61574:   The \<^emph>\<open>dockable window manager\<close> of jEdit organizes these dockable windows,
wenzelm@61574:   either as \<^emph>\<open>floating\<close> windows, or \<^emph>\<open>docked\<close> 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>\<open>the\<close> 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>\<open>HyperSearch Results\<close> or the \<^emph>\<open>File System Browser\<close>. 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>\<open>Documentation\<close>, \<^emph>\<open>State\<close>, \<^emph>\<open>Theories\<close> \<^emph>\<open>Output\<close>, \<^emph>\<open>Query\<close>. 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>\<open>dialog\<close> 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>\<open>Output\<close> (\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>\<open>Query\<close> (\secref{sec:query})
wenzelm@62184:   or \<^emph>\<open>Sledgehammer\<close> \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>\<open>Detach\<close>. This produces an independent copy of the
wenzelm@61477:   current output as a floating \<^emph>\<open>Info\<close> 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>\<open>Detach\<close> operation as an icon.
wenzelm@58618: \<close>
wenzelm@57316: 
wenzelm@57316: 
wenzelm@58618: section \<open>Isabelle symbols \label{sec:symbols}\<close>
wenzelm@57319: 
wenzelm@58618: text \<open>
wenzelm@61477:   Isabelle sources consist of \<^emph>\<open>symbols\<close> 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>\<open>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.\<close> 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>\<open>a\<close>'' or symbolic
wenzelm@61574:   ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
wenzelm@61574:   physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
wenzelm@61574:   example. This symbol interpretation is specified by the Isabelle system
wenzelm@63680:   distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the
wenzelm@69597:   user in \<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close>.
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>\<open>\<foobar>\<close>''. 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: \<close>
wenzelm@57319: 
wenzelm@61506: paragraph \<open>Encoding.\<close>
wenzelm@67304: 
wenzelm@62184: text \<open>Technically, the Unicode interpretation of Isabelle symbols is an
wenzelm@62184:   \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (\<^emph>\<open>not\<close> in the underlying
wenzelm@66462:   JVM). It is provided by the Isabelle Base plugin and enabled by default for
wenzelm@67304:   all source files in Isabelle/jEdit.
wenzelm@67304: 
wenzelm@67304:   Sometimes such defaults are reset accidentally, or malformed UTF-8 sequences
wenzelm@67304:   in the text force jEdit to fall back on a different encoding like
wenzelm@67304:   \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim ``\<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text
wenzelm@67304:   buffer instead of its Unicode rendering ``\<open>\<alpha>\<close>''. The jEdit menu operation
wenzelm@67304:   \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps to resolve such
wenzelm@67304:   problems (after repairing malformed parts of the text).
wenzelm@67304: 
wenzelm@67304:   If the loaded text already contains Unicode sequences that are in conflict
wenzelm@67304:   with the Isabelle symbol encoding, the fallback-encoding UTF-8 is used and
wenzelm@67304:   Isabelle symbols remain in literal \<^verbatim>\<open>\<symbol>\<close> form. The jEdit menu
wenzelm@67304:   operation \<^emph>\<open>Utilities~/ Buffer Options~/ Character encoding\<close> allows to
wenzelm@67304:   enforce the UTF-8-Isabelle, but this will also change original Unicode
wenzelm@67304:   text into Isabelle symbols when saving the file!
wenzelm@67304: \<close>
wenzelm@57319: 
wenzelm@61506: paragraph \<open>Font.\<close>
wenzelm@61506: text \<open>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@69343:   Isabelle/jEdit prefers its own font collection \<^verbatim>\<open>Isabelle DejaVu\<close>, which
wenzelm@69343:   ensures that all standard Isabelle symbols are shown on the screen (or
wenzelm@69343:   printer) as expected.
wenzelm@57319: 
wenzelm@57420:   Note that a Java/AWT/Swing application can load additional fonts only if
wenzelm@69343:   they are not installed on the operating system already! Outdated versions of
wenzelm@69343:   Isabelle fonts that happen to be provided by the operating system prevent
wenzelm@69343:   Isabelle/jEdit to use its bundled version. This could lead to missing glyphs
wenzelm@69343:   (black rectangles), when the system version of a font is older than the
wenzelm@69343:   application version. This problem can be avoided by refraining to
wenzelm@69343:   ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the first place, although it
wenzelm@69343:   might be tempting to use the same font in other applications.
wenzelm@62184: 
wenzelm@69343:   HTML pages generated by Isabelle refer to the same Isabelle fonts as a
wenzelm@62184:   server-side resource. Thus a web-browser can use that without requiring a
wenzelm@62184:   locally installed copy.
wenzelm@61506: \<close>
wenzelm@57319: 
wenzelm@61506: paragraph \<open>Input methods.\<close>
wenzelm@61506: text \<open>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>\<open>input methods\<close>. Regular jEdit also provides various ways to
wenzelm@61506:   work with \<^emph>\<open>abbreviations\<close> 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>\<open>Symbols\<close> 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>\<open>symbol
wenzelm@61504:   abbreviations\<close> (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>\<open>copy\<close> in secondary Isabelle/jEdit
wenzelm@61504:   windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or \<^verbatim>\<open>C+INSERT\<close>, 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>\<open>\<lambda>\<close>, or its name preceded by backslash
wenzelm@61504:   \<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.
wenzelm@57319: 
wenzelm@57319:   The following table is an extract of the information provided by the
wenzelm@63680:   standard \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> file:
wenzelm@57319: 
wenzelm@61415:   \<^medskip>
wenzelm@57319:   \begin{tabular}{lll}
wenzelm@61477:     \<^bold>\<open>symbol\<close> & \<^bold>\<open>name with backslash\<close> & \<^bold>\<open>abbreviation\<close> \\\hline
wenzelm@61503:     \<open>\<lambda>\<close> & \<^verbatim>\<open>\lambda\<close> & \<^verbatim>\<open>%\<close> \\
wenzelm@61503:     \<open>\<Rightarrow>\<close> & \<^verbatim>\<open>\Rightarrow\<close> & \<^verbatim>\<open>=>\<close> \\
wenzelm@61503:     \<open>\<Longrightarrow>\<close> & \<^verbatim>\<open>\Longrightarrow\<close> & \<^verbatim>\<open>==>\<close> \\[0.5ex]
wenzelm@61503:     \<open>\<And>\<close> & \<^verbatim>\<open>\And\<close> & \<^verbatim>\<open>!!\<close> \\
wenzelm@61503:     \<open>\<equiv>\<close> & \<^verbatim>\<open>\equiv\<close> & \<^verbatim>\<open>==\<close> \\[0.5ex]
wenzelm@61503:     \<open>\<forall>\<close> & \<^verbatim>\<open>\forall\<close> & \<^verbatim>\<open>!\<close> \\
wenzelm@61503:     \<open>\<exists>\<close> & \<^verbatim>\<open>\exists\<close> & \<^verbatim>\<open>?\<close> \\
wenzelm@61503:     \<open>\<longrightarrow>\<close> & \<^verbatim>\<open>\longrightarrow\<close> & \<^verbatim>\<open>-->\<close> \\
wenzelm@61503:     \<open>\<and>\<close> & \<^verbatim>\<open>\and\<close> & \<^verbatim>\<open>&\<close> \\
wenzelm@61503:     \<open>\<or>\<close> & \<^verbatim>\<open>\or\<close> & \<^verbatim>\<open>|\<close> \\
wenzelm@61503:     \<open>\<not>\<close> & \<^verbatim>\<open>\not\<close> & \<^verbatim>\<open>~\<close> \\
wenzelm@61503:     \<open>\<noteq>\<close> & \<^verbatim>\<open>\noteq\<close> & \<^verbatim>\<open>~=\<close> \\
wenzelm@61503:     \<open>\<in>\<close> & \<^verbatim>\<open>\in\<close> & \<^verbatim>\<open>:\<close> \\
wenzelm@61503:     \<open>\<notin>\<close> & \<^verbatim>\<open>\notin\<close> & \<^verbatim>\<open>~:\<close> \\
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>\<open>!\<close> or \<^verbatim>\<open>ALL\<close> 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>\<open>C+b\<close> explained in \secref{sec:completion}).
wenzelm@61506: \<close>
wenzelm@57319: 
wenzelm@61506: paragraph \<open>Control symbols.\<close>
wenzelm@61506: text \<open>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>\<open>Symbols\<close> 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>\<open>style\<close> & \<^bold>\<open>symbol\<close> & \<^bold>\<open>shortcut\<close> & \<^bold>\<open>action\<close> \\\hline
wenzelm@61503:     superscript & \<^verbatim>\<open>\<^sup>\<close> & \<^verbatim>\<open>C+e UP\<close> & @{action_ref "isabelle.control-sup"} \\
wenzelm@61503:     subscript & \<^verbatim>\<open>\<^sub>\<close> & \<^verbatim>\<open>C+e DOWN\<close> & @{action_ref "isabelle.control-sub"} \\
wenzelm@61503:     bold face & \<^verbatim>\<open>\<^bold>\<close> & \<^verbatim>\<open>C+e RIGHT\<close> & @{action_ref "isabelle.control-bold"} \\
wenzelm@61503:     emphasized & \<^verbatim>\<open>\<^emph>\<close> & \<^verbatim>\<open>C+e LEFT\<close> & @{action_ref "isabelle.control-emph"} \\
wenzelm@61503:     reset & & \<^verbatim>\<open>C+e BACK_SPACE\<close> & @{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>\<open>\sup\<close>, \<^verbatim>\<open>\sub\<close>, \<^verbatim>\<open>\bold\<close>, \<^verbatim>\<open>\emph\<close> 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: \<close>
wenzelm@57319: 
wenzelm@57319: 
wenzelm@58618: section \<open>Scala console \label{sec:scala-console}\<close>
wenzelm@57319: 
wenzelm@58618: text \<open>
wenzelm@61574:   The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters), e.g.\
wenzelm@61574:   \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and the
wenzelm@61574:   cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar
wenzelm@61574:   functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and \<^verbatim>\<open>*shell*\<close>.
wenzelm@57319: 
wenzelm@61574:   Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, 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>\<open>isabelle\<close> and
wenzelm@61503:   \<^verbatim>\<open>isabelle.jedit\<close>.
wenzelm@57603: 
wenzelm@61574:   For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, and \<^verbatim>\<open>view\<close>
wenzelm@61574:   to the current editor view of jEdit. The Scala expression
wenzelm@61574:   \<^verbatim>\<open>PIDE.snapshot(view)\<close> 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: \<close>
wenzelm@57319: 
wenzelm@57319: 
wenzelm@58618: section \<open>File-system access\<close>
wenzelm@57318: 
wenzelm@58618: text \<open>
wenzelm@57420:   File specifications in jEdit follow various formats and conventions
wenzelm@61477:   according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by
wenzelm@61503:   additional plugins. This allows to access remote files via the \<^verbatim>\<open>http:\<close>
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>\<open>all\<close>
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>\<open>/cygdrive/c\<close>). Moreover,
wenzelm@62184:   environment variables from the Isabelle process may be used freely, e.g.\
wenzelm@63680:   \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME/README\<close>. There are special
wenzelm@63680:   shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.
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>\<open>$ISABELLE_HOME\<close>, \<^verbatim>\<open>$ISABELLE_HOME_USER\<close>, \<^verbatim>\<open>$JEDIT_HOME\<close>,
wenzelm@63749:   \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> 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: \<close>
wenzelm@57318: 
wenzelm@57318: 
wenzelm@64515: section \<open>Indentation\<close>
wenzelm@64515: 
wenzelm@64515: text \<open>
wenzelm@64515:   Isabelle/jEdit augments the existing indentation facilities of jEdit to take
wenzelm@64515:   the structure of theory and proof texts into account. There is also special
wenzelm@64515:   support for unstructured proof scripts.
wenzelm@64515: 
wenzelm@64515:     \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar.
wenzelm@64515: 
wenzelm@64515:     Action @{action "indent-lines"} (shortcut \<^verbatim>\<open>C+i\<close>) indents the current line
wenzelm@64515:     according to command keywords and some command substructure: this
wenzelm@64515:     approximation may need further manual tuning.
wenzelm@64515: 
wenzelm@64515:     Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the old
wenzelm@64515:     and the new line according to command keywords only: this leads to precise
wenzelm@64515:     alignment of the main Isar language elements. This depends on option
wenzelm@64515:     @{system_option_def "jedit_indent_newline"} (enabled by default).
wenzelm@64515: 
wenzelm@66681:     Regular input (via keyboard or completion) indents the current line
wenzelm@66683:     whenever an new keyword is emerging at the start of the line. This depends
wenzelm@66683:     on option @{system_option_def "jedit_indent_input"} (enabled by default).
wenzelm@66681: 
wenzelm@64515:     \<^descr>[Semantic indentation] adds additional white space to unstructured proof
wenzelm@64515:     scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
wenzelm@64515:     of ongoing document processing and may thus lag behind, when the user is
wenzelm@64515:     editing too quickly; see also option @{system_option_def
wenzelm@64515:     "jedit_script_indent"} and @{system_option_def
wenzelm@64515:     "jedit_script_indent_limit"}.
wenzelm@64515: 
wenzelm@64515:   The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
wenzelm@66681:   Isabelle / General\<close>. A prerequisite for advanced indentation is \<^emph>\<open>Utilities
wenzelm@66681:   / Buffer Options / Automatic indentation\<close>: it needs to be set to \<^verbatim>\<open>full\<close>
wenzelm@66681:   (default).
wenzelm@64515: \<close>
wenzelm@64515: 
wenzelm@64515: 
wenzelm@62184: section \<open>SideKick parsers \label{sec:sidekick}\<close>
wenzelm@62184: 
wenzelm@62184: text \<open>
wenzelm@62184:   The \<^emph>\<open>SideKick\<close> 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>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system
wenzelm@64513:   \<^verbatim>\<open>options\<close>, 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>\<open>isabelle\<close>: 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>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>
wenzelm@64513:   end\<close> 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>\<open>isabelle-ml\<close> 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>\<open>isabelle-markup\<close> 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: \<close>
wenzelm@62184: 
wenzelm@62184: 
wenzelm@58618: chapter \<open>Prover IDE functionality \label{sec:document-model}\<close>
wenzelm@57315: 
wenzelm@58618: section \<open>Document model \label{sec:document-model}\<close>
wenzelm@57322: 
wenzelm@58618: text \<open>
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: \<close>
wenzelm@57322: 
wenzelm@54322: 
wenzelm@58618: subsection \<open>Editor buffers and document nodes \label{sec:buffer-node}\<close>
wenzelm@57322: 
wenzelm@58618: text \<open>
wenzelm@61477:   As a regular text editor, jEdit maintains a collection of \<^emph>\<open>buffers\<close> to
wenzelm@57322:   store text files; each buffer may be associated with any number of visible
wenzelm@61574:   \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> 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>\<open>mode\<close> & \<^bold>\<open>file name\<close> & \<^bold>\<open>content\<close> \\\hline
wenzelm@62185:   \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>*.thy\<close> & theory source \\
wenzelm@62185:   \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>*.ML\<close> & Isabelle/ML source \\
wenzelm@62185:   \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>*.sml\<close> or \<^verbatim>\<open>*.sig\<close> & Standard ML source \\
wenzelm@62185:   \<^verbatim>\<open>isabelle-root\<close> & \<^verbatim>\<open>ROOT\<close> & session root \\
wenzelm@62185:   \<^verbatim>\<open>isabelle-options\<close> & & Isabelle options \\
wenzelm@62185:   \<^verbatim>\<open>isabelle-news\<close> & & 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>\<open>document nodes\<close>. The overall document structure is defined by the theory
wenzelm@61574:   nodes in two dimensions:
wenzelm@57322: 
wenzelm@61574:     \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory header\<close> using
wenzelm@61574:     concrete syntax of the @{command_ref theory} command @{cite
wenzelm@61574:     "isabelle-isar-ref"};
wenzelm@57322: 
wenzelm@66683:     \<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>load
wenzelm@61574:     commands\<close>, 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: \<close>
wenzelm@57322: 
wenzelm@57322: 
wenzelm@58618: subsection \<open>Theories \label{sec:theories}\<close>
wenzelm@57322: 
wenzelm@58618: text \<open>
wenzelm@61574:   The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview
wenzelm@61574:   of the status of continuous checking of theory nodes within the document
wenzelm@66683:   model.
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@64842:   Theory imports are resolved automatically by the PIDE document model: all
wenzelm@64842:   required files are loaded and stored internally, without the need to open
wenzelm@64842:   corresponding jEdit buffers. Opening or closing editor buffers later on has
wenzelm@66683:   no direct impact on the formal document content: it only affects visibility.
wenzelm@64842: 
wenzelm@66683:   In contrast, auxiliary files (e.g.\ from @{command ML_file} commands) are
wenzelm@66683:   \<^emph>\<open>not\<close> resolved within the editor by default, but the prover process takes
wenzelm@66683:   care of that. This may be changed by enabling the system option
wenzelm@66683:   @{system_option jedit_auto_resolve}: it ensures that all files are uniformly
wenzelm@66683:   provided by the editor.
wenzelm@54321: 
wenzelm@61415:   \<^medskip>
wenzelm@61574:   The visible \<^emph>\<open>perspective\<close> 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>\<open>Theories\<close> 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>\<open>required\<close> 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@66683:   The \<^emph>\<open>Purge\<close> button restricts the document model to theories that are
wenzelm@66683:   required for open editor buffers: inaccessible theories are removed and will
wenzelm@66683:   be rechecked when opened or imported later.
wenzelm@66683: 
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>\<open>sendback\<close> markup by automated provers or
wenzelm@62185:   disprovers in the background). \<close>
wenzelm@57322: 
wenzelm@57322: 
wenzelm@58618: subsection \<open>Auxiliary files \label{sec:aux-files}\<close>
wenzelm@57322: 
wenzelm@58618: text \<open>
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>\<open>Pure\<close> as logic session image, the exploration may start
wenzelm@63680:   at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
wenzelm@66683:   \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example. It is also possible to
wenzelm@66683:   explore the Isabelle/Pure bootstrap process (a virtual copy) by opening
wenzelm@66683:   \<^file>\<open>$ISABELLE_HOME/src/Pure/ROOT.ML\<close> like a theory in the Prover IDE.
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>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, 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: \<close>
wenzelm@54322: 
wenzelm@54352: 
wenzelm@58618: section \<open>Output \label{sec:output}\<close>
wenzelm@54353: 
wenzelm@58618: text \<open>
wenzelm@61574:   Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. 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>\<open>Theories\<close> panel, \<^emph>\<open>Output\<close> 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>\<open>Theories\<close> 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@66683:   execution status of commands. The border of each rectangle indicates the
wenzelm@66683:   overall status of processing: a thick border means it is \<^emph>\<open>finished\<close> or
wenzelm@66683:   \<^emph>\<open>failed\<close> (with color for errors). A double-click on one of the theory
wenzelm@66683:   entries with their status overview opens the corresponding text buffer,
wenzelm@66683:   without moving the cursor to a specific point.
wenzelm@54353: 
wenzelm@61415:   \<^medskip>
wenzelm@62185:   The \<^emph>\<open>Output\<close> 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>\<open>Auto update\<close> and \<^emph>\<open>Update\<close>. This is particularly useful for multiple
wenzelm@62185:   instances of the \<^emph>\<open>Output\<close> panel to look at different situations.
wenzelm@62185:   Alternatively, the panel can be turned into a passive \<^emph>\<open>Info\<close> window via the
wenzelm@62185:   \<^emph>\<open>Detach\<close> 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>\<open>proof state\<close> and \<^emph>\<open>tracing\<close>.
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: \<close>
wenzelm@54353: 
wenzelm@54353: 
wenzelm@62185: section \<open>Proof state \label{sec:state-output}\<close>
wenzelm@62154: 
wenzelm@62154: text \<open>
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>\<open>State\<close> panel shows exclusively such
wenzelm@62185:   proof state messages without further distraction, while all other messages
wenzelm@62185:   are displayed in \<^emph>\<open>Output\<close> (\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>\<open>State\<close> panel open (as
wenzelm@62185:   floating windows), with \<^emph>\<open>Auto update\<close> disabled to look at an old situation
wenzelm@62185:   while the proof text in the vicinity is changed. The \<^emph>\<open>Update\<close> 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>\<open>S+ENTER\<close>).
wenzelm@62185: 
wenzelm@62185:   On small screens, it is occasionally useful to have all messages
wenzelm@62185:   concatenated in the regular \<^emph>\<open>Output\<close> panel, e.g.\ see
wenzelm@62185:   \figref{fig:output-including-state}.
wenzelm@62185: 
wenzelm@62185:   \<^medskip>
wenzelm@62185:   The mechanics of \<^emph>\<open>Output\<close> versus \<^emph>\<open>State\<close> are slightly different:
wenzelm@62185: 
wenzelm@62185:     \<^item> \<^emph>\<open>Output\<close> 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>\<open>State\<close> 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>\<open>Auto update\<close>)
wenzelm@62185:     or the \<^emph>\<open>Update\<close> 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>\<open>State\<close> panel.
wenzelm@62154: \<close>
wenzelm@62154: 
wenzelm@62185: 
wenzelm@58618: section \<open>Query \label{sec:query}\<close>
wenzelm@57311: 
wenzelm@58618: text \<open>
wenzelm@61574:   The \<^emph>\<open>Query\<close> 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>\<open>Find Theorems\<close>,
wenzelm@62249:   \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual
wenzelm@62249:   in jEdit, multiple \<^emph>\<open>Query\<close> 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>\<open>Apply\<close> 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>\<open>Search\<close> 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>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>
wenzelm@61574:     This may serve as an additional visual filter of the result.
wenzelm@57311: 
wenzelm@61574:     \<^item> The \<^emph>\<open>Zoom\<close> 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>\<open>Info\<close>
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: \<close>
wenzelm@57311: 
wenzelm@57311: 
wenzelm@58618: subsection \<open>Find theorems\<close>
wenzelm@57311: 
wenzelm@58618: text \<open>
wenzelm@61574:   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory
wenzelm@61574:   or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A
wenzelm@68042:   single criterion has the following syntax:
wenzelm@57311: 
wenzelm@69597:   \<^rail>\<open>
wenzelm@62969:     ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
wenzelm@57313:       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
wenzelm@69597:   \<close>
wenzelm@57313: 
wenzelm@61574:   See also the Isar command @{command_ref find_theorems} in @{cite
wenzelm@61574:   "isabelle-isar-ref"}.
wenzelm@58618: \<close>
wenzelm@57311: 
wenzelm@57311: 
wenzelm@58618: subsection \<open>Find constants\<close>
wenzelm@57311: 
wenzelm@58618: text \<open>
wenzelm@61574:   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type
wenzelm@61574:   meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single
wenzelm@68042:   criterion has the following syntax:
wenzelm@57313: 
wenzelm@69597:   \<^rail>\<open>
wenzelm@57313:     ('-'?)
wenzelm@62969:       ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
wenzelm@69597:   \<close>
wenzelm@57313: 
wenzelm@58554:   See also the Isar command @{command_ref find_consts} in @{cite
wenzelm@58554:   "isabelle-isar-ref"}.
wenzelm@58618: \<close>
wenzelm@57311: 
wenzelm@57311: 
wenzelm@58618: subsection \<open>Print context\<close>
wenzelm@57311: 
wenzelm@58618: text \<open>
wenzelm@61574:   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> 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: \<close>
wenzelm@57311: 
wenzelm@57311: 
wenzelm@58618: section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close>
wenzelm@54352: 
wenzelm@58618: text \<open>
wenzelm@62249:   Formally processed text (prover input or output) contains rich markup that
wenzelm@62249:   can be explored by using the \<^verbatim>\<open>CONTROL\<close> modifier key on Linux and Windows,
wenzelm@62249:   or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse while the modifier is
wenzelm@62249:   pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup)
wenzelm@62249:   and/or a \<^emph>\<open>hyperlink\<close> (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>\<open>close\<close> or \<^emph>\<open>detach\<close> the
wenzelm@61574:   window, turning it into a separate \<^emph>\<open>Info\<close> window managed by jEdit. The
wenzelm@61574:   \<^verbatim>\<open>ESCAPE\<close> key closes \<^emph>\<open>all\<close> 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>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still
wenzelm@61574:   pressed). Such jumps to other text locations are recorded by the
wenzelm@61574:   \<^emph>\<open>Navigator\<close> 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: \<close>
wenzelm@54321: 
wenzelm@54321: 
wenzelm@64514: section \<open>Formal scopes and semantic selection\<close>
wenzelm@64514: 
wenzelm@64514: text \<open>
wenzelm@64514:   Formal entities are semantically annotated in the source text as explained
wenzelm@64514:   in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the
wenzelm@64514:   defining position with all its referencing positions. This correspondence is
wenzelm@64514:   highlighted in the text according to the cursor position, see also
wenzelm@64514:   \figref{fig:scope1}. Here the referencing positions are rendered with an
wenzelm@64514:   additional border, in reminiscence to a hyperlink: clicking there moves the
wenzelm@64514:   cursor to the original defining position.
wenzelm@64514: 
wenzelm@64514:   \begin{figure}[!htb]
wenzelm@64514:   \begin{center}
wenzelm@64514:   \includegraphics[scale=0.5]{scope1}
wenzelm@64514:   \end{center}
wenzelm@64514:   \caption{Scope of formal entity: defining vs.\ referencing positions}
wenzelm@64514:   \label{fig:scope1}
wenzelm@64514:   \end{figure}
wenzelm@64514: 
wenzelm@64514:   The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
wenzelm@64514:   supports semantic selection of all occurrences of the formal entity at the
wenzelm@64514:   caret position. This facilitates systematic renaming, using regular jEdit
wenzelm@64514:   editing of a multi-selection, see also \figref{fig:scope2}.
wenzelm@64514: 
wenzelm@64514:   \begin{figure}[!htb]
wenzelm@64514:   \begin{center}
wenzelm@64514:   \includegraphics[scale=0.5]{scope2}
wenzelm@64514:   \end{center}
wenzelm@64514:   \caption{The result of semantic selection and systematic renaming}
wenzelm@64514:   \label{fig:scope2}
wenzelm@64514:   \end{figure}
wenzelm@64514: \<close>
wenzelm@64514: 
wenzelm@64514: 
wenzelm@58618: section \<open>Completion \label{sec:completion}\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
wenzelm@61477:   Smart completion of partial input is the IDE functionality \<^emph>\<open>par
wenzelm@61477:   excellance\<close>. 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>\<open>Explicit completion\<close> is triggered by the action @{action_ref
wenzelm@61574:   "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\<open>C+b\<close>, and
wenzelm@61574:   thus overrides the jEdit default for @{action_ref "complete-word"}.
wenzelm@57335: 
wenzelm@61574:   \<^emph>\<open>Implicit completion\<close> 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>\<open>Plugin Options~/ Isabelle~/
wenzelm@61574:   General~/ Completion\<close>. 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: \<close>
wenzelm@57324: 
wenzelm@57324: 
wenzelm@58618: subsection \<open>Varieties of completion \label{sec:completion-varieties}\<close>
wenzelm@57324: 
wenzelm@58618: subsubsection \<open>Built-in templates\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
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>\<open>`\<close> (single ASCII back-quote) or \<^verbatim>\<open>"\<close> (double ASCII quote) support
wenzelm@64513:     \<^emph>\<open>quotations\<close> 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 ``\<open>\<open>\<box>\<close>\<close>'', 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>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'', where the box indicates
wenzelm@61574:     the cursor position after insertion. Here it is convenient to use the
wenzelm@61574:     wildcard ``\<^verbatim>\<open>__\<close>'' 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: \<close>
wenzelm@57335: 
wenzelm@57327: 
wenzelm@58618: subsubsection \<open>Syntax keywords\<close>
wenzelm@57335: 
wenzelm@58618: text \<open>
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 \<open>simp\<close>.
wenzelm@58618: \<close>
wenzelm@57324: 
wenzelm@57324: 
wenzelm@58618: subsubsection \<open>Isabelle symbols\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
wenzelm@57325:   The completion tables for Isabelle symbols (\secref{sec:symbols}) are
wenzelm@69597:   determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and \<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close> for each symbol specification as follows:
wenzelm@57325: 
wenzelm@61415:   \<^medskip>
wenzelm@57325:   \begin{tabular}{ll}
wenzelm@61477:   \<^bold>\<open>completion entry\<close> & \<^bold>\<open>example\<close> \\\hline
wenzelm@61503:   literal symbol & \<^verbatim>\<open>\<forall>\<close> \\
wenzelm@61503:   symbol name with backslash & \<^verbatim>\<open>\\<close>\<^verbatim>\<open>forall\<close> \\
wenzelm@61503:   symbol abbreviation & \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>!\<close> \\
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 \<open>\<forall>\<close> of the underlying symbol \<^verbatim>\<open>\<forall>\<close>.
wenzelm@57325: 
wenzelm@61574:   A symbol abbreviation that is a plain word, like \<^verbatim>\<open>ALL\<close>, is treated like a
wenzelm@61574:   syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close> are inserted more
wenzelm@61574:   aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.
wenzelm@57324: 
wenzelm@62250:   Completion via abbreviations like \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>-->\<close> depends on the semantic
wenzelm@62250:   language context (\secref{sec:completion-context}). In contrast, backslash
wenzelm@68736:   sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require additional
wenzelm@68736:   interaction to confirm (via popup). This is important in ambiguous
wenzelm@68736:   situations, e.g.\ for Isabelle document source, which may contain formal
wenzelm@68736:   symbols or informal {\LaTeX} macros. Backslash sequences also help when
wenzelm@68736:   input is broken, and thus escapes its normal semantic context: e.g.\
wenzelm@68736:   antiquotations or string literals in ML, which do not allow arbitrary
wenzelm@68736:   backslash sequences.
wenzelm@62250: 
wenzelm@68736:   Special symbols like \<^verbatim>\<open>\<comment>\<close> or control symbols like \<^verbatim>\<open>\<^cancel>\<close>,
wenzelm@68736:   \<^verbatim>\<open>\<^latex>\<close>, \<^verbatim>\<open>\<^binding>\<close> can have an argument: completing on a name
wenzelm@68736:   prefix offers a template with an empty cartouche. Thus completion of \<^verbatim>\<open>\co\<close>
wenzelm@68736:   or \<^verbatim>\<open>\ca\<close> allows to compose formal document comments quickly.\<^footnote>\<open>It is
wenzelm@68736:   customary to put a space between \<^verbatim>\<open>\<comment>\<close> and its argument, while
wenzelm@68736:   control symbols do \<^emph>\<open>not\<close> allow extra space here.\<close>
wenzelm@58618: \<close>
wenzelm@57324: 
wenzelm@57324: 
wenzelm@64513: subsubsection \<open>User-defined abbreviations\<close>
wenzelm@64513: 
wenzelm@64513: text \<open>
wenzelm@64513:   The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> 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>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.
wenzelm@64513: 
wenzelm@64513:   The \<^emph>\<open>Symbols\<close> panel shows the abbreviations that are available in the
wenzelm@64513:   current theory buffer (according to its \<^theory_text>\<open>imports\<close>) in the \<^verbatim>\<open>Abbrevs\<close> tab.
wenzelm@64513: \<close>
wenzelm@64513: 
wenzelm@64513: 
wenzelm@58618: subsubsection \<open>Name-space entries\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
wenzelm@57324:   This is genuine semantic completion, using information from the prover, so
wenzelm@61477:   it requires some delay. A \<^emph>\<open>failed name-space lookup\<close> 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>\<open>not\<close> 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>\<open>foo\<close> and \<^verbatim>\<open>foobar\<close> are known, the input
wenzelm@61574:   \<^verbatim>\<open>foo\<close> remains unchanged, but \<^verbatim>\<open>foo_\<close> may be completed to \<^verbatim>\<open>foo\<close> or
wenzelm@61574:   \<^verbatim>\<open>foobar\<close>.
wenzelm@57324: 
wenzelm@61574:   The special identifier ``\<^verbatim>\<open>__\<close>'' 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: \<close>
wenzelm@57324: 
wenzelm@57324: 
wenzelm@58618: subsubsection \<open>File-system paths\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
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>\<open>master
wenzelm@62250:   directory\<close> 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: \<close>
wenzelm@57324: 
wenzelm@57324: 
wenzelm@58618: subsubsection \<open>Spell-checking\<close>
wenzelm@57328: 
wenzelm@58618: text \<open>
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>\<open>C+b\<close>.
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: \<close>
wenzelm@57328: 
wenzelm@57328: 
wenzelm@58618: subsection \<open>Semantic completion context \label{sec:completion-context}\<close>
wenzelm@57325: 
wenzelm@58618: text \<open>
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>\<open>language context\<close> 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>\<open>=>\<close>'' is \<^emph>\<open>not\<close> completed in
wenzelm@62250:   regular ML source, but is completed within ML strings, comments,
wenzelm@62250:   antiquotations. Backslash representations of symbols like ``\<^verbatim>\<open>\foobar\<close>'' or
wenzelm@62250:   ``\<^verbatim>\<open>\<foobar>\<close>'' work in any context --- after additional confirmation.
wenzelm@57325: 
wenzelm@61574:   The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional situations, to
wenzelm@61574:   tell that some language keywords should be excluded from further completion
wenzelm@62250:   attempts. For example, ``\<^verbatim>\<open>:\<close>'' within accepted Isar syntax looses its
wenzelm@62250:   meaning as abbreviation for symbol ``\<open>\<in>\<close>''.
wenzelm@58618: \<close>
wenzelm@57325: 
wenzelm@57325: 
wenzelm@58618: subsection \<open>Input events \label{sec:completion-input}\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
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>\<open>C+b\<close>. 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>\<open>Global Options~/
wenzelm@61574:   Shortcuts\<close> 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: \<close>
wenzelm@57324: 
wenzelm@57324: 
wenzelm@58618: subsection \<open>Completion popup \label{sec:completion-popup}\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
wenzelm@61574:   A \<^emph>\<open>completion popup\<close> 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>\<open>ENTER\<close>, \<^verbatim>\<open>TAB\<close>, \<^verbatim>\<open>ESCAPE\<close>, \<^verbatim>\<open>UP\<close>, \<^verbatim>\<open>DOWN\<close>, \<^verbatim>\<open>PAGE_UP\<close>,
wenzelm@61574:   \<^verbatim>\<open>PAGE_DOWN\<close>, 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>\<open>key\<close> & \<^bold>\<open>action\<close> \\\hline
wenzelm@61503:   \<^verbatim>\<open>ENTER\<close> & select completion (if @{system_option jedit_completion_select_enter}) \\
wenzelm@61503:   \<^verbatim>\<open>TAB\<close> & select completion (if @{system_option jedit_completion_select_tab}) \\
wenzelm@61503:   \<^verbatim>\<open>ESCAPE\<close> & dismiss popup \\
wenzelm@61503:   \<^verbatim>\<open>UP\<close> & move up one item \\
wenzelm@61503:   \<^verbatim>\<open>DOWN\<close> & move down one item \\
wenzelm@61503:   \<^verbatim>\<open>PAGE_UP\<close> & move up one page of items \\
wenzelm@61503:   \<^verbatim>\<open>PAGE_DOWN\<close> & 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: \<close>
wenzelm@57324: 
wenzelm@57324: 
wenzelm@58618: subsection \<open>Insertion \label{sec:completion-insert}\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
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>\<open>text selection\<close>. 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>\<open>HyperSearch\<close>:
wenzelm@61574:   clicking on one of the items in the \<^emph>\<open>HyperSearch Results\<close> 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>\<open>C+b\<close>, e.g.\ to replace occurrences
wenzelm@61574:   of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>.
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>\<open>ESCAPE\<close> is required to reset the selection and to continue
wenzelm@61574:   typing more text.
wenzelm@58618: \<close>
wenzelm@57324: 
wenzelm@57324: 
wenzelm@58618: subsection \<open>Options \label{sec:completion-options}\<close>
wenzelm@57324: 
wenzelm@58618: text \<open>
wenzelm@57324:   This is a summary of Isabelle/Scala system options that are relevant for
wenzelm@61574:   completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>
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>\<open>> 0\<close> 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>\<open>= true\<close> means that
wenzelm@61574:   abbreviations of Isabelle symbols are handled nonetheless.
wenzelm@57332: 
wenzelm@66158:   \<^item> @{system_option_def 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@69597:   permanent dictionary updates is stored in the directory \<^path>\<open>$ISABELLE_HOME_USER/dictionaries\<close>, in a separate file for each dictionary.
wenzelm@57332: 
wenzelm@67395:   \<^item> @{system_option_def spell_checker_include} 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@67395: 
wenzelm@67395:   \<^item> @{system_option_def spell_checker_exclude} specifies a comma-separated
wenzelm@67395:   list of markup elements that disable spell-checking (e.g.\ in nested
wenzelm@67395:   antiquotations).
wenzelm@58618: \<close>
wenzelm@54361: 
wenzelm@54361: 
wenzelm@58618: section \<open>Automatically tried tools \label{sec:auto-tools}\<close>
wenzelm@54353: 
wenzelm@58618: text \<open>
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>\<open>asynchronous print functions\<close>. 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>\<open>information
wenzelm@61574:   messages\<close>, 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>\<open>sendback\<close> 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>\<open>Plugin Options~/ Isabelle~/
wenzelm@61574:   General~/ Automatically tried tools\<close>):
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>\<open>enabled\<close> 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>\<open>enabled\<close> 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: \<close>
wenzelm@54353: 
wenzelm@54353: 
wenzelm@58618: section \<open>Sledgehammer \label{sec:sledgehammer}\<close>
wenzelm@54353: 
wenzelm@61574: text \<open>
wenzelm@61574:   The \<^emph>\<open>Sledgehammer\<close> 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>\<open>Apply\<close> 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>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close>
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>\<open>sendback\<close>, 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: \<close>
wenzelm@54353: 
wenzelm@54353: 
wenzelm@60255: chapter \<open>Isabelle document preparation\<close>
wenzelm@60255: 
wenzelm@61574: text \<open>
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: \<close>
wenzelm@60255: 
wenzelm@60255: 
wenzelm@60255: section \<open>Document outline\<close>
wenzelm@60255: 
wenzelm@61574: text \<open>
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>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The default
wenzelm@61574:   mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions, statements, and
wenzelm@61574:   proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the document structure of the
wenzelm@61574:   SideKick parser, as explained above.
wenzelm@61574: \<close>
wenzelm@60264: 
wenzelm@60255: 
wenzelm@62154: section \<open>Markdown structure\<close>
wenzelm@62154: 
wenzelm@62154: text \<open>
wenzelm@62251:   Document text is internally structured in paragraphs and nested lists, using
wenzelm@63680:   notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>. There are
wenzelm@63680:   special control symbols for items of different kinds of lists, corresponding
wenzelm@63680:   to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This is illustrated
wenzelm@63680:   in for \<^verbatim>\<open>itemize\<close> 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>\<open>CONTROL\<close> / \<^verbatim>\<open>COMMAND\<close> as usual
wenzelm@62251:   (\secref{sec:tooltips-hyperlinks}).
wenzelm@62154: \<close>
wenzelm@62154: 
wenzelm@62154: 
wenzelm@62184: section \<open>Citations and Bib{\TeX} entries \label{sec:bibtex}\<close>
wenzelm@60255: 
wenzelm@61574: text \<open>
wenzelm@61574:   Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> 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 \<open>@{cite}\<close> 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>\<open>not\<close> know about the actual Bib{\TeX} environment used
wenzelm@61574:   in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> 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@68736:   Isabelle/jEdit also provides IDE support for editing \<^verbatim>\<open>.bib\<close> 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@68736:   \figref{fig:bibtex-mode}. Semantic checking with errors and warnings is
wenzelm@68736:   performed by the original \<^verbatim>\<open>bibtex\<close> tool using style \<^verbatim>\<open>plain\<close>: different
wenzelm@68736:   Bib{\TeX} styles may produce slightly different results.
wenzelm@60255: 
wenzelm@62183:   \begin{figure}[!htb]
wenzelm@60255:   \begin{center}
wenzelm@60255:   \includegraphics[scale=0.333]{bibtex-mode}
wenzelm@60255:   \end{center}
wenzelm@68737:   \caption{Bib{\TeX} mode with context menu, SideKick tree view, and
wenzelm@68737:     semantic output from the \<^verbatim>\<open>bibtex\<close> tool}
wenzelm@60255:   \label{fig:bibtex-mode}
wenzelm@60255:   \end{figure}
wenzelm@68736: 
wenzelm@68736:   Regular document preview (\secref{sec:document-preview}) of \<^verbatim>\<open>.bib\<close> files
wenzelm@68736:   approximates the usual {\LaTeX} bibliography output in HTML (using style
wenzelm@68736:   \<^verbatim>\<open>unsort\<close>).
wenzelm@60255: \<close>
wenzelm@60255: 
wenzelm@60255: 
wenzelm@68736: section \<open>Document preview \label{sec:document-preview}\<close>
wenzelm@66683: 
wenzelm@66683: text \<open>
wenzelm@66683:   The action @{action_def isabelle.preview} opens an HTML preview of the
wenzelm@67246:   current document node in the default web browser. The content is derived
wenzelm@66683:   from the semantic markup produced by the prover, and thus depends on the
wenzelm@66683:   status of formal processing.
wenzelm@67262: 
wenzelm@67262:   Action @{action_def isabelle.draft} is similar to @{action
wenzelm@67262:   isabelle.preview}, but shows a plain-text document draft.
wenzelm@66683: \<close>
wenzelm@66683: 
wenzelm@66683: 
wenzelm@62253: chapter \<open>ML debugging within the Prover IDE\<close>
wenzelm@62154: 
wenzelm@62154: text \<open>
wenzelm@68224:   Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>https://www.polyml.org\<close>\<close> and thus
wenzelm@62253:   benefits from the source-level debugger of that implementation of Standard
wenzelm@62253:   ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> 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>\<open>Plugins /
wenzelm@62253:       Plugin Options / Isabelle / General\<close>. 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>\<open>Debugger\<close> 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>\<open>Toggle Breakpoint\<close> item. Alternatively, the
wenzelm@62253:     \<^emph>\<open>Break\<close> checkbox in the \<^emph>\<open>Debugger\<close> 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>\<open>gets lost\<close> 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 \<open>Context\<close> and \<open>ML\<close>, and pushing the
wenzelm@62253:   \<open>Eval\<close> 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>\<open>SML\<close> 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@69597:   \<^ML_type>\<open>theory\<close>, \<^ML_type>\<open>Proof.context\<close>, or \<^ML_type>\<open>Context.generic\<close>.
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>\<open>Continue\<close>, \<^emph>\<open>Step\<close>, \<^emph>\<open>Step over\<close>, \<^emph>\<open>Step out\<close>
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: \<close>
wenzelm@62154: 
wenzelm@62154: 
wenzelm@58618: chapter \<open>Miscellaneous tools\<close>
wenzelm@54358: 
wenzelm@58618: section \<open>Timing\<close>
wenzelm@54359: 
wenzelm@61574: text \<open>
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>\<open>Timing\<close> 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>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> 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>\<open>Plugin Options~/
wenzelm@62251:   Isabelle~/ General\<close>.
wenzelm@54360: 
wenzelm@61415:   \<^medskip>
wenzelm@61574:   The \<^emph>\<open>Monitor\<close> 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>\<open>isabelle.ML_Statistics\<close>
wenzelm@61503:   provides further access to statistics of Isabelle/ML.
wenzelm@61503: \<close>
wenzelm@54359: 
wenzelm@54359: 
wenzelm@58618: section \<open>Low-level output\<close>
wenzelm@54358: 
wenzelm@61574: text \<open>
wenzelm@62251:   Prover output is normally shown directly in the main text area or specific
wenzelm@62251:   panels like \<^emph>\<open>Output\<close> (\secref{sec:output}) or \<^emph>\<open>State\<close>
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>\<open>Protocol\<close> 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>\<open>Protocol\<close> panels for production work.
wenzelm@54358: 
wenzelm@61503:   \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close>
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@69597:   channels (corresponding to \<^ML>\<open>writeln\<close>, \<^ML>\<open>warning\<close>, \<^ML>\<open>Output.error_message\<close> in Isabelle/ML), which are displayed by regular means
wenzelm@60257:   within the document model (\secref{sec:output}). Unhandled Isabelle/ML
wenzelm@69597:   exceptions are printed by the system via \<^ML>\<open>Output.error_message\<close>.
wenzelm@54358: 
wenzelm@61477:   \<^item> \<^emph>\<open>Syslog\<close> 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@69597:   includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an explicit \<^ML>\<open>Output.system_message\<close> 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>\<open>Syslog\<close> 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: \<close>
wenzelm@54358: 
wenzelm@54358: 
wenzelm@58618: chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
wenzelm@53770: 
wenzelm@58618: text \<open>
wenzelm@61574:   \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with global
wenzelm@61574:   side-effects, like writing a physical file.
wenzelm@53770: 
wenzelm@61574:   \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable
wenzelm@61574:   continuous checking temporarily.
wenzelm@53770: 
wenzelm@61574:   \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
wenzelm@61574:   editor font size depend on platform details and national keyboards.
wenzelm@61574: 
wenzelm@61574:   \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/ Shortcuts\<close>.
wenzelm@54330: 
wenzelm@61503:   \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application
wenzelm@61574:   \<^emph>\<open>Preferences\<close> is in conflict with the jEdit default keyboard shortcut for
wenzelm@61574:   \<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref "quick-search"}).
wenzelm@53770: 
wenzelm@61574:   \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to
wenzelm@61574:   national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones.
wenzelm@53770: 
wenzelm@61522:   \<^item> \<^bold>\<open>Problem:\<close> 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>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option
wenzelm@61522:   \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.
wenzelm@61522: 
wenzelm@61574:   \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
wenzelm@61574:   the main text area.
wenzelm@54349: 
wenzelm@69343:   \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.
wenzelm@62265: 
wenzelm@61574:   \<^item> \<^bold>\<open>Problem:\<close> 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>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment variable
wenzelm@61574:   \<^verbatim>\<open>XMODIFIERS\<close> is reset by default within Isabelle settings.
wenzelm@61574: 
wenzelm@61574:   \<^item> \<^bold>\<open>Problem:\<close> 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>\<open>awesome\<close> or \<^verbatim>\<open>xmonad\<close>.
wenzelm@54329: 
wenzelm@61477:   \<^bold>\<open>Workaround:\<close> Use a regular re-parenting X11 window manager.
wenzelm@54329: 
wenzelm@61574:   \<^item> \<^bold>\<open>Problem:\<close> 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>\<open>Workaround:\<close> Use suitable version of Linux desktops.
wenzelm@60291: 
wenzelm@61477:   \<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref
wenzelm@61574:   "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on Windows,
wenzelm@61574:   but not on Mac OS X or various Linux/X11 window managers.
wenzelm@54349: 
wenzelm@61574:   \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window manager (notably
wenzelm@61574:   on Mac OS X).
wenzelm@64512: 
wenzelm@64512:   \<^item> \<^bold>\<open>Problem:\<close> 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@67092:   \<^bold>\<open>Workaround:\<close> Increase JVM heap parameters by editing platform-specific
wenzelm@67092:   files (for ``properties'' or ``options'') that are associated with the main
wenzelm@67092:   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: \<close>
wenzelm@53770: 
nipkow@67399: end




