merged
authorwenzelm
Sat Sep 23 20:09:16 2017 +0200 (19 months ago)
changeset 66688ebb97a834338
parent 66662 4b10fa05423b
parent 66687 cd8ad4eddb8a
child 66689 ef81649ad051
merged
NEWS
     1.1 --- a/.hgtags	Fri Sep 22 14:14:41 2017 -0300
     1.2 +++ b/.hgtags	Sat Sep 23 20:09:16 2017 +0200
     1.3 @@ -36,3 +36,4 @@
     1.4  a5dd01b682189f5412460b78b9611f7665b26894 Isabelle2017-RC0
     1.5  34b20f7236ea2b59c1994ee10770267bb156c9e5 Isabelle2017-RC1
     1.6  e9d8ff531700c7c19ea6f9c1315c06015f95d2b8 Isabelle2017-RC2
     1.7 +4f73201b8043b92783824b55dcded6891de0a41e Isabelle2017-RC3
     2.1 --- a/Admin/components/components.sha1	Fri Sep 22 14:14:41 2017 -0300
     2.2 +++ b/Admin/components/components.sha1	Sat Sep 23 20:09:16 2017 +0200
     2.3 @@ -6,6 +6,8 @@
     2.4  70105fd6fbfd1a868383fc510772b95234325d31  csdp-6.x.tar.gz
     2.5  2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
     2.6  d70bfbe63590153c07709dea7084fbc39c669841  cvc4-1.5-1.tar.gz
     2.7 +541eac340464c5d34b70bb163ae277cc8829c40f  cvc4-1.5-2.tar.gz
     2.8 +1a44895d2a440091a15cc92d7f77a06a2e432507  cvc4-1.5-3.tar.gz
     2.9  a5e02b5e990da4275dc5d4480c3b72fc73160c28  cvc4-1.5pre-1.tar.gz
    2.10  4d9658fd2688ae8ac78da8fdfcbf85960f871b71  cvc4-1.5pre-2.tar.gz
    2.11  b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9  cvc4-1.5pre-3.tar.gz
    2.12 @@ -36,6 +38,7 @@
    2.13  e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
    2.14  b98a98025d1f7e560ca6864a53296137dae736b4  e-1.6.tar.gz
    2.15  c11b25c919e2ec44fe2b6ac2086337b456344e97  e-1.8.tar.gz
    2.16 +a895a96ec7e6fcc275114bb9b4c92b20fac73dba  e-2.0-1.tar.gz
    2.17  6b962a6b4539b7ca4199977973c61a8c98a492e8  e-2.0.tar.gz
    2.18  6d34b18ca0aa1e10bab6413045d079188c0e2dfb  exec_process-1.0.1.tar.gz
    2.19  8b9bffd10e396d965e815418295f2ee2849bea75  exec_process-1.0.2.tar.gz
     3.1 --- a/Admin/components/main	Fri Sep 22 14:14:41 2017 -0300
     3.2 +++ b/Admin/components/main	Sat Sep 23 20:09:16 2017 +0200
     3.3 @@ -1,8 +1,8 @@
     3.4  #main components for everyday use, without big impact on overall build time
     3.5  bash_process-1.2.1
     3.6  csdp-6.x
     3.7 -cvc4-1.5-1
     3.8 -e-2.0
     3.9 +cvc4-1.5-3
    3.10 +e-2.0-1
    3.11  isabelle_fonts-20160830
    3.12  jdk-8u144
    3.13  jedit_build-20170319
     4.1 --- a/NEWS	Fri Sep 22 14:14:41 2017 -0300
     4.2 +++ b/NEWS	Sat Sep 23 20:09:16 2017 +0200
     4.3 @@ -126,7 +126,7 @@
     4.4  * Deleting the last code equations for a particular function using
     4.5  [code del] results in function with no equations (runtime abort) rather
     4.6  than an unimplemented function (generation time abort). Use explicit
     4.7 -[[code drop:]] to enforce the latter. Minor INCOMPATIBILTIY.
     4.8 +[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
     4.9  
    4.10  * Proper concept of code declarations in code.ML:
    4.11    - Regular code declarations act only on the global theory level, being
    4.12 @@ -316,7 +316,7 @@
    4.13  serves as example for alternative PIDE front-ends.
    4.14  
    4.15  * Command-line tool "isabelle imports" helps to maintain theory imports
    4.16 -wrt. session structure. Examples:
    4.17 +wrt. session structure. Examples for the main Isabelle distribution:
    4.18  
    4.19    isabelle imports -I -a
    4.20    isabelle imports -U -a
     5.1 --- a/lib/scripts/getfunctions	Fri Sep 22 14:14:41 2017 -0300
     5.2 +++ b/lib/scripts/getfunctions	Sat Sep 23 20:09:16 2017 +0200
     5.3 @@ -70,6 +70,7 @@
     5.4  #classpath
     5.5  function classpath ()
     5.6  {
     5.7 +  local X=""
     5.8    for X in "$@"
     5.9    do
    5.10      if [ -z "$ISABELLE_CLASSPATH" ]; then
    5.11 @@ -98,6 +99,7 @@
    5.12  {
    5.13    SPLITARRAY=()
    5.14    local IFS="$1"; shift
    5.15 +  local X=""
    5.16    for X in $*
    5.17    do
    5.18      SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
    5.19 @@ -149,6 +151,7 @@
    5.20  #init component forest
    5.21  function init_components ()
    5.22  {
    5.23 +  local REPLY=""
    5.24    local BASE="$1"
    5.25    local CATALOG="$2"
    5.26    local COMPONENT=""
     6.1 --- a/src/Doc/Implementation/ML.thy	Fri Sep 22 14:14:41 2017 -0300
     6.2 +++ b/src/Doc/Implementation/ML.thy	Sat Sep 23 20:09:16 2017 +0200
     6.3 @@ -946,9 +946,9 @@
     6.4    Another benefit of @{ML add_content} is its ``open'' form as a function on
     6.5    buffers that can be continued in further linear transformations, folding
     6.6    etc. Thus it is more compositional than the naive @{ML slow_content}. As
     6.7 -  realistic example, compare the old-style @{ML "Term.maxidx_of_term: term ->
     6.8 -  int"} with the newer @{ML "Term.maxidx_term: term -> int -> int"} in
     6.9 -  Isabelle/Pure.
    6.10 +  realistic example, compare the old-style
    6.11 +  @{ML "Term.maxidx_of_term: term -> int"} with the newer @{ML
    6.12 +  "Term.maxidx_term: term -> int -> int"} in Isabelle/Pure.
    6.13  
    6.14    Note that @{ML fast_content} above is only defined as example. In many
    6.15    practical situations, it is customary to provide the incremental @{ML
    6.16 @@ -1851,18 +1851,18 @@
    6.17    evaluation via promises, evaluation with time limit etc.
    6.18  
    6.19    \<^medskip>
    6.20 -  An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction \<^verbatim>\<open>fn
    6.21 -  () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of type
    6.22 -  \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required to
    6.23 -  tell them apart --- the static type-system of SML is only of limited help
    6.24 +  An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction
    6.25 +  \<^verbatim>\<open>fn () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of
    6.26 +  type \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required
    6.27 +  to tell them apart --- the static type-system of SML is only of limited help
    6.28    here.
    6.29  
    6.30 -  The first form is more intuitive: some combinator \<open>(unit -> 'a) -> 'a\<close>
    6.31 -  applies the given function to \<open>()\<close> to initiate the postponed evaluation
    6.32 -  process. The second form is more flexible: some combinator \<open>('a -> 'b) -> 'a
    6.33 -  -> 'b\<close> acts like a modified form of function application; several such
    6.34 -  combinators may be cascaded to modify a given function, before it is
    6.35 -  ultimately applied to some argument.
    6.36 +  The first form is more intuitive: some combinator \<^verbatim>\<open>(unit -> 'a) -> 'a\<close>
    6.37 +  applies the given function to \<^verbatim>\<open>()\<close> to initiate the postponed evaluation
    6.38 +  process. The second form is more flexible: some combinator
    6.39 +  \<^verbatim>\<open>('a -> 'b) -> 'a -> 'b\<close> acts like a modified form of function application;
    6.40 +  several such combinators may be cascaded to modify a given function, before
    6.41 +  it is ultimately applied to some argument.
    6.42  
    6.43    \<^medskip>
    6.44    \<^emph>\<open>Reified results\<close> make the disjoint sum of regular values versions
     7.1 --- a/src/Doc/Implementation/Proof.thy	Fri Sep 22 14:14:41 2017 -0300
     7.2 +++ b/src/Doc/Implementation/Proof.thy	Sat Sep 23 20:09:16 2017 +0200
     7.3 @@ -101,7 +101,8 @@
     7.4    @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
     7.5    @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
     7.6    @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
     7.7 -  ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\
     7.8 +  ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list)
     7.9 +    * Proof.context"} \\
    7.10    @{index_ML Variable.focus: "binding list option -> term -> Proof.context ->
    7.11    ((string * (string * typ)) list * term) * Proof.context"} \\
    7.12    \end{mldecls}
     8.1 --- a/src/Doc/JEdit/JEdit.thy	Fri Sep 22 14:14:41 2017 -0300
     8.2 +++ b/src/Doc/JEdit/JEdit.thy	Sat Sep 23 20:09:16 2017 +0200
     8.3 @@ -26,9 +26,9 @@
     8.4      \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It
     8.5      extends the pure logical environment of Isabelle/ML towards the outer
     8.6      world of graphical user interfaces, text editors, IDE frameworks, web
     8.7 -    services etc. Special infrastructure allows to transfer algebraic
     8.8 -    datatypes and formatted text easily between ML and Scala, using
     8.9 -    asynchronous protocol commands.
    8.10 +    services, SSH servers, SQL databases etc. Special infrastructure allows to
    8.11 +    transfer algebraic datatypes and formatted text easily between ML and
    8.12 +    Scala, using asynchronous protocol commands.
    8.13  
    8.14      \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It
    8.15      is built around a concept of parallel and asynchronous document
    8.16 @@ -79,14 +79,14 @@
    8.17  
    8.18    The options allow to specify a logic session name, but the same selector is
    8.19    also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After
    8.20 -  application startup, the selected logic session image is provided
    8.21 +  startup of the Isabelle plugin, the selected logic session image is provided
    8.22    automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
    8.23 -  absent or outdated wrt.\ its sources, the build process updates it while the
    8.24 -  text editor is running. Prover IDE functionality is only activated after
    8.25 +  absent or outdated wrt.\ its sources, the build process updates it within
    8.26 +  the running text editor. Prover IDE functionality is fully activated after
    8.27    successful termination of the build process. A failure may require changing
    8.28 -  some options and restart the application. Changing the logic session, or the
    8.29 -  underlying ML system platform (32\,bit versus 64\,bit) requires a restart of
    8.30 -  the application to take effect.
    8.31 +  some options and restart of the Isabelle plugin or application. Changing the
    8.32 +  logic session, or the underlying ML system platform (32\,bit versus 64\,bit)
    8.33 +  requires a restart of the whole application to take effect.
    8.34  
    8.35    \<^medskip>
    8.36    The main job of the Prover IDE is to manage sources and their changes,
    8.37 @@ -122,7 +122,7 @@
    8.38    individual plugins.
    8.39  
    8.40    Most of the information about jEdit is relevant for Isabelle/jEdit as well,
    8.41 -  but one needs to keep in mind that defaults sometimes differ, and the
    8.42 +  but users need to keep in mind that defaults sometimes differ, and the
    8.43    official jEdit documentation does not know about the Isabelle plugin with
    8.44    its support for continuous checking of formal source text: jEdit is a plain
    8.45    text editor, but Isabelle/jEdit is a Prover IDE.
    8.46 @@ -144,16 +144,17 @@
    8.47    sense how it is meant to work, before loading too many other plugins.
    8.48  
    8.49    \<^medskip>
    8.50 -  The \<^emph>\<open>Isabelle\<close> plugin provides the main Prover IDE functionality of
    8.51 -  Isabelle/jEdit: it manages the prover session in the background. A few
    8.52 +  The \<^emph>\<open>Isabelle\<close> plugin is responsible for the main Prover IDE functionality
    8.53 +  of Isabelle/jEdit: it manages the prover session in the background. A few
    8.54    additional plugins are bundled with Isabelle/jEdit for convenience or out of
    8.55 -  necessity, notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin
    8.56 +  necessity, notably \<^emph>\<open>Console\<close> with its \<^emph>\<open>Scala\<close> sub-plugin
    8.57    (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
    8.58    parsers for document tree structure (\secref{sec:sidekick}). The
    8.59    \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
    8.60    formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
    8.61    (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
    8.62 -  of bundled plugins, but have no particular use in Isabelle/jEdit. \<close>
    8.63 +  of bundled plugins, but have no particular use in Isabelle/jEdit.
    8.64 +\<close>
    8.65  
    8.66  
    8.67  subsection \<open>Options \label{sec:options}\<close>
    8.68 @@ -174,11 +175,11 @@
    8.69  
    8.70    Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable in
    8.71    Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there
    8.72 -  are various options for rendering of document content, which are
    8.73 -  configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin
    8.74 -  Options~/ Isabelle\<close> in jEdit provides a view on a subset of Isabelle system
    8.75 -  options. Note that some of these options affect general parameters that are
    8.76 -  relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
    8.77 +  are various options for rendering document content, which are configurable
    8.78 +  via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin Options~/
    8.79 +  Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options.
    8.80 +  Note that some of these options affect general parameters that are relevant
    8.81 +  outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
    8.82    @{system_option parallel_proofs} for the Isabelle build tool @{cite
    8.83    "isabelle-system"}, but it is possible to use the settings variable
    8.84    @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds
    8.85 @@ -189,10 +190,9 @@
    8.86  
    8.87    \<^medskip>
    8.88    Options are usually loaded on startup and saved on shutdown of
    8.89 -  Isabelle/jEdit. Editing the machine-generated @{path
    8.90 -  "$JEDIT_SETTINGS/properties"} or @{path
    8.91 -  "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
    8.92 -  running is likely to cause surprise due to lost update!
    8.93 +  Isabelle/jEdit. Editing the generated @{path "$JEDIT_SETTINGS/properties"}
    8.94 +  or @{path "$ISABELLE_HOME_USER/etc/preferences"} manually while the
    8.95 +  application is running may cause surprise due to lost updates!
    8.96  \<close>
    8.97  
    8.98  
    8.99 @@ -205,14 +205,12 @@
   8.100    first start of the editor; afterwards the keymap file takes precedence and
   8.101    is no longer affected by change of default properties.
   8.102  
   8.103 -  Users may change their keymap later, but need to keep its content @{path
   8.104 -  "$JEDIT_SETTINGS/keymaps"} in sync with \<^verbatim>\<open>shortcut\<close> properties in
   8.105 -  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
   8.106 +  Users may change their keymap later, but this may lead to conflicts with
   8.107 +  \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
   8.108  
   8.109 -  \<^medskip>
   8.110    The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
   8.111    Isabelle keymap changes that are in conflict with the current jEdit keymap;
   8.112 -  non-conflicting changes are always applied implicitly. This action is
   8.113 +  while non-conflicting changes are applied implicitly. This action is
   8.114    automatically invoked on Isabelle/jEdit startup.
   8.115  \<close>
   8.116  
   8.117 @@ -232,11 +230,13 @@
   8.118    Options are:
   8.119      -D NAME=X    set JVM system property
   8.120      -J OPTION    add JVM runtime option
   8.121 +                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
   8.122      -R           open ROOT entry of logic session and use its parent
   8.123      -b           build only
   8.124      -d DIR       include session directory
   8.125      -f           fresh build
   8.126      -j OPTION    add jEdit runtime option
   8.127 +                 (default $JEDIT_OPTIONS)
   8.128      -l NAME      logic image name
   8.129      -m MODE      add print mode for output
   8.130      -n           no build of session image on startup
   8.131 @@ -248,8 +248,8 @@
   8.132  
   8.133    The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used
   8.134    for proof processing. Additional session root directories may be included
   8.135 -  via option \<^verbatim>\<open>-d\<close> to augment that name space of @{tool build} @{cite
   8.136 -  "isabelle-system"}.
   8.137 +  via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
   8.138 +  "isabelle-system"}).
   8.139  
   8.140    By default, the specified image is checked and built on demand. The \<^verbatim>\<open>-s\<close>
   8.141    option determines where to store the result session image of @{tool build}.
   8.142 @@ -266,11 +266,10 @@
   8.143    do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
   8.144    Isabelle/jEdit), without requiring command-line invocation.
   8.145  
   8.146 -  The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options allow to pass additional low-level options to
   8.147 -  the JVM or jEdit, respectively. The defaults are provided by the Isabelle
   8.148 -  settings environment @{cite "isabelle-system"}, but note that these only
   8.149 -  work for the command-line tool described here, and not the regular
   8.150 -  application.
   8.151 +  The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or
   8.152 +  jEdit, respectively. The defaults are provided by the Isabelle settings
   8.153 +  environment @{cite "isabelle-system"}, but note that these only work for the
   8.154 +  command-line tool described here, and not the regular application.
   8.155  
   8.156    The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
   8.157    directly to the underlying \<^verbatim>\<open>java\<close> process.
   8.158 @@ -299,7 +298,7 @@
   8.159  
   8.160    The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
   8.161    different server name. The default server name is the official distribution
   8.162 -  name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<close>). Thus @{tool jedit_client} can connect to the
   8.163 +  name (e.g.\ \<^verbatim>\<open>Isabelle2017\<close>). Thus @{tool jedit_client} can connect to the
   8.164    Isabelle desktop application without further options.
   8.165  
   8.166    The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
   8.167 @@ -317,7 +316,7 @@
   8.168  subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close>
   8.169  
   8.170  text \<open>
   8.171 -  jEdit is a Java/AWT/Swing application with some ambition to support
   8.172 +  jEdit is a Java/AWT/Swing application with the ambition to support
   8.173    ``native'' look-and-feel on all platforms, within the limits of what Oracle
   8.174    as Java provider and major operating system distributors allow (see also
   8.175    \secref{sec:problems}).
   8.176 @@ -327,9 +326,9 @@
   8.177  
   8.178      \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.
   8.179  
   8.180 -    The Linux-specific \<^emph>\<open>GTK+\<close> also works under the side-condition that the
   8.181 -    overall GTK theme and options are selected in a way that works with Java
   8.182 -    AWT/Swing. The JVM has no direct influence of GTK rendering.
   8.183 +    The Linux-specific \<^emph>\<open>GTK+\<close> often works as well, but the overall GTK theme
   8.184 +    and options need to be selected to suite Java/AWT/Swing. Note that Java
   8.185 +    Virtual Machine has no direct influence of GTK rendering.
   8.186  
   8.187      \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
   8.188  
   8.189 @@ -342,13 +341,13 @@
   8.190      \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
   8.191  
   8.192    Users may experiment with different Swing look-and-feels, but need to keep
   8.193 -  in mind that this extra variance of GUI functionality is unlikely to work in
   8.194 -  arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close>
   8.195 -  should always work on all platforms, although they are technically and
   8.196 -  stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
   8.197 +  in mind that this extra variance of GUI functionality often causes problems.
   8.198 +  The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work on all
   8.199 +  platforms, although they are technically and stylistically outdated. The
   8.200 +  historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
   8.201  
   8.202 -  After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>,
   8.203 -  Isabelle/jEdit should be restarted to take full effect.
   8.204 +  Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the
   8.205 +  GUI only partially: proper restart of Isabelle/jEdit is usually required.
   8.206  \<close>
   8.207  
   8.208  
   8.209 @@ -357,7 +356,7 @@
   8.210  text \<open>
   8.211    In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
   8.212    pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
   8.213 -  pixels as adequate for text rendering. In 2016, we routinely see much higher
   8.214 +  pixels as adequate for text rendering. In 2017, we routinely see much higher
   8.215    resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' /
   8.216    ``4K'' at $3840 \times 2160$.
   8.217  
   8.218 @@ -720,6 +719,10 @@
   8.219      alignment of the main Isar language elements. This depends on option
   8.220      @{system_option_def "jedit_indent_newline"} (enabled by default).
   8.221  
   8.222 +    Regular input (via keyboard or completion) indents the current line
   8.223 +    whenever an new keyword is emerging at the start of the line. This depends
   8.224 +    on option @{system_option_def "jedit_indent_input"} (enabled by default).
   8.225 +
   8.226      \<^descr>[Semantic indentation] adds additional white space to unstructured proof
   8.227      scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
   8.228      of ongoing document processing and may thus lag behind, when the user is
   8.229 @@ -728,12 +731,9 @@
   8.230      "jedit_script_indent_limit"}.
   8.231  
   8.232    The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
   8.233 -  Isabelle / General\<close>.
   8.234 -
   8.235 -  \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That
   8.236 -  can be purged manually with the jEdit action @{action "remove-trailing-ws"}
   8.237 -  (shortcut \<^verbatim>\<open>C+e r\<close>). Moreover, the \<^emph>\<open>WhiteSpace\<close> plugin provides some
   8.238 -  aggressive options to trim whitespace on buffer-save.
   8.239 +  Isabelle / General\<close>. A prerequisite for advanced indentation is \<^emph>\<open>Utilities
   8.240 +  / Buffer Options / Automatic indentation\<close>: it needs to be set to \<^verbatim>\<open>full\<close>
   8.241 +  (default).
   8.242  \<close>
   8.243  
   8.244  
   8.245 @@ -820,7 +820,7 @@
   8.246      concrete syntax of the @{command_ref theory} command @{cite
   8.247      "isabelle-isar-ref"};
   8.248  
   8.249 -    \<^enum> via \<^bold>\<open>auxiliary files\<close> that are loaded into a theory by special \<^emph>\<open>load
   8.250 +    \<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>load
   8.251      commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}
   8.252      @{cite "isabelle-isar-ref"}.
   8.253  
   8.254 @@ -836,10 +836,7 @@
   8.255  text \<open>
   8.256    The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview
   8.257    of the status of continuous checking of theory nodes within the document
   8.258 -  model. Unlike batch sessions of @{tool build} @{cite "isabelle-system"},
   8.259 -  theory nodes are identified by full path names; this allows to work with
   8.260 -  multiple (disjoint) Isabelle sessions simultaneously within the same editor
   8.261 -  session.
   8.262 +  model.
   8.263  
   8.264    \begin{figure}[!htb]
   8.265    \begin{center}
   8.266 @@ -853,13 +850,13 @@
   8.267    Theory imports are resolved automatically by the PIDE document model: all
   8.268    required files are loaded and stored internally, without the need to open
   8.269    corresponding jEdit buffers. Opening or closing editor buffers later on has
   8.270 -  no impact on the formal document content: it only affects visibility.
   8.271 +  no direct impact on the formal document content: it only affects visibility.
   8.272  
   8.273 -  In contrast, auxiliary files (e.g.\ from \<^verbatim>\<open>ML_file\<close> commands) are \<^emph>\<open>not\<close>
   8.274 -  resolved within the editor by default, but the prover process takes care of
   8.275 -  that. This may be changed by enabling the system option @{system_option
   8.276 -  jedit_auto_resolve}: it ensures that all files are uniformly provided by the
   8.277 -  editor.
   8.278 +  In contrast, auxiliary files (e.g.\ from @{command ML_file} commands) are
   8.279 +  \<^emph>\<open>not\<close> resolved within the editor by default, but the prover process takes
   8.280 +  care of that. This may be changed by enabling the system option
   8.281 +  @{system_option jedit_auto_resolve}: it ensures that all files are uniformly
   8.282 +  provided by the editor.
   8.283  
   8.284    \<^medskip>
   8.285    The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective
   8.286 @@ -877,6 +874,10 @@
   8.287    visibility status (if continuous checking is enabled). Big theory libraries
   8.288    that are marked as required can have significant impact on performance!
   8.289  
   8.290 +  The \<^emph>\<open>Purge\<close> button restricts the document model to theories that are
   8.291 +  required for open editor buffers: inaccessible theories are removed and will
   8.292 +  be rechecked when opened or imported later.
   8.293 +
   8.294    \<^medskip>
   8.295    Formal markup of checked theory content is turned into GUI rendering, based
   8.296    on a standard repertoire known from mainstream IDEs for programming
   8.297 @@ -912,7 +913,9 @@
   8.298    edited conveniently in the Prover IDE on small machines with only 8\,GB of
   8.299    main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
   8.300    at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
   8.301 -  \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example.
   8.302 +  \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example. It is also possible to
   8.303 +  explore the Isabelle/Pure bootstrap process (a virtual copy) by opening
   8.304 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/ROOT.ML\<close> like a theory in the Prover IDE.
   8.305  
   8.306    Initially, before an auxiliary file is opened in the editor, the prover
   8.307    reads its content from the physical file-system. After the file is opened
   8.308 @@ -980,9 +983,11 @@
   8.309    The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but without
   8.310    direct correspondence to text positions. The coloured rectangles represent
   8.311    the amount of messages of a certain kind (warnings, errors, etc.) and the
   8.312 -  execution status of commands. A double-click on one of the theory entries
   8.313 -  with their status overview opens the corresponding text buffer, without
   8.314 -  moving the cursor to a specific point.
   8.315 +  execution status of commands. The border of each rectangle indicates the
   8.316 +  overall status of processing: a thick border means it is \<^emph>\<open>finished\<close> or
   8.317 +  \<^emph>\<open>failed\<close> (with color for errors). A double-click on one of the theory
   8.318 +  entries with their status overview opens the corresponding text buffer,
   8.319 +  without moving the cursor to a specific point.
   8.320  
   8.321    \<^medskip>
   8.322    The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given
   8.323 @@ -1877,6 +1882,16 @@
   8.324  \<close>
   8.325  
   8.326  
   8.327 +section \<open>Document preview\<close>
   8.328 +
   8.329 +text \<open>
   8.330 +  The action @{action_def isabelle.preview} opens an HTML preview of the
   8.331 +  current theory document in the default web browser. The content is derived
   8.332 +  from the semantic markup produced by the prover, and thus depends on the
   8.333 +  status of formal processing.
   8.334 +\<close>
   8.335 +
   8.336 +
   8.337  chapter \<open>ML debugging within the Prover IDE\<close>
   8.338  
   8.339  text \<open>
   8.340 @@ -2064,12 +2079,6 @@
   8.341    \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable
   8.342    continuous checking temporarily.
   8.343  
   8.344 -  \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the collection
   8.345 -  of theories.
   8.346 -
   8.347 -  \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close \<^emph>\<open>without\<close>
   8.348 -  saving changes.
   8.349 -
   8.350    \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
   8.351    editor font size depend on platform details and national keyboards.
   8.352  
   8.353 @@ -2095,15 +2104,6 @@
   8.354  
   8.355    \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
   8.356  
   8.357 -  \<^item> \<^bold>\<open>Problem:\<close> Mac OS X with Retina display has problems to determine the
   8.358 -  font metrics of \<^verbatim>\<open>IsabelleText\<close> accurately, notably in plain Swing text
   8.359 -  fields (e.g.\ in the \<^emph>\<open>Search and Replace\<close> dialog).
   8.360 -
   8.361 -  \<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system
   8.362 -  with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against
   8.363 -  that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{path
   8.364 -  "$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.
   8.365 -
   8.366    \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
   8.367    event handling of Java/AWT/Swing.
   8.368  
   8.369 @@ -2135,7 +2135,7 @@
   8.370    \<^bold>\<open>Workaround:\<close> On a 64bit platform, ensure that the JVM runs in 64bit mode,
   8.371    but the Isabelle/ML process remains in 32bit mode! Do not switch Isabelle/ML
   8.372    into 64bit mode in the expectation to be ``more efficient'' --- this
   8.373 -  requires approx.\ 32\,GB to make sense.
   8.374 +  requires 16--32\,GB to make sense.
   8.375  
   8.376    For the JVM, always use the 64bit version. That is the default on all
   8.377    platforms, except for Windows: the standard download is for win32, but there
     9.1 Binary file src/Doc/JEdit/document/output-and-state.png has changed
    10.1 Binary file src/Doc/JEdit/document/output-including-state.png has changed
    11.1 Binary file src/Doc/JEdit/document/output.png has changed
    12.1 Binary file src/Doc/JEdit/document/theories.png has changed
    13.1 --- a/src/Doc/System/Sessions.thy	Fri Sep 22 14:14:41 2017 -0300
    13.2 +++ b/src/Doc/System/Sessions.thy	Sat Sep 23 20:09:16 2017 +0200
    13.3 @@ -440,4 +440,82 @@
    13.4    @{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
    13.5  \<close>
    13.6  
    13.7 +
    13.8 +section \<open>Maintain theory imports wrt.\ session structure\<close>
    13.9 +
   13.10 +text \<open>
   13.11 +  The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
   13.12 +  session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
   13.13 +  \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
   13.14 +\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
   13.15 +
   13.16 +  Options are:
   13.17 +    -D DIR       include session directory and select its sessions
   13.18 +    -I           operation: report potential session imports
   13.19 +    -M           operation: Mercurial repository check for theory files
   13.20 +    -R           operate on requirements of selected sessions
   13.21 +    -U           operation: update theory imports to use session qualifiers
   13.22 +    -X NAME      exclude sessions from group NAME and all descendants
   13.23 +    -a           select all sessions
   13.24 +    -d DIR       include session directory
   13.25 +    -g NAME      select session group NAME
   13.26 +    -i           incremental update according to session graph structure
   13.27 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   13.28 +    -v           verbose
   13.29 +    -x NAME      exclude session NAME and all descendants
   13.30 +
   13.31 +  Maintain theory imports wrt. session structure. At least one operation
   13.32 +  needs to be specified (see options -I -M -U).\<close>}
   13.33 +
   13.34 +  \<^medskip>
   13.35 +  The selection of sessions and session directories works as for @{tool build}
   13.36 +  via options \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
   13.37 +  \secref{sec:tool-build}).
   13.38 +
   13.39 +  \<^medskip>
   13.40 +  Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
   13.41 +  (see \secref{sec:tool-build}).
   13.42 +
   13.43 +  \<^medskip>
   13.44 +  Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
   13.45 +
   13.46 +  \<^medskip>
   13.47 +  Option \<^verbatim>\<open>-I\<close> determines potential session imports, which may be turned into
   13.48 +  \isakeyword{sessions} within the corresponding \<^verbatim>\<open>ROOT\<close> file entry. Thus
   13.49 +  theory imports from other sessions may use session-qualified names. For
   13.50 +  example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> may become formal
   13.51 +  \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
   13.52 +  \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
   13.53 +
   13.54 +  \<^medskip>
   13.55 +  Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
   13.56 +  the underlying session directories; non-repository directories are ignored.
   13.57 +  This helps to find files that are accidentally ignored, e.g.\ due to
   13.58 +  rearrangements of the session structure.
   13.59 +
   13.60 +  \<^medskip>
   13.61 +  Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
   13.62 +  to canonical session-qualified theory names, according to the theory name
   13.63 +  space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
   13.64 +
   13.65 +  Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
   13.66 +  following to the session graph structure in bottom-up order. This may
   13.67 +  lead to more accurate results in complex session hierarchies.
   13.68 +\<close>
   13.69 +
   13.70 +subsubsection \<open>Examples\<close>
   13.71 +
   13.72 +text \<open>
   13.73 +  Determine potential session imports for some project directory:
   13.74 +  @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
   13.75 +
   13.76 +  \<^smallskip>
   13.77 +  Mercurial repository check for some project directory:
   13.78 +  @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
   13.79 +
   13.80 +  \<^smallskip>
   13.81 +  Incremental update of theory imports for some project directory:
   13.82 +  @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
   13.83 +\<close>
   13.84 +
   13.85  end
    14.1 --- a/src/Doc/antiquote_setup.ML	Fri Sep 22 14:14:41 2017 -0300
    14.2 +++ b/src/Doc/antiquote_setup.ML	Sat Sep 23 20:09:16 2017 +0200
    14.3 @@ -177,7 +177,8 @@
    14.4              NONE => ""
    14.5            | SOME is_def =>
    14.6                "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
    14.7 -        val _ = check ctxt (name, pos);
    14.8 +        val _ =
    14.9 +          if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
   14.10        in
   14.11          idx ^
   14.12          (Output.output name
    15.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Fri Sep 22 14:14:41 2017 -0300
    15.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Sat Sep 23 20:09:16 2017 +0200
    15.3 @@ -10,7 +10,7 @@
    15.4    "HOL-Library.Discrete"
    15.5    "HOL-Library.Extended_Real"
    15.6    "HOL-Library.Liminf_Limsup"
    15.7 -  "Extended_Real_Limits"
    15.8 +  Extended_Real_Limits
    15.9  begin
   15.10  
   15.11  text \<open>
    16.1 --- a/src/HOL/Data_Structures/Base_FDS.thy	Fri Sep 22 14:14:41 2017 -0300
    16.2 +++ b/src/HOL/Data_Structures/Base_FDS.thy	Sat Sep 23 20:09:16 2017 +0200
    16.3 @@ -1,5 +1,5 @@
    16.4  theory Base_FDS
    16.5 -imports "../Library/Pattern_Aliases"
    16.6 +imports "HOL-Library.Pattern_Aliases"
    16.7  begin
    16.8  
    16.9  declare Let_def [simp]
    17.1 --- a/src/Pure/PIDE/protocol.scala	Fri Sep 22 14:14:41 2017 -0300
    17.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Sep 23 20:09:16 2017 +0200
    17.3 @@ -316,11 +316,14 @@
    17.4      Symbol.encode_yxml(list(pair(string, string))(table))
    17.5    }
    17.6  
    17.7 -  def session_base(resources: Resources): Unit =
    17.8 +  def session_base(resources: Resources)
    17.9 +  {
   17.10 +    val base = resources.session_base.standard_path
   17.11      protocol_command("Prover.session_base",
   17.12 -      encode_table(resources.session_base.global_theories.toList),
   17.13 -      encode_table(resources.session_base.loaded_theories.toList),
   17.14 -      encode_table(resources.session_base.dest_known_theories))
   17.15 +      encode_table(base.global_theories.toList),
   17.16 +      encode_table(base.loaded_theories.toList),
   17.17 +      encode_table(base.dest_known_theories))
   17.18 +  }
   17.19  
   17.20  
   17.21    /* interned items */
    18.1 --- a/src/Pure/System/isabelle_system.ML	Fri Sep 22 14:14:41 2017 -0300
    18.2 +++ b/src/Pure/System/isabelle_system.ML	Sat Sep 23 20:09:16 2017 +0200
    18.3 @@ -6,6 +6,7 @@
    18.4  
    18.5  signature ISABELLE_SYSTEM =
    18.6  sig
    18.7 +  val rm_tree: Path.T -> unit
    18.8    val mkdirs: Path.T -> unit
    18.9    val mkdir: Path.T -> unit
   18.10    val copy_dir: Path.T -> Path.T -> unit
    19.1 --- a/src/Pure/System/options.scala	Fri Sep 22 14:14:41 2017 -0300
    19.2 +++ b/src/Pure/System/options.scala	Sat Sep 23 20:09:16 2017 +0200
    19.3 @@ -147,7 +147,7 @@
    19.4  
    19.5    /* Isabelle tool wrapper */
    19.6  
    19.7 -  val isabelle_tool = Isabelle_Tool("option", "print Isabelle system options", args =>
    19.8 +  val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options", args =>
    19.9    {
   19.10      var build_options = false
   19.11      var get_option = ""
    20.1 --- a/src/Pure/Thy/present.ML	Fri Sep 22 14:14:41 2017 -0300
    20.2 +++ b/src/Pure/Thy/present.ML	Sat Sep 23 20:09:16 2017 +0200
    20.3 @@ -196,7 +196,7 @@
    20.4  
    20.5  fun isabelle_document {verbose, purge} format name tags dir =
    20.6    let
    20.7 -    val s = "isabelle document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
    20.8 +    val s = "isabelle document -o '" ^ format ^ "' \
    20.9        \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
   20.10      val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
   20.11      val _ = if verbose then writeln s else ();
   20.12 @@ -206,6 +206,7 @@
   20.13          cat_error out ("Failed to build document " ^ quote (show_path doc_path))
   20.14        else if verbose then writeln out
   20.15        else ();
   20.16 +    val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
   20.17    in doc_path end;
   20.18  
   20.19  
    21.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 22 14:14:41 2017 -0300
    21.2 +++ b/src/Pure/Thy/sessions.scala	Sat Sep 23 20:09:16 2017 +0200
    21.3 @@ -81,6 +81,11 @@
    21.4          theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
    21.5          files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
    21.6  
    21.7 +    def standard_path: Known =
    21.8 +      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))),
    21.9 +        theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
   21.10 +        files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
   21.11 +
   21.12      def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
   21.13      {
   21.14        val res = files.getOrElse(File.canonical(file), Nil).headOption
   21.15 @@ -114,6 +119,7 @@
   21.16      def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
   21.17  
   21.18      def platform_path: Base = copy(known = known.platform_path)
   21.19 +    def standard_path: Base = copy(known = known.standard_path)
   21.20  
   21.21      def loaded_theory(name: Document.Node.Name): Boolean =
   21.22        loaded_theories.isDefinedAt(name.theory)
    22.1 --- a/src/Pure/Tools/build.scala	Fri Sep 22 14:14:41 2017 -0300
    22.2 +++ b/src/Pure/Tools/build.scala	Sat Sep 23 20:09:16 2017 +0200
    22.3 @@ -455,9 +455,6 @@
    22.4              //{{{ finish job
    22.5  
    22.6              val process_result = job.join
    22.7 -            process_result.err_lines.foreach(progress.echo(_))
    22.8 -            if (process_result.ok)
    22.9 -              progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   22.10  
   22.11              val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   22.12              val process_result_tail =
   22.13 @@ -469,6 +466,8 @@
   22.14                    (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   22.15              }
   22.16  
   22.17 +
   22.18 +            // write log file
   22.19              val heap_stamp =
   22.20                if (process_result.ok) {
   22.21                  (store.output_dir + store.log(name)).file.delete
   22.22 @@ -485,8 +484,6 @@
   22.23                  (store.output_dir + store.log_gz(name)).file.delete
   22.24  
   22.25                  File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
   22.26 -                progress.echo(name + " FAILED")
   22.27 -                if (!process_result.interrupted) progress.echo(process_result_tail.out)
   22.28  
   22.29                  None
   22.30                }
   22.31 @@ -506,6 +503,16 @@
   22.32                      Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
   22.33              }
   22.34  
   22.35 +            // messages
   22.36 +            process_result.err_lines.foreach(progress.echo(_))
   22.37 +
   22.38 +            if (process_result.ok)
   22.39 +              progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   22.40 +            else {
   22.41 +              progress.echo(name + " FAILED")
   22.42 +              if (!process_result.interrupted) progress.echo(process_result_tail.out)
   22.43 +            }
   22.44 +
   22.45              loop(pending - name, running - name,
   22.46                results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   22.47              //}}}
    23.1 --- a/src/Pure/Tools/imports.scala	Fri Sep 22 14:14:41 2017 -0300
    23.2 +++ b/src/Pure/Tools/imports.scala	Sat Sep 23 20:09:16 2017 +0200
    23.3 @@ -119,7 +119,7 @@
    23.4      }
    23.5  
    23.6      if (operation_repository_files) {
    23.7 -      progress.echo("\nMercurial files check:")
    23.8 +      progress.echo("\nMercurial repository check:")
    23.9        val unused_files =
   23.10          for {
   23.11            (_, dir) <- Sessions.directories(dirs, select_dirs)
   23.12 @@ -235,7 +235,7 @@
   23.13    Options are:
   23.14      -D DIR       include session directory and select its sessions
   23.15      -I           operation: report potential session imports
   23.16 -    -M           operation: Mercurial files check for imported theory files
   23.17 +    -M           operation: Mercurial repository check for theory files
   23.18      -R           operate on requirements of selected sessions
   23.19      -U           operation: update theory imports to use session qualifiers
   23.20      -X NAME      exclude sessions from group NAME and all descendants
    24.1 --- a/src/Pure/Tools/jedit.ML	Fri Sep 22 14:14:41 2017 -0300
    24.2 +++ b/src/Pure/Tools/jedit.ML	Sat Sep 23 20:09:16 2017 +0200
    24.3 @@ -32,7 +32,8 @@
    24.4    Lazy.lazy (fn () =>
    24.5      (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) of
    24.6        XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
    24.7 -    | _ => []));
    24.8 +    | _ => [])
    24.9 +    |> maps (fn a => [a, a ^ "-toggle", a ^ "-float"]));
   24.10  
   24.11  val jedit_actions =
   24.12    Lazy.lazy (fn () =>
    25.1 --- a/src/Tools/VSCode/extension/package.json	Fri Sep 22 14:14:41 2017 -0300
    25.2 +++ b/src/Tools/VSCode/extension/package.json	Sat Sep 23 20:09:16 2017 +0200
    25.3 @@ -10,7 +10,7 @@
    25.4          "document preparation"
    25.5      ],
    25.6      "icon": "isabelle.png",
    25.7 -    "version": "0.23.0",
    25.8 +    "version": "1.0.0",
    25.9      "publisher": "makarius",
   25.10      "license": "MIT",
   25.11      "repository": {
   25.12 @@ -492,9 +492,9 @@
   25.13          "postinstall": "node ./node_modules/vscode/bin/install"
   25.14      },
   25.15      "devDependencies": {
   25.16 -        "@types/mocha": "^2.2.42",
   25.17 +        "@types/mocha": "^2.2.43",
   25.18          "@types/node": "^7.0.43",
   25.19 -        "mocha": "^3.5.0",
   25.20 +        "mocha": "^3.5.3",
   25.21          "typescript": "^2.5.2",
   25.22          "vscode": "^1.1.5"
   25.23      },
    26.1 --- a/src/Tools/VSCode/src/document_model.scala	Fri Sep 22 14:14:41 2017 -0300
    26.2 +++ b/src/Tools/VSCode/src/document_model.scala	Sat Sep 23 20:09:16 2017 +0200
    26.3 @@ -45,6 +45,16 @@
    26.4      lazy val bibtex_entries: List[Text.Info[String]] =
    26.5        try { Bibtex.entries(text) }
    26.6        catch { case ERROR(_) => Nil }
    26.7 +
    26.8 +    def recode_symbols: List[Protocol.TextEdit] =
    26.9 +      (for {
   26.10 +        (line, l) <- doc.lines.iterator.zipWithIndex
   26.11 +        text1 = Symbol.encode(line.text)
   26.12 +        if (line.text != text1)
   26.13 +      } yield {
   26.14 +        val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length))
   26.15 +        Protocol.TextEdit(range, text1)
   26.16 +      }).toList
   26.17    }
   26.18  
   26.19    def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
   26.20 @@ -56,6 +66,7 @@
   26.21    editor: Server.Editor,
   26.22    node_name: Document.Node.Name,
   26.23    content: Document_Model.Content,
   26.24 +  version: Option[Long] = None,
   26.25    external_file: Boolean = false,
   26.26    node_required: Boolean = false,
   26.27    last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
   26.28 @@ -66,10 +77,12 @@
   26.29    model =>
   26.30  
   26.31  
   26.32 -  /* text */
   26.33 +  /* content */
   26.34  
   26.35    def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
   26.36  
   26.37 +  def set_version(new_version: Long): Document_Model = copy(version = Some(new_version))
   26.38 +
   26.39  
   26.40    /* external file */
   26.41  
   26.42 @@ -163,12 +176,27 @@
   26.43      }
   26.44    }
   26.45  
   26.46 -  def flush_edits(doc_blobs: Document.Blobs, caret: Option[Line.Position])
   26.47 -    : Option[(List[Document.Edit_Text], Document_Model)] =
   26.48 +  def flush_edits(
   26.49 +      unicode_symbols: Boolean,
   26.50 +      doc_blobs: Document.Blobs,
   26.51 +      file: JFile,
   26.52 +      caret: Option[Line.Position])
   26.53 +    : Option[((List[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] =
   26.54    {
   26.55 +    val workspace_edits =
   26.56 +      if (unicode_symbols && version.isDefined) {
   26.57 +        val edits = content.recode_symbols
   26.58 +        if (edits.nonEmpty) List(Protocol.TextDocumentEdit(file, version.get, edits))
   26.59 +        else Nil
   26.60 +      }
   26.61 +      else Nil
   26.62 +
   26.63      val (reparse, perspective) = node_perspective(doc_blobs, caret)
   26.64 -    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
   26.65 -      val edits = node_edits(node_header, pending_edits, perspective)
   26.66 +    if (reparse || pending_edits.nonEmpty || last_perspective != perspective ||
   26.67 +        workspace_edits.nonEmpty)
   26.68 +    {
   26.69 +      val prover_edits = node_edits(node_header, pending_edits, perspective)
   26.70 +      val edits = (workspace_edits, prover_edits)
   26.71        Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
   26.72      }
   26.73      else None
    27.1 --- a/src/Tools/VSCode/src/protocol.scala	Fri Sep 22 14:14:41 2017 -0300
    27.2 +++ b/src/Tools/VSCode/src/protocol.scala	Sat Sep 23 20:09:16 2017 +0200
    27.3 @@ -62,6 +62,11 @@
    27.4  
    27.5    /* request message */
    27.6  
    27.7 +  object Id
    27.8 +  {
    27.9 +    def empty: Id = Id("")
   27.10 +  }
   27.11 +
   27.12    sealed case class Id(id: Any)
   27.13    {
   27.14      require(
   27.15 @@ -118,6 +123,9 @@
   27.16      def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
   27.17        if (error == "") apply(id, result = result)
   27.18        else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
   27.19 +
   27.20 +    def is_empty(json: JSON.T): Boolean =
   27.21 +      JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined
   27.22    }
   27.23  
   27.24    sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
   27.25 @@ -324,6 +332,28 @@
   27.26    object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
   27.27  
   27.28  
   27.29 +  /* workspace edits */
   27.30 +
   27.31 +  sealed case class TextEdit(range: Line.Range, new_text: String)
   27.32 +  {
   27.33 +    def json: JSON.T = Map("range" -> Range(range), "newText" -> new_text)
   27.34 +  }
   27.35 +
   27.36 +  sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit])
   27.37 +  {
   27.38 +    def json: JSON.T =
   27.39 +      Map("textDocument" -> Map("uri" -> Url.print_file(file), "version" -> version),
   27.40 +        "edits" -> edits.map(_.json))
   27.41 +  }
   27.42 +
   27.43 +  object WorkspaceEdit
   27.44 +  {
   27.45 +    def apply(edits: List[TextDocumentEdit]): JSON.T =
   27.46 +      RequestMessage(Id.empty, "workspace/applyEdit",
   27.47 +        Map("edit" -> Map("documentChanges" -> edits.map(_.json))))
   27.48 +  }
   27.49 +
   27.50 +
   27.51    /* completion */
   27.52  
   27.53    sealed case class CompletionItem(
   27.54 @@ -342,8 +372,7 @@
   27.55        JSON.optional("documentation" -> documentation) ++
   27.56        JSON.optional("insertText" -> text) ++
   27.57        JSON.optional("range" -> range.map(Range(_))) ++
   27.58 -      JSON.optional("textEdit" ->
   27.59 -        range.map(r => Map("range" -> Range(r), "newText" -> text.getOrElse(label)))) ++
   27.60 +      JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++
   27.61        JSON.optional("command" -> command.map(_.json))
   27.62    }
   27.63  
    28.1 --- a/src/Tools/VSCode/src/server.scala	Fri Sep 22 14:14:41 2017 -0300
    28.2 +++ b/src/Tools/VSCode/src/server.scala	Sat Sep 23 20:09:16 2017 +0200
    28.3 @@ -123,7 +123,7 @@
    28.4  
    28.5    private val delay_input: Standard_Thread.Delay =
    28.6      Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
    28.7 -    { resources.flush_input(session) }
    28.8 +    { resources.flush_input(session, channel) }
    28.9  
   28.10    private val delay_load: Standard_Thread.Delay =
   28.11      Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
   28.12 @@ -153,7 +153,7 @@
   28.13      delay_output.invoke()
   28.14    }
   28.15  
   28.16 -  private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
   28.17 +  private def change_document(file: JFile, version: Long, changes: List[Protocol.TextDocumentChange])
   28.18    {
   28.19      val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange]
   28.20      @tailrec def norm(chs: List[Protocol.TextDocumentChange])
   28.21 @@ -168,7 +168,7 @@
   28.22      }
   28.23      norm(changes)
   28.24      norm_changes.foreach(change =>
   28.25 -      resources.change_model(session, editor, file, change.text, change.range))
   28.26 +      resources.change_model(session, editor, file, version, change.text, change.range))
   28.27  
   28.28      delay_input.invoke()
   28.29      delay_output.invoke()
   28.30 @@ -326,8 +326,8 @@
   28.31          delay_caret_update.revoke()
   28.32          delay_preview.revoke()
   28.33  
   28.34 -        val rc = session.stop()
   28.35 -        if (rc == 0) reply("") else reply("Prover shutdown failed: return code " + rc)
   28.36 +        val result = session.stop()
   28.37 +        if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc)
   28.38          None
   28.39        case None =>
   28.40          reply("Prover inactive")
   28.41 @@ -436,9 +436,10 @@
   28.42            case Protocol.Initialized(()) =>
   28.43            case Protocol.Shutdown(id) => shutdown(id)
   28.44            case Protocol.Exit(()) => exit()
   28.45 -          case Protocol.DidOpenTextDocument(file, _, _, text) =>
   28.46 -            change_document(file, List(Protocol.TextDocumentChange(None, text)))
   28.47 -          case Protocol.DidChangeTextDocument(file, _, changes) => change_document(file, changes)
   28.48 +          case Protocol.DidOpenTextDocument(file, _, version, text) =>
   28.49 +            change_document(file, version, List(Protocol.TextDocumentChange(None, text)))
   28.50 +          case Protocol.DidChangeTextDocument(file, version, changes) =>
   28.51 +            change_document(file, version, changes)
   28.52            case Protocol.DidCloseTextDocument(file) => close_document(file)
   28.53            case Protocol.Completion(id, node_pos) => completion(id, node_pos)
   28.54            case Protocol.Include_Word(()) => update_dictionary(true, false)
   28.55 @@ -457,7 +458,7 @@
   28.56            case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
   28.57            case Protocol.Preview_Request(file, column) => request_preview(file, column)
   28.58            case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
   28.59 -          case _ => log("### IGNORED")
   28.60 +          case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED")
   28.61          }
   28.62        }
   28.63        catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
   28.64 @@ -486,7 +487,7 @@
   28.65      /* session */
   28.66  
   28.67      override def session: Session = server.session
   28.68 -    override def flush(): Unit = resources.flush_input(session)
   28.69 +    override def flush(): Unit = resources.flush_input(session, channel)
   28.70      override def invoke(): Unit = delay_input.invoke()
   28.71  
   28.72  
    29.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 22 14:14:41 2017 -0300
    29.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Sep 23 20:09:16 2017 +0200
    29.3 @@ -155,13 +155,15 @@
    29.4      session: Session,
    29.5      editor: Server.Editor,
    29.6      file: JFile,
    29.7 +    version: Long,
    29.8      text: String,
    29.9      range: Option[Line.Range] = None)
   29.10    {
   29.11      state.change(st =>
   29.12        {
   29.13          val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
   29.14 -        val model1 = (model.change_text(text, range) getOrElse model).external(false)
   29.15 +        val model1 =
   29.16 +          (model.change_text(text, range) getOrElse model).set_version(version).external(false)
   29.17          st.update_models(Some(file -> model1))
   29.18        })
   29.19    }
   29.20 @@ -256,7 +258,7 @@
   29.21  
   29.22    /* pending input */
   29.23  
   29.24 -  def flush_input(session: Session)
   29.25 +  def flush_input(session: Session, channel: Channel)
   29.26    {
   29.27      state.change(st =>
   29.28        {
   29.29 @@ -264,10 +266,15 @@
   29.30            (for {
   29.31              file <- st.pending_input.iterator
   29.32              model <- st.models.get(file)
   29.33 -            (edits, model1) <- model.flush_edits(st.document_blobs, st.get_caret(file))
   29.34 +            (edits, model1) <-
   29.35 +              model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
   29.36            } yield (edits, (file, model1))).toList
   29.37  
   29.38 -        session.update(st.document_blobs, changed_models.flatMap(_._1))
   29.39 +        for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
   29.40 +          channel.write(Protocol.WorkspaceEdit(workspace_edits))
   29.41 +
   29.42 +        session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
   29.43 +
   29.44          st.copy(
   29.45            models = st.models ++ changed_models.iterator.map(_._2),
   29.46            pending_input = Set.empty)
    30.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 22 14:14:41 2017 -0300
    30.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Sep 23 20:09:16 2017 +0200
    30.3 @@ -110,13 +110,14 @@
    30.4    echo
    30.5    echo "  Options are:"
    30.6    echo "    -D NAME=X    set JVM system property"
    30.7 -  echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
    30.8 +  echo "    -J OPTION    add JVM runtime option"
    30.9 +  echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
   30.10    echo "    -R           open ROOT entry of logic session and use its parent"
   30.11    echo "    -b           build only"
   30.12    echo "    -d DIR       include session directory"
   30.13    echo "    -f           fresh build"
   30.14    echo "    -j OPTION    add jEdit runtime option"
   30.15 -  echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
   30.16 +  echo "                 (default $JEDIT_OPTIONS)"
   30.17    echo "    -l NAME      logic session name"
   30.18    echo "    -m MODE      add print mode for output"
   30.19    echo "    -n           no build of session image on startup"