misc tuning;
authorwenzelm
Thu May 09 14:22:25 2019 +0200 (6 months ago)
changeset 70252236c1bb128da
parent 70251 b2eac0e8241c
child 70253 cb334a92a4db
misc tuning;
src/Doc/JEdit/JEdit.thy
src/Doc/JEdit/document/root.tex
src/Doc/manual.bib
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Thu May 09 11:35:57 2019 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu May 09 14:22:25 2019 +0200
     1.3 @@ -14,8 +14,9 @@
     1.4    interaction\<close> @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and
     1.5    "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented
     1.6    approach to \<^emph>\<open>continuous proof processing\<close> @{cite "Wenzel:2011:CICM" and
     1.7 -  "Wenzel:2012"}. Many concepts and system components are fit together in
     1.8 -  order to make this work. The main building blocks are as follows.
     1.9 +  "Wenzel:2012" and "Wenzel:2018:FIDE" and "Wenzel:2019:MKM"}. Many concepts
    1.10 +  and system components are fit together in order to make this work. The main
    1.11 +  building blocks are as follows.
    1.12  
    1.13      \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle,
    1.14      see also @{cite "isabelle-implementation"}. It is integrated into the
    1.15 @@ -38,9 +39,10 @@
    1.16      rich formal markup for GUI rendering.
    1.17  
    1.18      \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
    1.19 -    implemented in Java\<^footnote>\<open>\<^url>\<open>https://www.java.com\<close>\<close>. It is easily extensible by
    1.20 -    plugins written in any language that works on the JVM. In the context of
    1.21 -    Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>.
    1.22 +    implemented in Java\<^footnote>\<open>\<^url>\<open>https://adoptopenjdk.net\<close>\<close>. It is easily
    1.23 +    extensible by plugins written in any language that works on the JVM. In
    1.24 +    the context of Isabelle this is always
    1.25 +    Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>.
    1.26  
    1.27      \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the
    1.28      default user-interface for Isabelle. It targets both beginners and
    1.29 @@ -85,17 +87,15 @@
    1.30    the running text editor. Prover IDE functionality is fully activated after
    1.31    successful termination of the build process. A failure may require changing
    1.32    some options and restart of the Isabelle plugin or application. Changing the
    1.33 -  logic session, or the underlying ML system platform (32\,bit versus 64\,bit)
    1.34 -  requires a restart of the whole application to take effect.
    1.35 +  logic session requires a restart of the whole application to take effect.
    1.36  
    1.37 -  \<^medskip>
    1.38 -  The main job of the Prover IDE is to manage sources and their changes,
    1.39 +  \<^medskip> The main job of the Prover IDE is to manage sources and their changes,
    1.40    taking the logical structure as a formal document into account (see also
    1.41    \secref{sec:document-model}). The editor and the prover are connected
    1.42 -  asynchronously in a lock-free manner. The prover is free to organize the
    1.43 -  checking of the formal text in parallel on multiple cores, and provides
    1.44 -  feedback via markup, which is rendered in the editor via colors, boxes,
    1.45 -  squiggly underlines, hyperlinks, popup windows, icons, clickable output etc.
    1.46 +  asynchronously without locking. The prover is free to organize the checking
    1.47 +  of the formal text in parallel on multiple cores, and provides feedback via
    1.48 +  markup, which is rendered in the editor via colors, boxes, squiggly
    1.49 +  underlines, hyperlinks, popup windows, icons, clickable output etc.
    1.50  
    1.51    Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, Windows)
    1.52    or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes formal content via tooltips and/or
    1.53 @@ -140,7 +140,7 @@
    1.54    to update bundled plugins or to add further functionality. This needs to be
    1.55    done with the usual care for such an open bazaar of contributions. Arbitrary
    1.56    combinations of add-on features are apt to cause problems. It is advisable
    1.57 -  to start with the default configuration of Isabelle/jEdit and develop some
    1.58 +  to start with the default configuration of Isabelle/jEdit and develop a
    1.59    sense how it is meant to work, before loading too many other plugins.
    1.60  
    1.61    \<^medskip>
    1.62 @@ -192,7 +192,7 @@
    1.63    Options are usually loaded on startup and saved on shutdown of
    1.64    Isabelle/jEdit. Editing the generated \<^path>\<open>$JEDIT_SETTINGS/properties\<close>
    1.65    or \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> manually while the
    1.66 -  application is running may cause surprise due to lost updates!
    1.67 +  application is running may cause lost updates!
    1.68  \<close>
    1.69  
    1.70  
    1.71 @@ -205,13 +205,13 @@
    1.72    first start of the editor; afterwards the keymap file takes precedence and
    1.73    is no longer affected by change of default properties.
    1.74  
    1.75 -  Users may change their keymap later, but this may lead to conflicts with
    1.76 +  Users may modify their keymap later, but this can lead to conflicts with
    1.77    \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
    1.78  
    1.79    The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
    1.80 -  Isabelle keymap changes that are in conflict with the current jEdit keymap;
    1.81 -  while non-conflicting changes are applied implicitly. This action is
    1.82 -  automatically invoked on Isabelle/jEdit startup.
    1.83 +  Isabelle keymap changes wrt. the current jEdit keymap; non-conflicting
    1.84 +  changes are applied implicitly. This action is automatically invoked on
    1.85 +  Isabelle/jEdit startup.
    1.86  \<close>
    1.87  
    1.88  
    1.89 @@ -280,7 +280,7 @@
    1.90    The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or
    1.91    jEdit, respectively. The defaults are provided by the Isabelle settings
    1.92    environment @{cite "isabelle-system"}, but note that these only work for the
    1.93 -  command-line tool described here, and not the regular application.
    1.94 +  command-line tool described here, and not the desktop application.
    1.95  
    1.96    The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
    1.97    directly to the underlying \<^verbatim>\<open>java\<close> process.
    1.98 @@ -309,7 +309,7 @@
    1.99  
   1.100    The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
   1.101    different server name. The default server name is the official distribution
   1.102 -  name (e.g.\ \<^verbatim>\<open>Isabelle2018\<close>). Thus @{tool jedit_client} can connect to the
   1.103 +  name (e.g.\ \<^verbatim>\<open>Isabelle2019\<close>). Thus @{tool jedit_client} can connect to the
   1.104    Isabelle desktop application without further options.
   1.105  
   1.106    The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
   1.107 @@ -328,17 +328,16 @@
   1.108  
   1.109  text \<open>
   1.110    jEdit is a Java/AWT/Swing application with the ambition to support
   1.111 -  ``native'' look-and-feel on all platforms, within the limits of what Oracle
   1.112 -  as Java provider and major operating system distributors allow (see also
   1.113 -  \secref{sec:problems}).
   1.114 +  ``native'' look-and-feel on all platforms, within the limits of what Java
   1.115 +  provider and major operating systems allow (see also \secref{sec:problems}).
   1.116  
   1.117    Isabelle/jEdit enables platform-specific look-and-feel by default as
   1.118    follows.
   1.119  
   1.120      \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.
   1.121  
   1.122 -    The Linux-specific \<^emph>\<open>GTK+\<close> often works as well, but the overall GTK theme
   1.123 -    and options need to be selected to suite Java/AWT/Swing. Note that Java
   1.124 +    The Linux-specific \<^emph>\<open>GTK+\<close> often works, but the overall GTK theme and
   1.125 +    options need to be selected to suite Java/AWT/Swing. Note that the Java
   1.126      Virtual Machine has no direct influence of GTK rendering.
   1.127  
   1.128      \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
   1.129 @@ -358,32 +357,31 @@
   1.130    historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
   1.131  
   1.132    Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the
   1.133 -  GUI only partially: proper restart of Isabelle/jEdit is usually required.
   1.134 +  GUI only partially: a proper restart of Isabelle/jEdit is usually required.
   1.135  \<close>
   1.136  
   1.137  
   1.138 -subsection \<open>Displays with very high resolution \label{sec:hdpi}\<close>
   1.139 +subsection \<open>Displays with high resolution \label{sec:hdpi}\<close>
   1.140  
   1.141  text \<open>
   1.142 -  In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
   1.143 -  pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
   1.144 -  pixels as adequate for text rendering. After 2016, we have routinely seen
   1.145 -  much higher resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or
   1.146 -  ``Ultra HD'' / ``4K'' at $3840 \times 2160$.
   1.147 -
   1.148 -  GUI frameworks are usually lagging behind, with hard-wired icon sizes and
   1.149 -  tiny fonts. Java and jEdit do provide reasonable support for very high
   1.150 -  resolution, but this requires manual adjustments as described below.
   1.151 +  In 2019, we usually see displays with high resolution like ``Ultra HD'' /
   1.152 +  ``4K'' at $3840 \times 2160$, or more. Old ``Full HD'' displays at $1920
   1.153 +  \times 1080$ pixels are still being used, but Java 11 font-rendering might
   1.154 +  look bad on it (see \secref{sec:problems}) --- this is a good opportunity to
   1.155 +  upgrade to current 4K or 5K technology. GUI layouts are lagging behind the
   1.156 +  high resolution trends, and implicitly assume very old-fashioned $1024
   1.157 +  \times 768$ or $1280 \times 1024$ screens and fonts with 12 or 14 pixels.
   1.158 +  Java and jEdit do provide reasonable support for high resolution, but this
   1.159 +  requires manual adjustments as described below.
   1.160  
   1.161 -  \<^medskip>
   1.162 -  The \<^bold>\<open>operating-system\<close> usually provides some configuration for global
   1.163 -  scaling of text fonts, e.g.\ $120\%$--$250\%$ on Windows. This impacts
   1.164 -  regular GUI elements, when used with native look-and-feel: Linux \<^emph>\<open>GTK+\<close>,
   1.165 -  \<^emph>\<open>Windows\<close>, \<^emph>\<open>Mac OS X\<close>, respectively. Alternatively, it is possible to use
   1.166 -  the platform-independent \<^emph>\<open>Metal\<close> look-and-feel and readjust its main font
   1.167 -  sizes via jEdit options explained below. The Isabelle/jEdit \<^bold>\<open>application\<close>
   1.168 -  provides further options to adjust font sizes in particular GUI elements.
   1.169 -  Here is a summary of all relevant font properties:
   1.170 +  \<^medskip> The \<^bold>\<open>operating-system\<close> often provides some configuration for global
   1.171 +  scaling of text fonts, e.g.\ to enlarge it uniformly by $200\%$. This
   1.172 +  impacts regular GUI elements, when used with native look-and-feel: Linux
   1.173 +  \<^emph>\<open>GTK+\<close>, \<^emph>\<open>Windows\<close>, \<^emph>\<open>Mac OS X\<close>, respectively. Alternatively, it is
   1.174 +  possible to use the platform-independent \<^emph>\<open>Metal\<close> look-and-feel and change
   1.175 +  its main font sizes via jEdit options explained below. The Isabelle/jEdit
   1.176 +  \<^bold>\<open>application\<close> provides further options to adjust font sizes in particular
   1.177 +  GUI elements. Here is a summary of all relevant font properties:
   1.178  
   1.179      \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font,
   1.180      which is also used as reference point for various derived font sizes,
   1.181 @@ -406,15 +404,15 @@
   1.182      e.g.\ relevant for Isabelle/Scala command-line.
   1.183  
   1.184    In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is configured
   1.185 -  with custom fonts at 30 pixels, and the main text area and console at 36
   1.186 -  pixels. This leads to decent rendering quality, despite the old-fashioned
   1.187 -  appearance of \<^emph>\<open>Metal\<close>.
   1.188 +  with custom fonts at 36 pixels, and the main text area and console at 40
   1.189 +  pixels. This leads to fairly good rendering quality, despite the
   1.190 +  old-fashioned appearance of \<^emph>\<open>Metal\<close>.
   1.191  
   1.192    \begin{sidewaysfigure}[!htb]
   1.193    \begin{center}
   1.194    \includegraphics[width=\textwidth]{isabelle-jedit-hdpi}
   1.195    \end{center}
   1.196 -  \caption{Metal look-and-feel with custom fonts for very high resolution}
   1.197 +  \caption{Metal look-and-feel with custom fonts for high resolution}
   1.198    \label{fig:isabelle-jedit-hdpi}
   1.199    \end{sidewaysfigure}
   1.200  \<close>
   1.201 @@ -478,7 +476,7 @@
   1.202    Isabelle sources consist of \<^emph>\<open>symbols\<close> that extend plain ASCII to allow
   1.203    infinitely many mathematical symbols within the formal sources. This works
   1.204    without depending on particular encodings and varying Unicode
   1.205 -  standards.\<^footnote>\<open>Raw Unicode characters within formal sources would compromise
   1.206 +  standards.\<^footnote>\<open>Raw Unicode characters within formal sources compromise
   1.207    portability and reliability in the face of changing interpretation of
   1.208    special features of Unicode, such as Combining Characters or Bi-directional
   1.209    Text.\<close> See @{cite "Wenzel:2011:CICM"}.
   1.210 @@ -486,10 +484,10 @@
   1.211    For the prover back-end, formal text consists of ASCII characters that are
   1.212    grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or symbolic
   1.213    ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
   1.214 -  physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
   1.215 -  example. This symbol interpretation is specified by the Isabelle system
   1.216 -  distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the
   1.217 -  user in \<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close>.
   1.218 +  physically via Unicode glyphs, to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for example.
   1.219 +  This symbol interpretation is specified by the Isabelle system distribution
   1.220 +  in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the user in
   1.221 +  \<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close>.
   1.222  
   1.223    The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
   1.224    standard interpretation of finitely many symbols from the infinite
   1.225 @@ -519,17 +517,18 @@
   1.226    with the Isabelle symbol encoding, the fallback-encoding UTF-8 is used and
   1.227    Isabelle symbols remain in literal \<^verbatim>\<open>\<symbol>\<close> form. The jEdit menu
   1.228    operation \<^emph>\<open>Utilities~/ Buffer Options~/ Character encoding\<close> allows to
   1.229 -  enforce the UTF-8-Isabelle, but this will also change original Unicode
   1.230 -  text into Isabelle symbols when saving the file!
   1.231 +  enforce \<^verbatim>\<open>UTF-8-Isabelle\<close>, but this will also change original Unicode text
   1.232 +  into Isabelle symbols when saving the file!
   1.233  \<close>
   1.234  
   1.235  paragraph \<open>Font.\<close>
   1.236  text \<open>Correct rendering via Unicode requires a font that contains glyphs for
   1.237    the corresponding codepoints. There are also various unusual symbols with
   1.238    particular purpose in Isabelle, e.g.\ control symbols and very long arrows.
   1.239 -  Isabelle/jEdit prefers its own font collection \<^verbatim>\<open>Isabelle DejaVu\<close>, which
   1.240 -  ensures that all standard Isabelle symbols are shown on the screen (or
   1.241 -  printer) as expected.
   1.242 +  Isabelle/jEdit prefers its own font collection \<^verbatim>\<open>Isabelle DejaVu\<close>, with
   1.243 +  families \<^verbatim>\<open>Serif\<close> (default for help texts), \<^verbatim>\<open>Sans\<close> (default for GUI
   1.244 +  elements), \<^verbatim>\<open>Mono Sans\<close> (default for text area). This ensures that all
   1.245 +  standard Isabelle symbols are shown on the screen (or printer) as expected.
   1.246  
   1.247    Note that a Java/AWT/Swing application can load additional fonts only if
   1.248    they are not installed on the operating system already! Outdated versions of
   1.249 @@ -537,7 +536,7 @@
   1.250    Isabelle/jEdit to use its bundled version. This could lead to missing glyphs
   1.251    (black rectangles), when the system version of a font is older than the
   1.252    application version. This problem can be avoided by refraining to
   1.253 -  ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the first place, although it
   1.254 +  ``install'' a copy of the Isabelle fonts in the first place, although it
   1.255    might be tempting to use the same font in other applications.
   1.256  
   1.257    HTML pages generated by Isabelle refer to the same Isabelle fonts as a
   1.258 @@ -562,11 +561,10 @@
   1.259    representation with some additional information about \<^emph>\<open>symbol
   1.260    abbreviations\<close> (see below).
   1.261  
   1.262 -  \<^enum> Copy/paste from decoded source files: text that is rendered as Unicode
   1.263 -  already can be re-used to produce further text. This also works between
   1.264 -  different applications, e.g.\ Isabelle/jEdit and some web browser or mail
   1.265 -  client, as long as the same Unicode interpretation of Isabelle symbols is
   1.266 -  used.
   1.267 +  \<^enum> Copy/paste from decoded source files: text that is already rendered as
   1.268 +  Unicode can be re-used for other text. This also works between different
   1.269 +  applications, e.g.\ Isabelle/jEdit and some web browser or mail client, as
   1.270 +  long as the same Unicode interpretation of Isabelle symbols is used.
   1.271  
   1.272    \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same principles
   1.273    as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary Isabelle/jEdit
   1.274 @@ -658,7 +656,8 @@
   1.275    For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, and \<^verbatim>\<open>view\<close>
   1.276    to the current editor view of jEdit. The Scala expression
   1.277    \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot of the current buffer
   1.278 -  within the current editor view.
   1.279 +  within the current editor view: it allows to retrieve document markup in a
   1.280 +  timeless~/ stateless manner, while the prover continues its processing.
   1.281  
   1.282    This helps to explore Isabelle/Scala functionality interactively. Some care
   1.283    is required to avoid interference with the internals of the running
   1.284 @@ -671,7 +670,7 @@
   1.285  text \<open>
   1.286    File specifications in jEdit follow various formats and conventions
   1.287    according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by
   1.288 -  additional plugins. This allows to access remote files via the \<^verbatim>\<open>http:\<close>
   1.289 +  additional plugins. This allows to access remote files via the \<^verbatim>\<open>https:\<close>
   1.290    protocol prefix, for example. Isabelle/jEdit attempts to work with the
   1.291    file-system model of jEdit as far as possible. In particular, theory sources
   1.292    are passed directly from the editor to the prover, without indirection via
   1.293 @@ -686,20 +685,19 @@
   1.294  
   1.295    The Java notation for files needs to be distinguished from the one of
   1.296    Isabelle, which uses POSIX notation with forward slashes on \<^emph>\<open>all\<close>
   1.297 -  platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and
   1.298 -  driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,
   1.299 -  environment variables from the Isabelle process may be used freely, e.g.\
   1.300 -  \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME/README\<close>. There are special
   1.301 -  shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.
   1.302 +  platforms. Isabelle/ML on Windows uses Unix-style path notation, with drive
   1.303 +  letters as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Environment variables from the
   1.304 +  Isabelle process may be used freely, e.g.\ \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or
   1.305 +  \<^file>\<open>$POLYML_HOME/README\<close>. There are special shortcuts: \<^dir>\<open>~\<close> for
   1.306 +  \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.
   1.307  
   1.308 -  \<^medskip>
   1.309 -  Since jEdit happens to support environment variables within file
   1.310 +  \<^medskip> Since jEdit happens to support environment variables within file
   1.311    specifications as well, it is natural to use similar notation within the
   1.312    editor, e.g.\ in the file-browser. This does not work in full generality,
   1.313    though, due to the bias of jEdit towards platform-specific notation and of
   1.314    Isabelle towards POSIX. Moreover, the Isabelle settings environment is not
   1.315 -  yet active when starting Isabelle/jEdit via its standard application
   1.316 -  wrapper, in contrast to @{tool jedit} run from the command line
   1.317 +  accessible when starting Isabelle/jEdit via the desktop application wrapper,
   1.318 +  in contrast to @{tool jedit} run from the command line
   1.319    (\secref{sec:command-line}).
   1.320  
   1.321    Isabelle/jEdit imitates important system settings within the Java process
   1.322 @@ -708,12 +706,11 @@
   1.323    \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> for
   1.324    these two important locations.
   1.325  
   1.326 -  \<^medskip>
   1.327 -  Path specifications in prover input or output usually include formal markup
   1.328 -  that turns it into a hyperlink (see also \secref{sec:tooltips-hyperlinks}).
   1.329 -  This allows to open the corresponding file in the text editor, independently
   1.330 -  of the path notation. If the path refers to a directory, the jEdit file
   1.331 -  browser is opened on it.
   1.332 +  \<^medskip> Path specifications in prover input or output usually include formal
   1.333 +  markup that turns it into a hyperlink (see also
   1.334 +  \secref{sec:tooltips-hyperlinks}). This allows to open the corresponding
   1.335 +  file in the text editor, independently of the path notation. If the path
   1.336 +  refers to a directory, it is opened in the jEdit file browser.
   1.337  
   1.338    Formally checked paths in prover input are subject to completion
   1.339    (\secref{sec:completion}): partial specifications are resolved via directory
   1.340 @@ -726,7 +723,7 @@
   1.341  text \<open>
   1.342    Isabelle/jEdit augments the existing indentation facilities of jEdit to take
   1.343    the structure of theory and proof texts into account. There is also special
   1.344 -  support for unstructured proof scripts.
   1.345 +  support for unstructured proof scripts (\<^theory_text>\<open>apply\<close> etc.).
   1.346  
   1.347      \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar.
   1.348  
   1.349 @@ -735,7 +732,7 @@
   1.350      approximation may need further manual tuning.
   1.351  
   1.352      Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the old
   1.353 -    and the new line according to command keywords only: this leads to precise
   1.354 +    and the new line according to command keywords only: leading to precise
   1.355      alignment of the main Isar language elements. This depends on option
   1.356      @{system_option_def "jedit_indent_newline"} (enabled by default).
   1.357  
   1.358 @@ -744,11 +741,10 @@
   1.359      on option @{system_option_def "jedit_indent_input"} (enabled by default).
   1.360  
   1.361      \<^descr>[Semantic indentation] adds additional white space to unstructured proof
   1.362 -    scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
   1.363 -    of ongoing document processing and may thus lag behind, when the user is
   1.364 -    editing too quickly; see also option @{system_option_def
   1.365 -    "jedit_script_indent"} and @{system_option_def
   1.366 -    "jedit_script_indent_limit"}.
   1.367 +    scripts via the number of subgoals. This requires information of ongoing
   1.368 +    document processing and may thus lag behind when the user is editing too
   1.369 +    quickly; see also option @{system_option_def "jedit_script_indent"} and
   1.370 +    @{system_option_def "jedit_script_indent_limit"}.
   1.371  
   1.372    The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
   1.373    Isabelle / General\<close>. A prerequisite for advanced indentation is \<^emph>\<open>Utilities
   1.374 @@ -1132,7 +1128,7 @@
   1.375  
   1.376      \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
   1.377      regular expression, in the notation that is commonly used on the Java
   1.378 -    platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>
   1.379 +    platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
   1.380      This may serve as an additional visual filter of the result.
   1.381  
   1.382      \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
   1.383 @@ -1331,7 +1327,7 @@
   1.384      completion of name-space entries propose antiquotation names.
   1.385  
   1.386    With some practice, input of quoted sub-languages and antiquotations of
   1.387 -  embedded languages should work fluently. Note that national keyboard layouts
   1.388 +  embedded languages should work smoothly. Note that national keyboard layouts
   1.389    might cause problems with back-quote as dead key, but double quote can be
   1.390    used instead.
   1.391  \<close>
   1.392 @@ -1426,7 +1422,7 @@
   1.393  
   1.394    Already recognized names are \<^emph>\<open>not\<close> completed further, but completion may be
   1.395    extended by appending a suffix of underscores. This provokes a failed
   1.396 -  lookup, and another completion attempt while ignoring the underscores. For
   1.397 +  lookup, and another completion attempt (ignoring the underscores). For
   1.398    example, in a name space where \<^verbatim>\<open>foo\<close> and \<^verbatim>\<open>foobar\<close> are known, the input
   1.399    \<^verbatim>\<open>foo\<close> remains unchanged, but \<^verbatim>\<open>foo_\<close> may be completed to \<^verbatim>\<open>foo\<close> or
   1.400    \<^verbatim>\<open>foobar\<close>.
   1.401 @@ -1854,7 +1850,7 @@
   1.402  
   1.403  text \<open>
   1.404    Document text is internally structured in paragraphs and nested lists, using
   1.405 -  notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>. There are
   1.406 +  notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>https://commonmark.org\<close>\<close>. There are
   1.407    special control symbols for items of different kinds of lists, corresponding
   1.408    to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This is illustrated
   1.409    in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
   1.410 @@ -1869,8 +1865,8 @@
   1.411  
   1.412    Items take colour according to the depth of nested lists. This helps to
   1.413    explore the implicit rules for list structure interactively. There is also
   1.414 -  markup for individual paragraphs in the text: it may be explored via mouse
   1.415 -  hovering with \<^verbatim>\<open>CONTROL\<close> / \<^verbatim>\<open>COMMAND\<close> as usual
   1.416 +  markup for individual items and paragraphs in the text: it may be explored
   1.417 +  via mouse hovering with \<^verbatim>\<open>CONTROL\<close> / \<^verbatim>\<open>COMMAND\<close> as usual
   1.418    (\secref{sec:tooltips-hyperlinks}).
   1.419  \<close>
   1.420  
   1.421 @@ -2078,7 +2074,7 @@
   1.422    messages starts with the first activation of the corresponding dockable
   1.423    window; earlier messages are lost.
   1.424  
   1.425 -  Actual display of protocol messages causes considerable slowdown, so it is
   1.426 +  Display of protocol messages causes considerable slowdown, so it is
   1.427    important to undock all \<^emph>\<open>Protocol\<close> panels for production work.
   1.428  
   1.429    \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close>
     2.1 --- a/src/Doc/JEdit/document/root.tex	Thu May 09 11:35:57 2019 +0200
     2.2 +++ b/src/Doc/JEdit/document/root.tex	Thu May 09 14:22:25 2019 +0200
     2.3 @@ -63,11 +63,11 @@
     2.4  Research and implementation of concepts around PIDE and Isabelle/jEdit has
     2.5  started in 2008 and was kindly supported by:
     2.6  \begin{itemize}
     2.7 -\item TU M\"unchen \url{http://www.in.tum.de}
     2.8 -\item BMBF \url{http://www.bmbf.de}
     2.9 -\item Universit\'e Paris-Sud \url{http://www.u-psud.fr}
    2.10 -\item Digiteo \url{http://www.digiteo.fr}
    2.11 -\item ANR \url{http://www.agence-nationale-recherche.fr}
    2.12 +\item TU M\"unchen \url{https://www.in.tum.de}
    2.13 +\item BMBF \url{https://www.bmbf.de}
    2.14 +\item Universit\'e Paris-Sud \url{https://www.u-psud.fr}
    2.15 +\item Digiteo \url{https://www.digiteo.fr}
    2.16 +\item ANR \url{https://www.agence-nationale-recherche.fr}
    2.17  \end{itemize}
    2.18  
    2.19  
     3.1 --- a/src/Doc/manual.bib	Thu May 09 11:35:57 2019 +0200
     3.2 +++ b/src/Doc/manual.bib	Thu May 09 14:22:25 2019 +0200
     3.3 @@ -2186,6 +2186,30 @@
     3.4    note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?UITP2014:11}}
     3.5  }
     3.6  
     3.7 +@InProceedings{Wenzel:2018:FIDE,
     3.8 +  author = {Makarius Wenzel},
     3.9 +  title = {{Isabelle/jEdit} as {IDE} for domain-specific formal
    3.10 +    languages and informal text documents},
    3.11 +  booktitle = {F-IDE Workshop 2018 (Oxford, UK)},
    3.12 +  year = {2018},
    3.13 +  editor = {Paolo Masci and Rosemary Monahan and Virgile Prevosto},
    3.14 +  number = 284,
    3.15 +  series = {EPTCS},
    3.16 +  note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?FIDE2018.6}},
    3.17 +}
    3.18 +
    3.19 +@InProceedings{Wenzel:2019:MKM,
    3.20 +  author = {Makarius Wenzel},
    3.21 +  title = {Interaction with Formal Mathematical Documents in {Isabelle/PIDE}},
    3.22 +  booktitle = {Intelligent Computer Mathematics (CICM 2019)},
    3.23 +  year = {2019},
    3.24 +  editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Sacerdoti Coen, Claudio},
    3.25 +  volume = {????},
    3.26 +  series = LNAI,
    3.27 +  publisher = {Springer},
    3.28 +  note = {\url{https://arxiv.org/abs/1905.01735}}
    3.29 +}
    3.30 +
    3.31  @book{principia,
    3.32    author	= {A. N. Whitehead and B. Russell},
    3.33    title		= {Principia Mathematica},