| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/JEdit/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 126 kB |
|
Quelle JEdit.thy Sprache: Isabelle |
|||||||||
|
(*:maxLineLen=78:*)
theory JEdit imports Base begin chapter \<open>Introduction\<close> section \<open>Concepts and terminology\<close> text \<open> Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close> \<^cite>\<open>"Wenzel:2009" and "Wenzel:2013:ITP"\<close> with \<^emph>\<open>asynchronous use interaction\<close> \<^cite>\<open>"Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"\<close>, based on a document-oriented approach to \<^emph>\<open>continuous proof processing\<close> \<^cite>\<open>"Wenzel:2011:CICM "Wenzel:2012" and "Wenzel:2018:FIDE" and "Wenzel:2019:MKM"\<close>. Many concepts and system components are fit together in order to make this work. The main building blocks are as follows. \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle, see also \<^cite>\<open>"isabelle-implementation"\<close>. It is integrated into the logical context of Isabelle/Isar and allows to manipulate logical entities directly. Arbitrary add-on tools may be implemented for object-logics such as Isabelle/HOL. \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It extends the pure logical environment of Isabelle/ML towards the outer world of graphical user interfaces, text editors, IDE frameworks, web services, SSH servers, SQL databases etc. Both Scala and ML provide library modules to support formatted text with formal markup, and to encode/decode algebraic datatypes. Scala communicates with ML via asynchronous protocol commands; from the ML perspective this is wrapped up as synchronous function call (RPC). \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It is built around a concept of parallel and asynchronous document processing, which is supported natively by the parallel proof engine that is implemented in Isabelle/ML. The traditional prover command loop is given up; instead there is direct support for editing of source text, with rich formal markup for GUI rendering. \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedi implemented in Java\<^footnote>\<open>\<^url>\<open>https://openjdk.java.net\<close>\<close>. T extensible by plugins written in any language that works on the JVM. In the context of Isabelle this is usually Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>. \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the default user-interface for Isabelle. It targets both beginners and experts. Technically, Isabelle/jEdit consists of the original jEdit code base with minimal patches and a special plugin for Isabelle. This is integrated as a desktop application for the main operating system families: Linux, Windows, macOS. End-users of Isabelle download and run a standalone application that exposes jEdit as a text editor on the surface. Thus there is occasionally a tendency to apply the name ``jEdit'' to any of the Isabelle Prover IDE aspects, without proper differentiation. When discussing these PIDE building blocks in public forums, mailing lists, or even scientific publications, it is particularly important to distinguish Isabelle/ML versus Standard ML, Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit. \<close> section \<open>The Isabelle/jEdit Prover IDE\<close> text \<open> \begin{figure}[!htb] \begin{center} \includegraphics[width=\textwidth]{isabelle-jedit} \end{center} \caption{The Isabelle/jEdit Prover IDE} \label{fig:isabelle-jedit} \end{figure} Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for the jEdit text editor, together with patches on the underlying code base. The overall look-and-feel of jEdit is changed significantly, and the different name of Isabelle/jEdit is justified even from the surface. The main plugin is called ``Isabelle'' and has its own menu \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several actions and add-on panels (see also \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ Isabelle\<clos (see also \secref{sec:options}). The plugin options allow to specify a logic session name, but the same selector is also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After startup of the Isabelle plugin, the selected logic session image is provided automatically by the Isabelle build tool \<^cite>\<open>"isabelle-system"\<close>: if it is absent or outdated wrt.\ its sources, the build process updates it within the running text editor. Prover IDE functionality is only activated after successful termination of the build process. A failure may require changing some options and restart of the Isabelle plugin or application. Changing the logic session requires a restart of the whole application to take effect. \<^medskip> The main job of the Prover IDE is to manage sources and their changes, taking the logical structure as a formal document into account (see also \secref{sec:document-model}). The editor and the prover are connected asynchronously without locking. The prover is free to organize the checking of the formal text in parallel on multiple cores, and provides feedback via markup, which is rendered in the editor via colors, boxes, squiggly underlines, hyperlinks, popup windows, icons, clickable output etc. Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, Window or \<^verbatim>\<open>COMMAND\<close> (macOS) exposes formal content via tooltips and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in popups etc.) may be explored recursively, using the same techniques as in the editor source buffer. Thus the Prover IDE gives an impression of direct access to formal content of the prover within the editor, but in reality only certain aspects are exposed, according to the possibilities of the prover and its add-on tools. \<close> subsection \<open>Documentation\<close> text \<open> The \<^emph>\<open>Documentation\<close> panel of Isabelle/jEdit provides access to some exampl theory files and the standard Isabelle documentation. PDF files are opened by regular desktop operations of the underlying platform. The section ``Original jEdit Documentation'' contains the original \<^emph>\<open>User's Guide\<close> of this sophisticated text editor. The same is accessible via the \<^verbatim>\<open>Help\<close> me or \<^verbatim>\<open>F1\<close> keyboard shortcut, using the built-in HTML viewer of Java/Swing The latter also includes \<^emph>\<open>Frequently Asked Questions\<close> and documentation of individual plugins. Most of the information about jEdit is relevant for Isabelle/jEdit as well, but users need to keep in mind that defaults sometimes differ, and the official jEdit documentation does not know about the Isabelle plugin with its support for continuous checking of formal source text: jEdit is a plain text editor, but Isabelle/jEdit is a Prover IDE. \<close> subsection \<open>Plugins\<close> text \<open> The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by JVM modules (jars) that are provided by the central plugin repository, which is accessible via various mirror sites. Connecting to the plugin server-infrastructure of the jEdit project allows to update bundled plugins or to add further functionality. This needs to be done with the usual care for such an open bazaar of contributions, many of them unmaintained. Arbitrary combinations of add-on features are apt to cause problems. It is advisable to start with the default configuration of Isabelle/jEdit and develop a sense how it is meant to work, before loading other plugins. \<^medskip> The \<^emph>\<open>Isabelle\<close> plugin is responsible for the main Prover IDE functionality of Isabelle/jEdit: it manages the prover session in the background. A few additional plugins are bundled with Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\<open>Console\<close> with its \<^emph>\<open>Scala\<close> sub-plugin (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specifi parsers for document tree structure (\secref{sec:sidekick}). Other plugins (e.g.\ \<^emph>\<open>Console\<close>, \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>SideKick\<cl dependencies of bundled plugins, but have no particular use in Isabelle/jEdit. \<close> subsection \<open>Options \label{sec:options}\<close> text \<open> Both jEdit and Isabelle have distinctive management of persistent options. Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip th two within the central options dialog. Changes are stored in \<^path>\<open>$JEDIT_SETTINGS/properties\<close> and \<^path>\<open>$JEDIT_SETTINGS/keymaps Isabelle system options are managed by Isabelle/Scala and changes are stored in \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close>, independently of other jEdit properties. See also \<^cite>\<open>"isabelle-system"\<close>, especially the coverage of sessions and command-line tools like @{tool build} or @{tool options}. Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable i Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, ther are various options for rendering document content, which are configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin Opti Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options. Note that some of these options affect general parameters that are relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or @{system_option parallel_proofs} for the Isabelle build tool \<^cite>\<open>"isabelle-system"\<close>, but it is possible to use the settings variable @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds on the command-line, without affecting the Prover IDE. The jEdit action @{action_def isabelle.options} opens the options dialog for the Isabelle plugin; it can be mapped to editor GUI elements as usual. \<^medskip> Options are usually loaded on startup and saved on shutdown of Isabelle/jEdit. Editing the generated \<^path>\<open>$JEDIT_SETTINGS/properties\<close> or \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> manually while the application is running may cause lost updates! \<close> subsection \<open>Keymaps\<close> text \<open> Keyboard shortcuts are managed as a separate concept of \<^emph>\<open>keymap\<close> that is configurable via \<^emph>\<open>Global Options~/ Shortcuts\<close>. The \<^verbatim>\<open>impor derived from the initial environment of properties that was available at the first start of the editor; afterwards the keymap file takes precedence and is no longer affected by change of default properties. Users may modify their keymap later, but this can lead to conflicts with \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/properties/jEdit The action @{action_def "isabelle.keymap-merge"} helps to resolve pending Isabelle keymap changes wrt. the current jEdit keymap; non-conflicting changes are applied implicitly. This action is automatically invoked on Isabelle/jEdit startup. \<close> section \<open>Command-line invocation \label{sec:command-line}\<close> text \<open> Isabelle/jEdit is normally invoked as a single-instance desktop application, based on platform-specific executables for Linux, Windows, macOS. It is also possible to invoke the Prover IDE on the command-line, with some extra options and environment settings. The command-line usage of @{tool_def jedit} is as follows: @{verbatim [display] \<open>Usage: isabelle jedit [OPTIONS] [FILES ...] Options are: -A NAME ancestor session for option -R (default: parent) -D NAME=X set JVM system property -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS) -R NAME build image with requirements from other sessions -b build only -d DIR include session directory -f fresh build -i NAME include session in name-space of theories -j OPTION add jEdit runtime option (default $JEDIT_OPTIONS) -l NAME logic session name -m MODE add print mode for output -n no build of session image on startup -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p CMD command prefix for ML process (e.g. NUMA policy) -s system build mode for session image (system_heaps=true) -u user build mode for session image (system_heaps=false) Start jEdit with Isabelle plugin setup and open FILES (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>} The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used for proof processing. Additional session root directories may be included via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also \<^cite>\<open>" demand, but option \<^verbatim>\<open>-n\<close> bypasses the implicit build process for the selected session image. Options \<^verbatim>\<open>-s\<close> and \<^verbatim>\<open>-u\<close> ove option @{system_option system_heaps}: this determines where to store the session image of @{tool build}. The \<^verbatim>\<open>-R\<close> option builds an auxiliary logic image with all theories from other sessions that are not already present in its parent; it also opens the session \<^verbatim>\<open>ROOT\<close> entry in the editor to facilitate editing of the main session. The \<^verbatim>\<open>-A\<close> option specifies and alternative ancestor session fo option \<^verbatim>\<open>-R\<close>: this allows to restructure the hierarchy of session images the spot. Options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-l\<close> are mutually exclu The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of theories: multiple occurrences are possible. The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process Note that the system option @{system_option_ref jedit_print_mode} allows to do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of Isabelle/jEdit), without requiring command-line invocation. The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-lev jEdit, respectively. The defaults are provided by the Isabelle settings environment \<^cite>\<open>"isabelle-system"\<close>, but note that these only work for the command-line tool described here, and not the desktop application. The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed directly to the underlying \<^verbatim>\<open>java\<close> process. The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build m Isabelle/Scala. This is only relevant for building from sources, the official Isabelle release already includes a pre-built version of everything required for Isabelle/jEdit. The \<^verbatim>\<open>-o\<close> option is analogous to @{tool build} \<^cite>\<open>"isabelle-sy but it takes persistent preferences into account (\secref{sec:options}). When options are loaded, command-line options take precedence. When options are saved, command-line options are ignored (despite subsequent changes), but original preferences take precedence (including subsequent changes). \<^bigskip> It is also possible to connect to an already running Isabelle/jEdit process via @{tool_def jedit_client}: @{verbatim [display] \<open>Usage: isabelle jedit_client [OPTIONS] [FILES ...] Options are: -c only check presence of server -n only report server name -s NAME server name (default "Isabelle") Connect to already running Isabelle/jEdit instance and open FILES\<close>} The \<^verbatim>\<open>-c\<close> option merely checks the presence of the server, producing a process return-code. The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<clo different server name. The default server name is the official distribution name (e.g.\ \<^verbatim>\<open>Isabelle2025-1\<close>). Thus @{tool jedit_client} can connect Isabelle desktop application without further options. The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system option @{system_option_ref process_policy} for ML processes started by the Prover IDE, e.g. to control CPU affinity on multiprocessor systems. The JVM system property \<^verbatim>\<open>isabelle.jedit_server\<close> provides a different name, e.g.\ use \<^verbatim>\<open>isabelle jedit -Disabelle.jedit_server=\<close>\<open>name \<^verbatim>\<open>isabelle jedit_client -s\<close>~\<open>name\<close> to connect later on. \<close> section \<open>GUI rendering\<close> text \<open> Isabelle/jEdit is a classic Java/AWT/Swing application: its GUI rendering usually works well, but there are technical side-conditions on the Java window system and graphics engine. When researching problems and solutions on the Web, it often helps to include other well-known Swing applications, notably IntelliJ IDEA and Netbeans. \<close> subsection \<open>Portable and scalable look-and-feel\<close> text \<open> In the past, \<^emph>\<open>system look-and-feels\<close> tried hard to imitate native GUI elements on specific platforms (Windows, macOS/Aqua, Linux/GTK+), but many technical problems have accumulated in recent years (e.g.\ see \secref{sec:problems}). Already since 2021, we are de-facto back to \<^emph>\<open>portable look-and-feels\<close>, which also happen to be \<^emph>\<open>scalable\<close> on high-resolution displays: \<^item> \<^verbatim>\<open>FlatLaf Light\<close> (or \<^verbatim>\<open>FlatLaf macOS Light\<close> generally looks good on all platforms, and works smoothly with high-resolution displays. \<^item> \<^verbatim>\<open>FlatLaf Dark\<close> (or \<^verbatim>\<open>FlatLaf macOS Dark\<close>) i indicates that \<^emph>\<open>dark mode\<close> should be used for rendering in Isabelle/jEdit, via jEdit options with suffix ``\<^verbatim>\<open>.dark\<close>'' and Isabell options with suffix ``\<^verbatim>\<open>_dark\<close>''. The panels for \<^emph>\<open>Global Opt \<^emph>\<open>Plugin Options / Isabelle / Rendering\<close> operate on options according to the current Swing look-and-feel, e.g. on \<^verbatim>\<open>view.fgColor.dark\<close> in dark m vs. \<^verbatim>\<open>view.fgColor\<close> in non-dark mode. \<^item> \<^verbatim>\<open>Metal\<close> still works, although it is stylistically outdated. It m require manual adjustments of font sizes for high-resolution displays (see \secref{sec:fonts}). Most other look-and-feels are better ignored: they look rather bad, or cause genuine problems with GUI interaction. Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> updates the GU only partially: a full restart of Isabelle/jEdit is required to see the true effect. \<close> subsection \<open>Adjusting fonts \label{sec:fonts}\<close> text \<open> The preferred font collection for Isabelle/jEdit is \<^verbatim>\<open>Isabelle DejaVu\<close> is used by default for the main text area and various GUI elements. The default font sizes attempt to deliver a usable application for common display types, such as ``Full HD'' at $1920 \times 1080$ and ``Ultra HD'' at $3840 \times 2160$. \<^medskip> Isabelle/jEdit provides various options to adjust font sizes in particular GUI elements. Here is a summary of all relevant font properties: \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font, which is also used as reference point for various derived font sizes, e.g.\ the \<^emph>\<open>Output\<close> (\secref{sec:output}) and \<^emph>\<open>State\<close> (\secref{sec:state-output}) panels. \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter area left of the main text area, e.g.\ relevant for display of line numbers (disabled by default). \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and secondary font for the \<^emph>\<open>Metal\<close> look-and-feel. \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main text area font size for action @{action_ref "isabelle.reset-font-size"}, e.g.\ relevant for quick scaling like in common web browsers. \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window font, e.g.\ relevant for Isabelle/Scala command-line. \<close> chapter \<open>Augmented jEdit functionality\<close> section \<open>Dockable windows \label{sec:dockables}\<close> text \<open> In jEdit terminology, a \<^emph>\<open>view\<close> is an editor window with one or more \<^emph>\<ope areas\<close> that show the content of one or more \<^emph>\<open>buffers\<close>. A regular view may be surrounded by \<^emph>\<open>dockable windows\<close> that show additional information in arbitrary format, not just text; a \<^emph>\<open>plain view\<close> does not allow dockables. The \<^emph>\<open>dockable window manager\<close> of jEdit organizes these dockable windows, either as \<^emph>\<open>floating\<close> windows, or \<^emph>\<open>docked\<close> panels within on margins of the view. There may be any number of floating instances of some dockable window, but at most one docked instance; jEdit actions that address \<^emph>\<open>the\<close> dockable window of a particular kind refer to the unique docked instance. Dockables are used routinely in jEdit for important functionality like \<^emph>\<open>HyperSearch Results\<close> or the \<^emph>\<open>File System Browser\<close>. Plugi a central dockable to access their main functionality, which may be opened by the user on demand. The Isabelle/jEdit plugin takes this approach to the extreme: its plugin menu provides the entry-points to many panels that are managed as dockable windows. Some important panels are docked by default, e.g.\ \<^emph>\<open>Documentation\<close>, \<^emph>\<open>State\<close>, \<^emph>\<open>Theories\<c can change this arrangement easily and persistently. Compared to plain jEdit, dockable window management in Isabelle/jEdit is slightly augmented according to the the following principles: \<^item> Floating windows are dependent on the main window as \<^emph>\<open>dialog\<close> in the sense of Java/AWT/Swing. Dialog windows always stay on top of the view, which is particularly important in full-screen mode. The desktop environment of the underlying platform may impose further policies on such dependent dialogs, in contrast to fully independent windows, e.g.\ some window management functions may be missing. \<^item> Keyboard focus of the main view vs.\ a dockable window is carefully managed according to the intended semantics, as a panel mainly for output or input. For example, activating the \<^emph>\<open>Output\<close> (\secref{sec:output}) or Stat (\secref{sec:state-output}) panel via the dockable window manager returns keyboard focus to the main text area, but for \<^emph>\<open>Query\<close> (\secref{sec:query}) or \<^emph>\<open>Sledgehammer\<close> \secref{sec:sledgehammer} the focus is given to the main input field of that panel. \<^item> Panels that provide their own text area for output have an additional dockable menu item \<^emph>\<open>Detach\<close>. This produces an independent copy of the current output as a floating \<^emph>\<open>Info\<close> window, which displays that content independently of ongoing changes of the PIDE document-model. Note that Isabelle/jEdit popup windows (\secref{sec:tooltips-hyperlinks}) provide a similar \<^emph>\<open>Detach\<close> operation as an icon. \<close> section \<open>Isabelle symbols \label{sec:symbols}\<close> text \<open> Isabelle sources consist of \<^emph>\<open>symbols\<close> that extend plain ASCII to allow infinitely many mathematical symbols within the formal sources. This works without depending on particular encodings and varying Unicode standards.\<^footnote>\<open>Raw Unicode characters within formal sources compromise portability and reliability in the face of changing interpretation of special features of Unicode, such as Combining Characters or Bi-directional Text.\<close> For further explanations, see \<^cite>\<open>"Wenzel:2011:CICM"\<close>. For the prover back-end, formal text consists of ASCII characters that are grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or symbol ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is r physically via Unicode glyphs, to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\< This symbol interpretation is specified by the Isabelle system distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the user in \<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close>. The appendix of \<^cite>\<open>"isabelle-isar-ref"\<close> gives an overview of the standard interpretation of finitely many symbols from the infinite collection. Uninterpreted symbols are displayed literally, e.g.\ ``\<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol interpretation with informal ones (which might appear e.g.\ in comments) needs to be avoided. Raw Unicode characters within prover source files should be restricted to informal parts, e.g.\ to write text in non-latin alphabets in comments (excluding actual Greek). \<close> paragraph \<open>Encoding.\<close> text \<open>Technically, the Unicode interpretation of Isabelle symbols is an \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (\<^emph> JVM). It is provided by the Isabelle Base plugin and enabled by default for all source files in Isabelle/jEdit. Sometimes such defaults are reset accidentally, or malformed UTF-8 sequences in the text force jEdit to fall back on a different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim ``\<^verbatim>\<open>\<alpha>\<clos buffer instead of its Unicode rendering ``\<open>\<alpha>\<close>''. The jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps to resolve such problems (after repairing malformed parts of the text). If the loaded text already contains Unicode sequences that are in conflict with the Isabelle symbol encoding, the fallback-encoding UTF-8 is used and Isabelle symbols remain in literal \<^verbatim>\<open>\<symbol>\<close> form. The jEdit menu operation \<^emph>\<open>Utilities~/ Buffer Options~/ Character encoding\<close> allows to enforce \<^verbatim>\<open>UTF-8-Isabelle\<close>, but this will also change original Unicode t into Isabelle symbols when saving the file! \<close> paragraph \<open>Font.\<close> text \<open>Correct rendering via Unicode requires a font that contains glyphs for the corresponding codepoints. There are also various unusual symbols with particular purpose in Isabelle, e.g.\ control symbols and very long arrows. Isabelle/jEdit prefers its own font collection \<^verbatim>\<open>Isabelle DejaVu\<close>, wit families \<^verbatim>\<open>Serif\<close> (default for help texts), \<^verbatim>\<open>Sans\<clos elements), \<^verbatim>\<open>Mono Sans\<close> (default for text area). This ensures that all standard Isabelle symbols are shown on the screen (or printer) as expected. Note that a Java/AWT/Swing application can load additional fonts only if they are not installed on the operating system already! Outdated versions of Isabelle fonts that happen to be provided by the operating system prevent Isabelle/jEdit to use its bundled version. This could lead to missing glyphs (black rectangles), when the system version of a font is older than the application version. This problem can be avoided by refraining to ``install'' a copy of the Isabelle fonts in the first place, although it might be tempting to use the same font in other applications. HTML pages generated by Isabelle refer to the bundled Isabelle fonts as a server-side resource. Thus a web-browser can use that without requiring a locally installed copy. \<close> paragraph \<open>Input methods.\<close> text \<open>In principle, Isabelle/jEdit could delegate the problem to produce Isabelle symbols in their Unicode rendering to the underlying operating system and its \<^emph>\<open>input methods\<close>. Regular jEdit also provides various ways to work with \<^emph>\<open>abbreviations\<close> to produce certain non-ASCII characters. Since none of these standard input methods work satisfactorily for the mathematical characters required for Isabelle, various specific Isabelle/jEdit mechanisms are provided. This is a summary for practically relevant input methods for Isabelle symbols. \<^enum> The \<^emph>\<open>Symbols\<close> panel: some GUI buttons allow to insert certain symbols the text buffer. There are also tooltips to reveal the official Isabelle representation with some additional information about \<^emph>\<open>symbol abbreviations\<close> (see below). \<^enum> Copy/paste from decoded source files: text that is already rendered as Unicode can be re-used for other text. This also works between different applications, e.g.\ Isabelle/jEdit and some web browser or mail client, as long as the same Unicode interpretation of Isabelle symbols is used. \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same principles as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary Isabelle/jEdit windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or \<^verbatim>\<open>C+IN menu actions always refer to the primary text area! \<^enum> Completion provided by the Isabelle plugin (see \secref{sec:completion}). Isabelle symbols have a canonical name and optional abbreviations. This can be used with the text completion mechanism of Isabelle/jEdit, to replace a prefix of the actual symbol like \<^verbatim>\<open>\<lambda>\<close>, or its name preceded by backs \<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Un The following table is an extract of the information provided by the standard \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> file: \<^medskip> \begin{tabular}{lll} \<^bold>\<open>symbol\<close> & \<^bold>\<open>name with backslash\<close> & \<^bold>\<open>ab \<open>\<lambda>\<close> & \<^verbatim>\<open>\lambda\<close> & \<^verbatim>\<open>%\<close> \\ \<open>\<Rightarrow>\<close> & \<^verbatim>\<open>\Rightarrow\<close> & \<^verbatim>\<open>=> \<open>\<Longrightarrow>\<close> & \<^verbatim>\<open>\Longrightarrow\<close> & \<^verbat \<open>\<And>\<close> & \<^verbatim>\<open>\And\<close> & \<^verbatim>\<open>!!\<close> \\ \<open>\<equiv>\<close> & \<^verbatim>\<open>\equiv\<close> & \<^verbatim>\<open>==\<close> \\[ \<open>\<forall>\<close> & \<^verbatim>\<open>\forall\<close> & \<^verbatim>\<open>!\<close> \\ \<open>\<exists>\<close> & \<^verbatim>\<open>\exists\<close> & \<^verbatim>\<open>?\<close> \\ \<open>\<longrightarrow>\<close> & \<^verbatim>\<open>\longrightarrow\<close> & \<^verbat \<open>\<and>\<close> & \<^verbatim>\<open>\and\<close> & \<^verbatim>\<open>&\<close> \\ \<open>\<or>\<close> & \<^verbatim>\<open>\or\<close> & \<^verbatim>\<open>|\<close> \\ \<open>\<not>\<close> & \<^verbatim>\<open>\not\<close> & \<^verbatim>\<open>~\<close> \\ \<open>\<noteq>\<close> & \<^verbatim>\<open>\noteq\<close> & \<^verbatim>\<open>~=\<close> \\ \<open>\<in>\<close> & \<^verbatim>\<open>\in\<close> & \<^verbatim>\<open>:\<close> \\ \<open>\<notin>\<close> & \<^verbatim>\<open>\notin\<close> & \<^verbatim>\<open>~:\<close> \\ \end{tabular} \<^medskip> Note that the above abbreviations refer to the input method. The logical notation provides ASCII alternatives that often coincide, but sometimes deviate. This occasionally causes user confusion with old-fashioned Isabelle source that use ASCII replacement notation like \<^verbatim>\<open>!\<close> or \<^verbatim>\<open> the text. On the other hand, coincidence of symbol abbreviations with ASCII replacement syntax syntax helps to update old theory sources via explicit completion (see also \<^verbatim>\<open>C+b\<close> explained in \secref{sec:completion}). \<close> paragraph \<open>Control symbols.\<close> text \<open>There are some special control symbols to modify the display style of a single symbol (without nesting). Control symbols may be applied to a region of selected text, either using the \<^emph>\<open>Symbols\<close> panel or keyboard shortcuts or jEdit actions. These editor operations produce a separate control symbol for each symbol in the text, in order to make the whole text appear in a certain style. \<^medskip> \begin{tabular}{llll} \<^bold>\<open>style\<close> & \<^bold>\<open>symbol\<close> & \<^bold>\<open>shortcut\<close> && superscript & \<^verbatim>\<open>\<^sup>\<close> & \<^verbatim>\<open>C+e UP\<close> & @{ subscript & \<^verbatim>\<open>\<^sub>\<close> & \<^verbatim>\<open>C+e DOWN\<close> & @{ bold face & \<^verbatim>\<open>\<^bold>\<close> & \<^verbatim>\<open>C+e RIGHT\<close> & @ emphasized & \<^verbatim>\<open>\<^emph>\<close> & \<^verbatim>\<open>C+e LEFT\<close> & reset & & \<^verbatim>\<open>C+e BACK_SPACE\<close> & @{action_ref "isabelle.cont \end{tabular} \<^medskip> To produce a single control symbol, it is also possible to complete on \<^verbatim>\<open>\sup\<close>, \<^verbatim>\<open>\sub\<close>, \<^verbatim>\<open>\bold\<close>, \< The emphasized style only takes effect in document output (when used with a cartouche), but not in the editor. \<close> section \<open>Scala console \label{sec:scala-console}\<close> text \<open> The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters), e.g.\ \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and the cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and \<^verbatim>\<open> Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which is the default. This is the regular Scala toplevel loop running inside the same JVM process as Isabelle/jEdit itself. So the Scala command interpreter has access to the JVM name space and state of the running Prover IDE application. The default environment imports the full content of packages \<^verbatim>\<open>isabelle\<close> and \<^verbatim>\<open>isabelle.jedit\<close>. For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, and \<^v to the current editor view of jEdit. The Scala expression \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot of the current bu within the current editor view: it allows to retrieve document markup in a timeless~/ stateless manner, while the prover continues its processing. This helps to explore Isabelle/Scala functionality interactively. Some care is required to avoid interference with the internals of the running application. \<close> section \<open>Physical and logical files \label{sec:files}\<close> text \<open> File specifications in jEdit follow various formats and conventions according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by plugins. This allows to access remote files via the \<^verbatim>\<open>https:\<close> protocol prefix, for example. Isabelle/jEdit attempts to work with the file-system model of jEdit as far as possible. In particular, theory sources are passed from the editor to the prover, without indirection via the file-system. Thus files don't need to be saved: the editor buffer content is used directly. \<close> subsection \<open>Local files and environment variables \label{sec:local-files}\<close> text \<open> Local files (without URL notation) are particularly important. The file path notation is that of the Java Virtual Machine on the underlying platform. On Windows the preferred form uses backslashes, but happens to accept forward slashes like Unix/POSIX as well. Further differences arise due to Windows drive letters and network shares: thus relative paths (with forward slashes) are portable, but absolute paths are not. File paths in Java are distinct from Isabelle; the latter uses POSIX notation with forward slashes on \<^emph>\<open>all\<close> platforms. Isabelle/ML on Windows uses Unix-style path notation, with drive letters according to Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Environment variables from the Isabelle process may b freely, e.g.\ \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME There are special shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\< \<^dir>\<open>$ISABELLE_HOME\<close>. \<^medskip> Since jEdit happens to support environment variables within file specifications as well, it is natural to use similar notation within the editor, e.g.\ in the file-browser. This does not work in full generality, though, due to the bias of jEdit towards platform-specific notation and of Isabelle towards POSIX. Moreover, the Isabelle settings environment is not accessible when starting Isabelle/jEdit via the desktop application wrapper, in contrast to @{tool jedit} run from the command line (\secref{sec:command-line}). Isabelle/jEdit imitates important system settings within the Java process environment, in order to allow easy access to these important places from the editor: \<^verbatim>\<open>$ISABELLE_HOME\<close>, \<^verbatim>\<open>$ISABELLE_HOME_USER \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<ope these locations. \<^medskip> Path specifications in prover input or output usually include formal markup that turns it into a hyperlink (see also \secref{sec:tooltips-hyperlinks}). This allows to open the corresponding file in the text editor, independently of the path notation. If the path refers to a directory, it is opened in the jEdit file browser. Formally checked paths in prover input are subject to completion (\secref{sec:completion}): partial specifications are resolved via directory content and possible completions are offered in a popup. \<close> subsection \<open>PIDE resources via virtual file-systems\<close> text \<open> The jEdit file browser is docked by default. It provides immediate access to the local file-system, as well as important Isabelle resources via the \<^emph>\<open>Favorites\<close> menu. Environment variables like \<^verbatim>\<open>$ISABELLE_ discussed in \secref{sec:local-files}. Virtual file-systems are more special: the idea is to present structured information like a directory tree. The following URLs are offered in the \<^emph>\<open>Favorites\<close> menu, or by corresponding jEdit actions. \<^item> URL \<^verbatim>\<open>isabelle-export:\<close> or action @{action_def "isabelle-export-browser"} shows a toplevel directory with theory names: each may provide its own tree structure of session exports. Exports are like a logical file-system for the current prover session, maintained as Isabelle/Scala data structures and written to the session database eventually. The \<^verbatim>\<open>isabelle-export:\<close> URL exposes the current content according to a snapshot of the document model. The file browser is \<^emph>\<open>not\<close> updated continuously when the PIDE document changes: the reload operation needs to be used explicitly. A notable example for exports is the command @{command_ref export_code} \<^cite>\<open>"isabelle-isar-ref"\<close> (e.g.\ see \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Code_Lazy_Demo.thy\<close>). \<^item> URL \<^verbatim>\<open>isabelle-session:\<close> or action @{action_def "isabelle-session-browser"} show the structure of session chapters and sessions within them. What looks like a file-entry is actually a reference to the session definition in its corresponding \<^verbatim>\<open>ROOT\<close> file. The latter i subject to Prover IDE markup, so the session theories and other files may be browsed quickly by following hyperlinks in the text. \<close> section \<open>Indentation\<close> text \<open> Isabelle/jEdit augments the existing indentation facilities of jEdit to take the structure of theory and proof texts into account. There is also special support for unstructured proof scripts (\<^theory_text>\<open>apply\<close> etc.). \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar. Action @{action "indent-lines"} (shortcut \<^verbatim>\<open>C+i\<close>) indents the current according to command keywords and some command substructure: this approximation may need further manual tuning. Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the o and the new line according to command keywords only: leading to precise alignment of the main Isar language elements. This depends on option @{system_option_def "jedit_indent_newline"} (enabled by default). Regular input (via keyboard or completion) indents the current line whenever an new keyword is emerging at the start of the line. This depends on option @{system_option_def "jedit_indent_input"} (enabled by default). \<^descr>[Semantic indentation] adds additional white space to unstructured proof scripts via the number of subgoals. This requires information of ongoing document processing and may thus lag behind when the user is editing too quickly; see also option @{system_option_def "jedit_script_indent"} and @{system_option_def "jedit_script_indent_limit"}. The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options / Isabelle / General\<close>. A prerequisite for advanced indentation is \<^emph>\<open>Utilities / Buffer Options / Automatic indentation\<close>: it needs to be set to \<^verbatim>\<open>full\<cl (default). \<close> section \<open>SideKick parsers \label{sec:sidekick}\<close> text \<open> The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer structure in a tree view. Isabelle/jEdit provides SideKick parsers for its main mode for theory files, ML files, as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>RO \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}). \begin{figure}[!htb] \begin{center} \includegraphics[scale=0.333]{sidekick} \end{center} \caption{The Isabelle NEWS file with SideKick tree view} \label{fig:sidekick} \end{figure} The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides tree-view on the formal document structure, with section headings at the top and formal specification elements at the bottom. The alternative parser \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^the end\<close> structure. \<^medskip> Isabelle/ML files are structured according to semi-formal comments that are explained in \<^cite>\<open>"isabelle-implementation"\<close>. This outline is turned into a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also folding mode of the same name, for hierarchic text folds within ML files. \<^medskip> The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpre markup tree of the PIDE document model of the current buffer. This is occasionally useful for informative purposes, but the amount of displayed information might cause problems for large buffers. \<close> chapter \<open>Prover IDE functionality \label{sec:document-model}\<close> section \<open>Document model \label{sec:document-model}\<close> text \<open> The document model is central to the PIDE architecture: the editor and the prover have a common notion of structured source text with markup, which is produced by formal processing. The editor is responsible for edits of document source, as produced by the user. The prover is responsible for reports of document markup, as produced by its processing in the background. Isabelle/jEdit handles classic editor events of jEdit, in order to connect the physical world of the GUI (with its singleton state) to the mathematical world of multiple document versions (with timeless and stateless updates). \<close> subsection \<open>Editor buffers and document nodes \label{sec:buffer-node}\<close> text \<open> As a regular text editor, jEdit maintains a collection of \<^emph>\<open>buffers\<close> to store text files; each buffer may be associated with any number of visible \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> that is d from the file name extension. The following modes are treated specifically in Isabelle/jEdit: \<^medskip> \begin{tabular}{lll} \<^bold>\<open>mode\<close> & \<^bold>\<open>file name\<close> & \<^bold>\<open>content\<close> \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>*.thy\<close> & theory source \\ \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>*.ML\<close> & Isabelle/ML so \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>*.sml\<close> or \<^verbatim>\<open>*.sig\<cl \<^verbatim>\<open>isabelle-root\<close> & \<^verbatim>\<open>ROOT\<close> & session root \<^verbatim>\<open>isabelle-options\<close> & & Isabelle options \\ \<^verbatim>\<open>isabelle-news\<close> & & Isabelle NEWS \\ \end{tabular} \<^medskip> All jEdit buffers are automatically added to the PIDE document-model as \<^emph>\<open>document nodes\<close>. The overall document structure is defined by the theory nodes in two dimensions: \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory hea concrete syntax of the @{command_ref theory} command \<^cite>\<open>"isabelle-isar-ref"\<clo \<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>l commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file} \<^cite>\<open>"isabelle-isar-ref"\<close>. In any case, source files are managed by the PIDE infrastructure: the physical file-system only plays a subordinate role. The relevant version of source text is passed directly from the editor to the prover, using internal communication channels. \<close> subsection \<open>Theories \label{sec:theories}\<close> text \<open> The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overvie of the status of continuous checking of theory nodes within the document model. \begin{figure}[!htb] \begin{center} \includegraphics[scale=0.333]{theories} \end{center} \caption{Theories panel with an overview of the document-model, and jEdit text areas as editable views on some of the document nodes} \label{fig:theories} \end{figure} Theory imports are resolved automatically by the PIDE document model: all required files are loaded and stored internally, without the need to open corresponding jEdit buffers. Opening or closing editor buffers later on has no direct impact on the formal document content: it only affects visibility. In contrast, auxiliary files (e.g.\ from @{command ML_file} commands) are \<^emph>\<open>not\<close> resolved within the editor by default, but the prover process takes care of that. This may be changed by enabling the system option @{system_option jedit_auto_resolve}: it ensures that all files are uniformly provided by the editor. \<^medskip> The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective view on theory buffers via open text areas. The perspective is taken as a hint for document processing: the prover ensures that those parts of a theory where the user is looking are checked, while other parts that are presently not required are ignored. The perspective is changed by opening or closing text area windows, or scrolling within a window. The \<^emph>\<open>Theories\<close> panel provides some further options to influence the process of continuous checking: it may be switched off globally to restrict the prover to superficial processing of command syntax. It is also possible to indicate theory nodes as \<^emph>\<open>required\<close> for continuous checking: this means such nodes and all their imports are always processed independently of the visibility status (if continuous checking is enabled). Big theory libraries that are marked as required can have significant impact on performance! The \<^emph>\<open>Purge\<close> button restricts the document model to theories that are required for open editor buffers: inaccessible theories are removed and will be rechecked when opened or imported later. \<^medskip> Formal markup of checked theory content is turned into GUI rendering, based on a standard repertoire known from mainstream IDEs for programming languages: colors, icons, highlighting, squiggly underlines, tooltips, hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional syntax-highlighting via static keywords and tokenization within the editor; this buffer syntax is determined from theory imports. In contrast, the painting of inner syntax (term language etc.)\ uses semantic information that is reported dynamically from the logical context. Thus the prover can provide additional markup to help the user to understand the meaning of formal text, and to produce more text with some add-on tools (e.g.\ information messages with \<^emph>\<open>sendback\<close> markup by automated provers or disprovers in the background). \<close> subsection \<open>Auxiliary files \label{sec:aux-files}\<close> text \<open> Special load commands like @{command_ref ML_file} and @{command_ref SML_file} \<^cite>\<open>"isabelle-isar-ref"\<close> refer to auxiliary files within some theory. Conceptually, the file argument of the command extends the theory source by the content of the file, but its editor buffer may be loaded~/ changed~/ saved separately. The PIDE document model propagates changes of auxiliary file content to the corresponding load command in the theory, to update and process it accordingly: changes of auxiliary file content are treated as changes of the corresponding load command. \<^medskip> As a concession to the massive amount of ML files in Isabelle/HOL itself, the content of auxiliary files is only added to the PIDE document-model on demand, the first time when opened explicitly in the editor. There are further tricks to manage markup of ML files, such that Isabelle/HOL may be edited conveniently in the Prover IDE on small machines with only 8\,GB of main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may st at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example. It is also possible to explore the Isabelle/Pure bootstrap process (a virtual copy) by opening \<^file>\<open>$ISABELLE_HOME/src/Pure/ROOT.ML\<close> like a theory in the Prover IDE. Initially, before an auxiliary file is opened in the editor, the prover reads its content from the physical file-system. After the file is opened for the first time in the editor, e.g.\ by following the hyperlink (\secref{sec:tooltips-hyperlinks}) for the argument of its @{command ML_file} command, the content is taken from the jEdit buffer. The change of responsibility from prover to editor counts as an update of the document content, so subsequent theory sources need to be re-checked. When the buffer is closed, the responsibility remains to the editor: the file may be opened again without causing another document update. A file that is opened in the editor, but its theory with the load command is not, is presently inactive in the document model. A file that is loaded via multiple load commands is associated to an arbitrary one: this situation is morally unsupported and might lead to confusion. \<^medskip> Output that refers to an auxiliary file is combined with that of the corresponding load command, and shown whenever the file or the command are active (see also \secref{sec:output}). Warnings, errors, and other useful markup is attached directly to the positions in the auxiliary file buffer, in the manner of standard IDEs. By using the load command @{command SML_file} as explained in \<^file>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, Isabelle/jEdit may be us fully-featured IDE for Standard ML, independently of theory or proof development: the required theory merely serves as some kind of project file for a collection of SML source modules. \<close> section \<open>Output \label{sec:output}\<close> text \<open> Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. Both ar attached to the corresponding positions in the original source text, and visualized in the text area, e.g.\ as text colours for free and bound variables, or as squiggly underlines for warnings, errors etc.\ (see also \figref{fig:output}). In the latter case, the corresponding messages are shown by hovering with the mouse over the highlighted text --- although in many situations the user should already get some clue by looking at the position of the text highlighting, without seeing the message body itself. \begin{figure}[!htb] \begin{center} \includegraphics[scale=0.333]{output} \end{center} \caption{Multiple views on prover output: gutter with icon, text area with popup, text overview column, \<^emph>\<open>Theories\<close> panel, \<^emph>\<open>Output\<close> p \label{fig:output} \end{figure} The ``gutter'' on the left-hand-side of the text area uses icons to provide a summary of the messages within the adjacent text line. Message priorities are used to prefer errors over warnings, warnings over information messages; other output is ignored. The ``text overview column'' on the right-hand-side of the text area uses similar information to paint small rectangles for the overall status of the whole text buffer. The graphics is scaled to fit the logical buffer length into the given window height. Mouse clicks on the overview area move the cursor approximately to the corresponding text line in the buffer. The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but withou direct correspondence to text positions. The coloured rectangles represent the amount of messages of a certain kind (warnings, errors, etc.) and the execution status of commands. The border of each rectangle indicates the overall status of processing: a thick border means it is \<^emph>\<open>finished\<close> or \<^emph>\<open>failed\<close> (with color for errors). A double-click on one of the theory entries with their status overview opens the corresponding text buffer, without moving the cursor to a specific point. \<^medskip> The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given command, within a separate window. The cursor position in the presently active text area determines the prover command whose cumulative message output is appended and shown in that window (in canonical order according to the internal execution of the command). There are also control elements to modify the update policy of the output wrt.\ continued editor movements: \<^emph>\<open>Auto update\<close> and \<^emph>\<open>Update\<close>. This is particularly useful fo instances of the \<^emph>\<open>Output\<close> panel to look at different situations. Alternatively, the panel can be turned into a passive \<^emph>\<open>Info\<close> window via the \<^emph>\<open>Detach\<close> menu item. Proof state is handled separately (\secref{sec:state-output}), but it is also possible to tick the corresponding checkbox to append it to regular output (\figref{fig:output-including-state}). This is a globally persistent option: it affects all open panels and future editor sessions. \begin{figure}[!htb] \begin{center} \includegraphics[scale=0.333]{output-including-state} \end{center} \caption{Proof state display within the regular output panel} \label{fig:output-including-state} \end{figure} \<^medskip> \<^emph>\<open>Explicit highlighting\<close> of output works via the \<^emph>\<open>Search\<close> f the text against a given regular expression, in the notation of Java.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/21/docs/api Results are also presented as a tree view, by sub-dividing the output panel on demand. \<^emph>\<open>Implicit highlighting\<close> of output is based on formal markup by the prover. If the \<^emph>\<open>Auto hovering\<close> option is enabled (default), then mouse hovering alone is sufficient to see highlighted ranges stemming from nested syntax structure (see also \secref{sec:tooltips-hyperlinks}); together with the ALT keyboard modifier this produces a selection that is ready for copy-paste. Without \<^emph>\<open>Auto hovering\<close>, an additional keyboard modifier \<^verbatim>\<open> Windows) or \<^verbatim>\<open>COMMAND\<close> (macOS) is required, as for input text. \<^medskip> Following the IDE principle, regular messages are attached to the original source in the proper place and may be inspected on demand via popups. This excludes messages that are somehow internal to the machinery of proof checking, notably \<^emph>\<open>proof state\<close> and \<^emph>\<open>tracing\<close>. In any case, the same display technology is used for small popups and big output windows. The formal text contains markup that may be explored recursively via further popups and hyperlinks (see \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}). \<^medskip> Alternatively, the subsequent actions (with keyboard shortcuts) allow to show tooltip messages or navigate error positions: \<^medskip> \begin{tabular}[t]{l} @{action_ref "isabelle.tooltip"} (\<^verbatim>\<open>CS+b\<close>) \\ @{action_ref "isabelle.message"} (\<^verbatim>\<open>CS+m\<close>) \\ \end{tabular}\quad \begin{tabular}[t]{l} @{action_ref "isabelle.first-error"} (\<^verbatim>\<open>CS+a\<close>) \\ @{action_ref "isabelle.last-error"} (\<^verbatim>\<open>CS+z\<close>) \\ @{action_ref "isabelle.next-error"} (\<^verbatim>\<open>CS+n\<close>) \\ @{action_ref "isabelle.prev-error"} (\<^verbatim>\<open>CS+p\<close>) \\ \end{tabular} \<^medskip> \<close> section \<open>Proof state \label{sec:state-output}\<close> text \<open> The main purpose of the Prover IDE is to help the user editing proof documents, with ongoing formal checking by the prover in the background. This can be done to some extent in the main text area alone, especially for well-structured Isar proofs. Nonetheless, internal proof state needs to be inspected in many situations of exploration and ``debugging''. The \<^emph>\<open>State\<close> panel shows exclusively such proof state messages without further distraction, while all other messages are displayed in \<^emph>\<open>Output\<close> (\secref{sec:output}). \Figref{fig:output-and-state} shows a typical GUI layout where both panels are open, while the \<^emph>\<open>Proof state\<close> option is disabled within \<^emph>\<open>Outp \begin{figure}[!htb] \begin{center} \includegraphics[scale=0.333]{output-and-state} \end{center} \caption{Separate proof state display (right) and other output (bottom).} \label{fig:output-and-state} \end{figure} Another typical arrangement has more than one \<^emph>\<open>State\<close> panel open (as floating windows), with \<^emph>\<open>Auto update\<close> disabled to look at an old situation while the proof text in the vicinity is changed. The \<^emph>\<open>Update\<close> button triggers an explicit one-shot update; this operation is also available via the action @{action "isabelle.update-state"} (keyboard shortcut \<^verbatim>\<open>S+ENTER On small screens, it is occasionally useful to have all messages concatenated in the regular \<^emph>\<open>Output\<close> panel, e.g.\ see \figref{fig:output-including-state}. \<^medskip> The mechanics of \<^emph>\<open>Output\<close> versus \<^emph>\<open>State\<close> are slightly diff \<^item> \<^emph>\<open>Output\<close> shows information that is continuously produced and alread present when the GUI wants to show it. This is implicitly controlled by the visible perspective on the text. \<^item> \<^emph>\<open>State\<close> initiates a real-time query on demand, with a full round trip including a fresh print operation on the prover side. This is controlled explicitly when the cursor is moved to the next command (\<^emph>\<open>Auto update\<close>) or the \<^emph>\<open>Update\<close> operation is triggered. This can make a difference in GUI responsibility and resource usage within the prover process. Applications with very big proof states that are only inspected in isolation work better with the \<^emph>\<open>State\<close> panel. \<close> section \<open>Query \label{sec:query}\<close> text \<open> The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information from the prover, as a replacement of old-style diagnostic commands like --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28