1.1 --- a/src/Doc/JEdit/JEdit.thy Sat Oct 12 00:10:07 2013 +0200
1.2 +++ b/src/Doc/JEdit/JEdit.thy Sat Oct 12 14:37:45 2013 +0200
1.3 @@ -15,42 +15,42 @@
1.4 document-oriented approach to \emph{continuous proof processing}
1.5 \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system
1.6 components are fit together in order to make this work. The main
1.7 - building blocks are as follows:
1.8 + building blocks are as follows.
1.9
1.10 \begin{description}
1.11
1.12 - \item [PIDE] is a general framework for Prover IDEs based on the
1.13 - Isabelle/Scala. It is built around a concept of asynchronous
1.14 - document processing, which is supported natively by the parallel
1.15 - proof engine that is implemented in Isabelle/ML. The prover
1.16 - discontinues the traditional TTY-based command loop in favor of
1.17 - direct editing of formal source text.
1.18 + \item [PIDE] is a general framework for Prover IDEs based on
1.19 + Isabelle/Scala. It is built around a concept of parallel and
1.20 + asynchronous document processing, which is supported natively by the
1.21 + parallel proof engine that is implemented in Isabelle/ML. The prover
1.22 + discontinues the traditional TTY-based command loop, and supports
1.23 + direct editing of formal source text with rich formal markup for GUI
1.24 + rendering.
1.25
1.26 \item [Isabelle/ML] is the implementation and extension language of
1.27 Isabelle, see also \cite{isabelle-implementation}. It is integrated
1.28 - into the formal logical context and allows to manipulate logical
1.29 - entities directly. Arbitrary add-on tools may be implemented for
1.30 - object-logics such as Isabelle/HOL.
1.31 + into the logical context of Isabelle/Isar and allows to manipulate
1.32 + logical entities directly. Arbitrary add-on tools may be implemented
1.33 + for object-logics such as Isabelle/HOL.
1.34
1.35 \item [Isabelle/Scala] is the system programming language of
1.36 Isabelle. It extends the pure logical environment of Isabelle/ML
1.37 towards the ``real world'' of graphical user interfaces, text
1.38 editors, IDE frameworks, web services etc. Special infrastructure
1.39 - allows to transfer algebraic datatypes and formatted text easily
1.40 - between ML and Scala, using asynchronous protocol commands.
1.41 + allows to transfer algebraic datatypes values and formatted text
1.42 + easily between ML and Scala, using asynchronous protocol commands.
1.43
1.44 - \item [jEdit] is a sophisticated text
1.45 - editor\footnote{\url{http://www.jedit.org}} implemented in Java. It
1.46 - is easily extensible by plugins written in languages that work on
1.47 - the JVM, e.g.\ Scala\footnote{\url{http://www.scala-lang.org/}}.
1.48 + \item [jEdit] is a sophisticated text editor implemented in
1.49 + Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
1.50 + by plugins written in languages that work on the JVM, e.g.\
1.51 + Scala\footnote{\url{http://www.scala-lang.org/}}.
1.52
1.53 \item [Isabelle/jEdit] is the main example application of the PIDE
1.54 - framework and the default user-interface for Isabelle. It is
1.55 - targeted at beginners and experts alike. Technically, Isabelle/jEdit
1.56 - combines a slightly modified version of the official jEdit code base
1.57 - with a special plugin for Isabelle, which is then integrated as
1.58 - standalone application for the main operating system platforms:
1.59 - Linux, Windows, Mac OS X.
1.60 + framework and the default user-interface for Isabelle. It targets
1.61 + both beginners and experts. Technically, Isabelle/jEdit combines a
1.62 + slightly modified version of the official jEdit code base with a
1.63 + special plugin for Isabelle, integrated as standalone application
1.64 + for the main operating system platforms: Linux, Windows, Mac OS X.
1.65
1.66 \end{description}
1.67
1.68 @@ -89,12 +89,13 @@
1.69 CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
1.70 additional formal content via tooltips and/or hyperlinks.
1.71
1.72 - \item Dockable windows (e.g.\ \emph{Output}, \emph{Symbols}) are
1.73 - managed separately by jEdit, which also allows multiple instances.
1.74 -
1.75 \item Formal output (in popups etc.) may be explored recursively,
1.76 using the same techniques as in the editor source buffer.
1.77
1.78 + \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
1.79 + organized by the Dockable Window Manager of jEdit, which also allows
1.80 + multiple floating instances of each window class.
1.81 +
1.82 \item The prover process and source files are managed on the editor
1.83 side. The prover operates on timeless and stateless document
1.84 content via Isabelle/Scala.
1.85 @@ -119,10 +120,10 @@
1.86 \emph{User's Guide} and \emph{Frequently Asked Questions} for this
1.87 sophisticated text editor.
1.88
1.89 - Most of the information is relevant for Isabelle/jEdit as well, but
1.90 - one needs to keep in mind that defaults sometimes differ, and the
1.91 - official jEdit documentation does not know about the Isabelle plugin
1.92 - with its bias towards theory editing.
1.93 + Most of this information about jEdit is relevant for Isabelle/jEdit
1.94 + as well, but one needs to keep in mind that defaults sometimes
1.95 + differ, and the official jEdit documentation does not know about the
1.96 + Isabelle plugin with its special support for theory editing.
1.97 *}
1.98
1.99
1.100 @@ -131,12 +132,12 @@
1.101 text {* The \emph{Plugin Manager} of jEdit allows to augment editor
1.102 functionality by JVM modules (jars) that are provided by the central
1.103 plugin repository, or one of various mirror sites. The main
1.104 - \emph{Isabelle} plugin that is bundled with Isabelle/jEdit needs to
1.105 - remain active at all times! A few additional plugins are bundled
1.106 + \emph{Isabelle} plugin is an integral part of Isabelle/jEdit needs
1.107 + to remain active at all times! A few additional plugins are bundled
1.108 with Isabelle/jEdit for convenience or out of necessity, notably
1.109 \emph{Console} with its Isabelle/Scala sub-plugin and
1.110 - \emph{SideKick} with some Isabelle-specific parsers for tree
1.111 - structure.
1.112 + \emph{SideKick} with some Isabelle-specific parsers for document
1.113 + tree structure.
1.114
1.115 Connecting to the plugin server infrastructure of the jEdit project
1.116 allows to update bundled plugins or to add further
1.117 @@ -152,32 +153,33 @@
1.118
1.119 subsection {* Options *}
1.120
1.121 -text {* jEdit and Isabelle have separate management of persistent
1.122 - options. Regular jEdit options are accessible via the dialogs for
1.123 - \emph{Global Options} and \emph{Plugin Options}. This results in an
1.124 - environment of name-value properties that is stored within the
1.125 +text {* Both jEdit and Isabelle have distinctive management of
1.126 + persistent options. Regular jEdit options are accessible via the
1.127 + dialogs for \emph{Global Options} and \emph{Plugin Options}. This
1.128 + results in an environment of properties that is stored within the
1.129 \emph{settings directory} of jEdit; see also the menu
1.130 \emph{Utilities / Settings Directory}.
1.131
1.132 - In contrast, Isabelle system options are managed by Isabelle/Scala;
1.133 - see also \cite{isabelle-sys}, especially the coverage of Isabelle
1.134 - sessions and build. Options that are declared as \textbf{public}
1.135 - are exposed to the \emph{Plugin Options} dialog of jEdit in its
1.136 - section \emph{Isabelle / General}. This provides a view on Isabelle
1.137 - options and persistent preferences in @{verbatim
1.138 - "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit
1.139 - properties in its settings directory.
1.140 -
1.141 - Isabelle options are loaded once on startup and saved on shutdown.
1.142 - Editing the machine-generated @{verbatim "etc/preferences"} manually
1.143 - while the application is running is likely to cause a lost-update!
1.144 + Isabelle system options are managed by Isabelle/Scala; see also
1.145 + \cite{isabelle-sys}, especially the coverage of sessions and
1.146 + command-line tools like @{tool build} or @{tool options}. Isabelle
1.147 + options that are declared as \textbf{public} are exposed to the
1.148 + jEdit \emph{Plugin Options} dialog, in its section \emph{Isabelle /
1.149 + General}. This provides a view on Isabelle options and persistent
1.150 + preferences in @{verbatim "$ISABELLE_HOME_USER/etc/preferences"},
1.151 + independently of the jEdit properties in its settings directory.
1.152
1.153 Some Isabelle options that are accessible in the Isabelle/jEdit
1.154 Plugin Options dialog affect general parameters that are relevant
1.155 outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
1.156 @{system_option parallel_proofs} for the Isabelle build tool
1.157 \cite{isabelle-sys}.
1.158 -*}
1.159 +
1.160 + \medskip Options are loaded once on startup and saved on shutdown of
1.161 + Isabelle/jEdit. Editing the machine-generated files @{verbatim
1.162 + "$ISABELLE_HOME_USER/jedit/properties"} or @{verbatim
1.163 + "$ISABELLE_HOME_USER/etc/preferences"} manually while the
1.164 + application is running is likely to cause a lost-update! *}
1.165
1.166
1.167 subsection {* Keymaps *}
1.168 @@ -191,30 +193,31 @@
1.169 This is relevant for Isabelle/jEdit due to various fine-tuning of
1.170 default properties, and additional keyboard shortcuts for Isabelle
1.171 specific functionality. Users may change their keymap later on, but
1.172 - may need to copy important key bindings manually.
1.173 + may need to copy Isabelle-specific key bindings manually.
1.174 *}
1.175
1.176
1.177 subsection {* Look-and-feel *}
1.178
1.179 text {* jEdit is a Java/Swing application with some ambition to
1.180 - support ``native'' platform look-and-feel, within the limits of what
1.181 - Oracle as Java provider and major operating system vendors and
1.182 - distributors allow.
1.183 + support ``native'' look-and-feel on all platforms, within the limits
1.184 + of what Oracle as Java provider and major operating system vendors
1.185 + and distributors allow (see also \secref{sec:problems}).
1.186
1.187 - Isabelle/jEdit uses platform-specific look-and-feel as follows:
1.188 + Isabelle/jEdit enables platform-specific look-and-feel by default as
1.189 + follows.
1.190
1.191 \begin{description}
1.192
1.193 \item[Linux] The platform-independent \emph{Nimbus} is used by
1.194 default, but the classic \emph{Metal} also works. \emph{GTK+} works
1.195 under the side-condition that the overall GTK theme is selected in a
1.196 - Java/Swing friendly way: the success rate is @{text "\<approx>"} 50\%.
1.197 + Java/Swing friendly way.
1.198
1.199 \item[Windows] Regular \emph{Windows} is used by default, but
1.200 platform-independent \emph{Nimbus} and \emph{Metal} also work.
1.201
1.202 - \item[Mac OS X] standard \emph{Apple Aqua} is used by default.
1.203 + \item[Mac OS X] Standard \emph{Apple Aqua} is used by default.
1.204 Moreover the bundled \emph{MacOSX} plugin provides various functions
1.205 that are expected from applications on that particular platform:
1.206 quit from menu or dock, preferences menu, drag-and-drop of text
1.207 @@ -224,11 +227,9 @@
1.208 \end{description}
1.209
1.210 Users may experiment with different look-and-feels, but need to keep
1.211 - in mind that this extra dimension of GUI functionality is unlikely
1.212 - to work in arbitrary combinations. The \emph{GTK+} look-and-feel is
1.213 + in mind that this extra variance of GUI functionality is unlikely to
1.214 + work in arbitrary combinations. The \emph{GTK+} look-and-feel is
1.215 particularly critical due to its additional dimension of ``themes''.
1.216 - It is also important to ensure that the fonts of standard GUI
1.217 - components use anti-aliasing as usual.
1.218
1.219 After changing the look-and-feel in \emph{Global Options /
1.220 Appearance}, it is advisable to restart Isabelle/jEdit in order to
1.221 @@ -242,48 +243,35 @@
1.222
1.223 text {* jEdit maintains a collection of open \emph{text buffers} to
1.224 store source files. Each buffer may be associated with any number
1.225 - of \emph{text areas} as visible GUI representation of the content.
1.226 + of visible \emph{text areas}. Buffers are subject to an
1.227 + \emph{editor mode} that is determined from the file type. Files
1.228 + with extension \texttt{.thy} are assigned to the mode
1.229 + \emph{isabelle} and treated specifically.
1.230
1.231 - Buffers are subject to a \emph{mode} that is determined from the
1.232 - file type. Files with extension \texttt{.thy} are assigned to the
1.233 - mode \emph{isabelle} and treated specifically as follows.
1.234 + \medskip Isabelle theory files are automatically added to the formal
1.235 + document model of Isabelle/Scala, which maintains a family of
1.236 + versions of all sources for the prover. The \emph{Theories} panel
1.237 + provides an overview of the status of continuous checking of theory
1.238 + sources. Unlike batch sessions \cite{isabelle-sys}, theory nodes
1.239 + are identified by full path names; this allows to work with multiple
1.240 + (disjoint) Isabelle sessions simultaneously within the same editor
1.241 + session.
1.242
1.243 - \begin{itemize}
1.244 + Certain events to open or update buffers with theory files cause
1.245 + Isabelle/jEdit to resolve dependencies of \emph{theory imports}.
1.246 + The system requests to load further files into jEdit editor buffers,
1.247 + to be added to the theory document model for further checking. It
1.248 + is also possible to resolve dependencies automatically, depending on
1.249 + the option @{system_option jedit_auto_load}.
1.250
1.251 - \item Theory files are implicitly added to the formal document model
1.252 - of Isabelle/jEdit, which maintains a family of versions of all
1.253 - sources for the prover in the background. The \emph{Theories} panel
1.254 - provides an overview of the status of continuous checking of theory
1.255 - sources. Unlike batch sessions \cite{isabelle-sys}, full theory
1.256 - file names are used to identify theory nodes; this allows to
1.257 - experiment with multiple (disjoint) Isabelle sessions
1.258 - simultaneously.
1.259 + \medskip The open text area views on theory buffers define the
1.260 + visible \emph{perspective} of Isabelle/jEdit. This is taken as a
1.261 + hint for document processing: the prover ensures that those parts of
1.262 + a theory where the user is looking are checked, while other parts
1.263 + that are presently not required are ignored.
1.264
1.265 - \item Certain events to open or update buffers containing theory
1.266 - files cause Isabelle/jEdit to resolve dependencies of \emph{theory
1.267 - imports}. The system will request to load further files into jEdit
1.268 - editor buffers, which will eventually be added to the theory
1.269 - document model for further checking. It is also possible to resolve
1.270 - dependencies automatically, depending on the option @{system_option
1.271 - jedit_auto_load}.
1.272 -
1.273 - \item Physical rendering of jEdit buffer content within the visible
1.274 - text areas is augmented by information from the formal document
1.275 - model. Thus the prover can provide additional markup to help the
1.276 - user understanding the meaning of the text, and to produce more text
1.277 - with some add-on tools (e.g.\ information messages produced by
1.278 - automated provers or disprovers in the background).
1.279 -
1.280 - \end{itemize}
1.281 -
1.282 - The text area views on theory buffers define the visible part of the
1.283 - \emph{perspective} of Isabelle/jEdit. This is taken as a hint for
1.284 - document processing: the prover will ensure that those parts of a
1.285 - theory where the user is looking are checked, while invisible parts
1.286 - that are presently not required are left alone.
1.287 -
1.288 - The perspective can may changed by opening or closing text areas, or
1.289 - scrolling the corresponding windows. It is also possible to
1.290 + The perspective can be changed by opening or closing text areas
1.291 + windows, or scrolling within some window. It is also possible to
1.292 indicate theory nodes as \emph{required} for continuous checking in
1.293 the \emph{Theories} panel. This means such nodes and all their
1.294 imports are always processed, independently of the visibility
1.295 @@ -292,14 +280,18 @@
1.296 \medskip Formal markup of checked theory content is turned into GUI
1.297 rendering, based on a standard repertoire known from IDEs for
1.298 programming languages: colors, icons, highlighting, squiggly
1.299 - underline, tooltips, hyperlinks etc. There is some traditional
1.300 - syntax-highlighting for the outer syntax of Isabelle/Isar, based on
1.301 - static keyword tables. The coloring of inner syntax (term language
1.302 - etc.) is based on dynamic information from the logical context of
1.303 - the prover.
1.304 + underline, tooltips, hyperlinks etc. For outer syntax of
1.305 + Isabelle/Isar there is some traditional syntax-highlighting, based
1.306 + on static keyword tables and tokenization within the editor. In
1.307 + contrast, the painting of inner syntax (term language etc.) is
1.308 + based on semantic information that is reported dynamically from the
1.309 + logical context. Thus the prover can provide additional markup to
1.310 + help the user understanding the meaning of the text, and to produce
1.311 + more text with some add-on tools (e.g.\ information messages by
1.312 + automated provers or disprovers running in the background).
1.313
1.314 Such formally annotated text can be explored further by using the
1.315 - @{verbatim CONTROL} modifier key on Linux or Windows, and @{verbatim
1.316 + @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim
1.317 COMMAND} on Mac OS X. Hovering with the mouse while the modifier is
1.318 pressed reveals \emph{tooltips} (grey box within the text with a
1.319 yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within
1.320 @@ -315,48 +307,24 @@
1.321
1.322 text {* Isabelle sources consist of \emph{symbols} that extend plain
1.323 ASCII and UTF-8 (for informal text) to allow infinitely many
1.324 - mathematical symbols, without depending on particular encodings.
1.325 + mathematical symbols within the formal sources. This works without
1.326 + depending on particular encodings or varying Unicode standards
1.327 + \cite{Wenzel:2011:CICM}.
1.328
1.329 For the prover back-end, formal text consists of ASCII characters
1.330 that are grouped according to some simple rules, e.g.\ as plain
1.331 ``@{verbatim a}'' or symbolic ``@{verbatim "\<alpha>"}''.
1.332
1.333 - For the editor front-end, some well-known symbols are rendered as
1.334 + For the editor front-end, a certain subset of symbols is rendered as
1.335 Unicode glyphs, in order to show ``@{verbatim "\<alpha>"}'' as actual
1.336 ``@{text "\<alpha>"}''. This symbol interpretation is specified by the
1.337 Isabelle system distribution (in @{file
1.338 - "$ISABELLE_HOME/etc/symbols"}) or the user (in @{verbatim
1.339 + "$ISABELLE_HOME/etc/symbols"}) or by the user (in @{verbatim
1.340 "$ISABELLE_HOME_USER/etc/symbols"}).
1.341
1.342 - \medskip The appendix of \cite{isabelle-isar-ref} gives an overview
1.343 - of the standard interpretation of finitely many symbols from the
1.344 - infinite collection. Uninterpreted symbols are shown literally.
1.345 - For example:
1.346 -
1.347 - \medskip
1.348 - \begin{tabular}{l}
1.349 - @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} \\
1.350 - @{text "\<forall>"}, @{text "\<exists>"}, @{text "\<or>"}, @{text "\<and>"}, @{text "\<longrightarrow>"}, @{text "\<longleftrightarrow>"}, @{text "\<dots>"} \\
1.351 - @{text "\<le>"}, @{text "\<ge>"}, @{text "\<sqinter>"}, @{text "\<squnion>"}, @{text "\<dots>"} \\
1.352 - @{text "\<aleph>"}, @{text "\<triangle>"}, @{text "\<nabla>"}, @{text "\<dots>"} \\
1.353 - @{verbatim "\<foo>"}, @{verbatim "\<bar>"}, @{verbatim "\<baz>"}, @{text "\<dots>"} \\
1.354 - \end{tabular}
1.355 - \medskip
1.356 -
1.357 - Correct rendering via Unicode requires a font that contains glyphs
1.358 - for the corresponding codepoints. Many standard fonts lack that, so
1.359 - Isabelle/jEdit uses the @{verbatim IsabelleText} by default, which
1.360 - ensures that standard collection of Isabelle symbols are actually
1.361 - seen on the screen (or printer).
1.362 -
1.363 - Note that a Java/Swing application can load additional fonts from
1.364 - the file-system only if they are not installed as system font
1.365 - already! This means an old version of @{verbatim IsabelleText} that
1.366 - happens to be already present will prevent Isabelle/jEdit from using
1.367 - its current bundled version. This might result in missing glyphs
1.368 - (black rectangles), since @{verbatim IsabelleText} is occasionally
1.369 - improved in its coverage over time. De-facto there is no need to
1.370 - ``install'' that font on the system in the first place.
1.371 + The appendix of \cite{isabelle-isar-ref} gives an overview of the
1.372 + standard interpretation of finitely many symbols from the infinite
1.373 + collection. Uninterpreted symbols are shown literally.
1.374
1.375 \medskip Technically, the Unicode view on Isabelle symbols is an
1.376 \emph{encoding} in Isabelle/jEdit, which is called @{verbatim
1.377 @@ -369,16 +337,33 @@
1.378 UTF-8-Isabelle} helps to resolve such problems, potentially after
1.379 repairing malformed parts of the text.
1.380
1.381 + \medskip Correct rendering via Unicode requires a font that contains
1.382 + glyphs for the corresponding codepoints. Most system fonts lack
1.383 + that, so Isabelle/jEdit prefers its own application font @{verbatim
1.384 + IsabelleText} by default, which ensures that standard collection of
1.385 + Isabelle symbols are actually seen on the screen (or printer).
1.386 +
1.387 + Note that a Java/Swing application can load additional fonts only if
1.388 + they are not installed as system font already! This means some old
1.389 + version of @{verbatim IsabelleText} that happens to be already
1.390 + present prevents Isabelle/jEdit from using its current bundled
1.391 + version. This might result in missing glyphs (black rectangles),
1.392 + since obsolete versions of @{verbatim IsabelleText} lack recent
1.393 + improvements of Unicode glyph coverage. This problem can be avoided
1.394 + by refraining to ``install'' any version of @{verbatim IsabelleText}
1.395 + in the first place.
1.396 +
1.397 \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
1.398 could delegate the problem to produce Isabelle symbols in their
1.399 Unicode rendering to the underlying operating system and its
1.400 - \emph{input methods}; jEdit also provides various ways to work with
1.401 - \emph{abbreviations} to produce certain non-ASCII characters. Since
1.402 - mathematical characters are far from mainstream use, various
1.403 - specific Isabelle/jEdit input methods are required.
1.404 + \emph{input methods}. Regular jEdit also provides various ways to
1.405 + work with \emph{abbreviations} to produce certain non-ASCII
1.406 + characters. Since none of these standard input methods work
1.407 + satisfactorily for the mathematical characters required for
1.408 + Isabelle, various specific Isabelle/jEdit mechanisms are provided.
1.409
1.410 - Here are some practically relevant input methods for Isabelle
1.411 - symbols:
1.412 + Here is a summary for practically relevant input methods for
1.413 + Isabelle symbols.
1.414
1.415 \begin{enumerate}
1.416
1.417 @@ -390,28 +375,28 @@
1.418 \item Copy / paste from decoded source files: text that is rendered
1.419 as Unicode already may get re-used to produce further such text.
1.420 This also works between different applications, e.g.\ Isabelle/jEdit
1.421 - and some web browser, as long as the same Unicode view on actual
1.422 - Isabelle symbols is used.
1.423 + and some web browser or mail client, as long as the same Unicode
1.424 + view on Isabelle symbols is used uniformly.
1.425
1.426 - \item Copy / paste from prover output within Isabelle/jEdit: the
1.427 - same principles as for text buffers apply. Note that copy in
1.428 - Isabelle \emph{Output} works via the keyboard shortcut @{verbatim
1.429 - "C+v"}, not the jEdit menu (which refers to the main text area).
1.430 + \item Copy / paste from prover output within Isabelle/jEdit. The
1.431 + same principles as for text buffers apply, but note that \emph{copy}
1.432 + in Isabelle \emph{Output} works via the keyboard shortcut @{verbatim
1.433 + "C+c"}, not the jEdit menu.
1.434
1.435 \item Completion provided by Isabelle plugin (see
1.436 \secref{sec:completion}). Isabelle symbols have a canonical name
1.437 and optional abbreviations. This can be used with the text
1.438 completion mechanism of Isabelle/jEdit, to replace a prefix of the
1.439 - actual symbol @{verbatim "\<lambda>"}, or its backslashed name @{verbatim
1.440 - "\\"}@{verbatim "lambda"}, or its ASCII abbreviation @{verbatim
1.441 - "%"}.
1.442 + actual symbol like @{verbatim "\<lambda>"}, or its backslashed name
1.443 + @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
1.444 + @{verbatim "%"}.
1.445
1.446 The following table is an extract of the information provided by the
1.447 - standard @{verbatim "etc/symbols"} file:
1.448 + standard @{file "$ISABELLE_HOME/etc/symbols"} file:
1.449
1.450 \medskip
1.451 \begin{tabular}{lll}
1.452 - \textbf{symbol} & \textbf{abbreviation} & \textbf{backslash escape} \\\hline
1.453 + \textbf{symbol} & \textbf{abbreviation} & \textbf{backslashed name} \\\hline
1.454 @{text "\<lambda>"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\
1.455 @{text "\<Rightarrow>"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\
1.456 @{text "\<Longrightarrow>"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\
1.457 @@ -429,33 +414,28 @@
1.458 @{text "\<in>"} & @{verbatim ":"} & @{verbatim "\\in"} \\
1.459 @{text "\<notin>"} & @{verbatim "~:"} & @{verbatim "\\notin"} \\
1.460 \end{tabular}
1.461 + \medskip
1.462 +
1.463 + Note that the above abbreviations refer to the input method. The
1.464 + logical notation provides ASCII alternatives that often coincide,
1.465 + but deviate occasionally. Writing formal sources directly with
1.466 + ASCII replacement notation like @{verbatim "!"} or @{verbatim "ALL"}
1.467 + or @{verbatim "-->"} is considered very old fashioned in 2013!
1.468
1.469 \end{enumerate}
1.470
1.471 - Some further notes on symbol completion:
1.472 -
1.473 - \begin{itemize}
1.474 -
1.475 - \item The above abbreviations refer to the input method. The logical
1.476 - notation provides ASCII alternatives that often coincide, but
1.477 - deviate occasionally.
1.478 -
1.479 - \item Generic jEdit abbreviations or plugins perform similar source
1.480 - replacement operations; this works for Isabelle as long as the
1.481 - Unicode sequences coincide with the symbol mapping.
1.482 -
1.483 - \item Raw Unicode characters within prover source files should be
1.484 + Raw Unicode characters within prover source files should be
1.485 restricted to informal parts, e.g.\ to write text in non-latin
1.486 alphabets. Mathematical symbols should be defined via the official
1.487 rendering tables, to avoid problems with portability and longterm
1.488 storage of formal text.
1.489
1.490 - \end{itemize}
1.491 -
1.492 \paragraph{Control symbols.} There are some special control symbols
1.493 - to modify the style of a \emph{single} symbol (without
1.494 - nesting). Control symbols may be applied to a region of selected
1.495 - text, either using the \emph{Symbols} panel or keyboard shortcuts.
1.496 + to modify the style of a single symbol (without nesting). Control
1.497 + symbols may be applied to a region of selected text, either using
1.498 + the \emph{Symbols} panel or keyboard shortcuts; these editor
1.499 + operations produce a separate control symbol for each symbol in the
1.500 + text.
1.501
1.502 \medskip
1.503 \begin{tabular}{lll}
1.504 @@ -507,18 +487,11 @@
1.505 *}
1.506
1.507
1.508 -chapter {* Known problems and workarounds *}
1.509 +chapter {* Known problems and workarounds \label{sec:problems} *}
1.510
1.511 text {*
1.512 \begin{itemize}
1.513
1.514 - \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
1.515 - @{verbatim "C+MINUS"} for adjusting the editor font size depend on
1.516 - platform details and national keyboards.
1.517 -
1.518 - \textbf{Workaround:} Use numeric keypad or rebind keys in the
1.519 - jEdit Shortcuts options dialog.
1.520 -
1.521 \item \textbf{Problem:} Lack of dependency management for auxiliary files
1.522 that contribute to a theory (e.g.\ @{command ML_file}).
1.523
1.524 @@ -532,28 +505,8 @@
1.525 \item \textbf{Problem:} No way to delete document nodes from the overall
1.526 collection of theories.
1.527
1.528 - \textbf{Workaround:} Restart whole Isabelle/jEdit session in worst-case
1.529 - situation.
1.530 -
1.531 - \item \textbf{Problem:} Linux: some desktop environments with extreme
1.532 - animation effects may disrupt Java 7 window placement and/or keyboard
1.533 - focus.
1.534 -
1.535 - \textbf{Workaround:} Disable such effects.
1.536 -
1.537 - \item \textbf{Problem:} Linux: some X11 input methods such as IBus tend
1.538 - to disrupt key event handling of Java/Swing.
1.539 -
1.540 - \textbf{Workaround:} Do not use input methods, reset the environment
1.541 - variable @{verbatim XMODIFIERS} within Isabelle settings (default in
1.542 - Isabelle2013-1).
1.543 -
1.544 - \item \textbf{Problem:} Linux: some X11 window managers that are not
1.545 - ``re-parenting'' cause problems with additional windows opened by the Java
1.546 - VM. This affects either historic or neo-minimalistic window managers like
1.547 - ``@{verbatim awesome}'' or ``@{verbatim xmonad}''.
1.548 -
1.549 - \textbf{Workaround:} Use regular re-parenting window manager.
1.550 + \textbf{Workaround:} Ignore unused files. Restart whole
1.551 + Isabelle/jEdit session in worst-case situation.
1.552
1.553 \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
1.554 "COMMAND+COMMA"} for Preferences is in conflict with the jEdit default
1.555 @@ -562,11 +515,32 @@
1.556 \textbf{Workaround:} Remap in jEdit manually according to national
1.557 keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
1.558
1.559 - \item \textbf{Problem:} Mac OS X: Java 7 is officially supported on Lion
1.560 - and Mountain Lion, but not Snow Leopard. It usually works on the latter,
1.561 - although with a small risk of instabilities.
1.562 + \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
1.563 + @{verbatim "C+MINUS"} for adjusting the editor font size depend on
1.564 + platform details and national keyboards.
1.565
1.566 - \textbf{Workaround:} Update to OS X Mountain Lion, or later.
1.567 + \textbf{Workaround:} Use numeric keypad or rebind keys in the
1.568 + jEdit Shortcuts options dialog.
1.569 +
1.570 + \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
1.571 + tend to disrupt key event handling of Java/Swing.
1.572 +
1.573 + \textbf{Workaround:} Do not use input methods, reset the environment
1.574 + variable @{verbatim XMODIFIERS} within Isabelle settings (default in
1.575 + Isabelle2013-1).
1.576 +
1.577 + \item \textbf{Problem:} Some Linux / X11 window managers that are
1.578 + not ``re-parenting'' cause problems with additional windows opened
1.579 + by the Java VM. This affects either historic or neo-minimalistic
1.580 + window managers like @{verbatim awesome} or @{verbatim xmonad}.
1.581 +
1.582 + \textbf{Workaround:} Use regular re-parenting window manager.
1.583 +
1.584 + \item \textbf{Problem:} Recent forks of Linux / X11 window managers
1.585 + and desktop environments (variants of Gnome) disrupt the handling of
1.586 + menu popups and mouse positions of Java/AWT/Swing.
1.587 +
1.588 + \textbf{Workaround:} Use mainstream versions of Linux desktops.
1.589
1.590 \end{itemize}
1.591 *}