--- a/.hgtags Fri Sep 22 14:14:41 2017 -0300
+++ b/.hgtags Sat Sep 23 20:09:16 2017 +0200
@@ -36,3 +36,4 @@
a5dd01b682189f5412460b78b9611f7665b26894 Isabelle2017-RC0
34b20f7236ea2b59c1994ee10770267bb156c9e5 Isabelle2017-RC1
e9d8ff531700c7c19ea6f9c1315c06015f95d2b8 Isabelle2017-RC2
+4f73201b8043b92783824b55dcded6891de0a41e Isabelle2017-RC3
--- a/Admin/components/components.sha1 Fri Sep 22 14:14:41 2017 -0300
+++ b/Admin/components/components.sha1 Sat Sep 23 20:09:16 2017 +0200
@@ -6,6 +6,8 @@
70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz
2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
d70bfbe63590153c07709dea7084fbc39c669841 cvc4-1.5-1.tar.gz
+541eac340464c5d34b70bb163ae277cc8829c40f cvc4-1.5-2.tar.gz
+1a44895d2a440091a15cc92d7f77a06a2e432507 cvc4-1.5-3.tar.gz
a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz
4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz
b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz
@@ -36,6 +38,7 @@
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz
c11b25c919e2ec44fe2b6ac2086337b456344e97 e-1.8.tar.gz
+a895a96ec7e6fcc275114bb9b4c92b20fac73dba e-2.0-1.tar.gz
6b962a6b4539b7ca4199977973c61a8c98a492e8 e-2.0.tar.gz
6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
--- a/Admin/components/main Fri Sep 22 14:14:41 2017 -0300
+++ b/Admin/components/main Sat Sep 23 20:09:16 2017 +0200
@@ -1,8 +1,8 @@
#main components for everyday use, without big impact on overall build time
bash_process-1.2.1
csdp-6.x
-cvc4-1.5-1
-e-2.0
+cvc4-1.5-3
+e-2.0-1
isabelle_fonts-20160830
jdk-8u144
jedit_build-20170319
--- a/NEWS Fri Sep 22 14:14:41 2017 -0300
+++ b/NEWS Sat Sep 23 20:09:16 2017 +0200
@@ -126,7 +126,7 @@
* Deleting the last code equations for a particular function using
[code del] results in function with no equations (runtime abort) rather
than an unimplemented function (generation time abort). Use explicit
-[[code drop:]] to enforce the latter. Minor INCOMPATIBILTIY.
+[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
* Proper concept of code declarations in code.ML:
- Regular code declarations act only on the global theory level, being
@@ -316,7 +316,7 @@
serves as example for alternative PIDE front-ends.
* Command-line tool "isabelle imports" helps to maintain theory imports
-wrt. session structure. Examples:
+wrt. session structure. Examples for the main Isabelle distribution:
isabelle imports -I -a
isabelle imports -U -a
--- a/lib/scripts/getfunctions Fri Sep 22 14:14:41 2017 -0300
+++ b/lib/scripts/getfunctions Sat Sep 23 20:09:16 2017 +0200
@@ -70,6 +70,7 @@
#classpath
function classpath ()
{
+ local X=""
for X in "$@"
do
if [ -z "$ISABELLE_CLASSPATH" ]; then
@@ -98,6 +99,7 @@
{
SPLITARRAY=()
local IFS="$1"; shift
+ local X=""
for X in $*
do
SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
@@ -149,6 +151,7 @@
#init component forest
function init_components ()
{
+ local REPLY=""
local BASE="$1"
local CATALOG="$2"
local COMPONENT=""
--- a/src/Doc/Implementation/ML.thy Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Doc/Implementation/ML.thy Sat Sep 23 20:09:16 2017 +0200
@@ -946,9 +946,9 @@
Another benefit of @{ML add_content} is its ``open'' form as a function on
buffers that can be continued in further linear transformations, folding
etc. Thus it is more compositional than the naive @{ML slow_content}. As
- realistic example, compare the old-style @{ML "Term.maxidx_of_term: term ->
- int"} with the newer @{ML "Term.maxidx_term: term -> int -> int"} in
- Isabelle/Pure.
+ realistic example, compare the old-style
+ @{ML "Term.maxidx_of_term: term -> int"} with the newer @{ML
+ "Term.maxidx_term: term -> int -> int"} in Isabelle/Pure.
Note that @{ML fast_content} above is only defined as example. In many
practical situations, it is customary to provide the incremental @{ML
@@ -1851,18 +1851,18 @@
evaluation via promises, evaluation with time limit etc.
\<^medskip>
- An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction \<^verbatim>\<open>fn
- () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of type
- \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required to
- tell them apart --- the static type-system of SML is only of limited help
+ An \<^emph>\<open>unevaluated expression\<close> is represented either as unit abstraction
+ \<^verbatim>\<open>fn () => a\<close> of type \<^verbatim>\<open>unit -> 'a\<close> or as regular function \<^verbatim>\<open>fn a => b\<close> of
+ type \<^verbatim>\<open>'a -> 'b\<close>. Both forms occur routinely, and special care is required
+ to tell them apart --- the static type-system of SML is only of limited help
here.
- The first form is more intuitive: some combinator \<open>(unit -> 'a) -> 'a\<close>
- applies the given function to \<open>()\<close> to initiate the postponed evaluation
- process. The second form is more flexible: some combinator \<open>('a -> 'b) -> 'a
- -> 'b\<close> acts like a modified form of function application; several such
- combinators may be cascaded to modify a given function, before it is
- ultimately applied to some argument.
+ The first form is more intuitive: some combinator \<^verbatim>\<open>(unit -> 'a) -> 'a\<close>
+ applies the given function to \<^verbatim>\<open>()\<close> to initiate the postponed evaluation
+ process. The second form is more flexible: some combinator
+ \<^verbatim>\<open>('a -> 'b) -> 'a -> 'b\<close> acts like a modified form of function application;
+ several such combinators may be cascaded to modify a given function, before
+ it is ultimately applied to some argument.
\<^medskip>
\<^emph>\<open>Reified results\<close> make the disjoint sum of regular values versions
--- a/src/Doc/Implementation/Proof.thy Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Doc/Implementation/Proof.thy Sat Sep 23 20:09:16 2017 +0200
@@ -101,7 +101,8 @@
@{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
@{index_ML Variable.import: "bool -> thm list -> Proof.context ->
- ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\
+ ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list)
+ * Proof.context"} \\
@{index_ML Variable.focus: "binding list option -> term -> Proof.context ->
((string * (string * typ)) list * term) * Proof.context"} \\
\end{mldecls}
--- a/src/Doc/JEdit/JEdit.thy Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Doc/JEdit/JEdit.thy Sat Sep 23 20:09:16 2017 +0200
@@ -26,9 +26,9 @@
\<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It
extends the pure logical environment of Isabelle/ML towards the outer
world of graphical user interfaces, text editors, IDE frameworks, web
- services etc. Special infrastructure allows to transfer algebraic
- datatypes and formatted text easily between ML and Scala, using
- asynchronous protocol commands.
+ services, SSH servers, SQL databases etc. Special infrastructure allows to
+ transfer algebraic datatypes and formatted text easily between ML and
+ Scala, using asynchronous protocol commands.
\<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It
is built around a concept of parallel and asynchronous document
@@ -79,14 +79,14 @@
The options allow to specify a logic session name, but the same selector is
also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After
- application startup, the selected logic session image is provided
+ startup of the Isabelle plugin, the selected logic session image is provided
automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
- absent or outdated wrt.\ its sources, the build process updates it while the
- text editor is running. Prover IDE functionality is only activated after
+ absent or outdated wrt.\ its sources, the build process updates it within
+ the running text editor. Prover IDE functionality is fully activated after
successful termination of the build process. A failure may require changing
- some options and restart the application. Changing the logic session, or the
- underlying ML system platform (32\,bit versus 64\,bit) requires a restart of
- the application to take effect.
+ some options and restart of the Isabelle plugin or application. Changing the
+ logic session, or the underlying ML system platform (32\,bit versus 64\,bit)
+ requires a restart of the whole application to take effect.
\<^medskip>
The main job of the Prover IDE is to manage sources and their changes,
@@ -122,7 +122,7 @@
individual plugins.
Most of the information about jEdit is relevant for Isabelle/jEdit as well,
- but one needs to keep in mind that defaults sometimes differ, and the
+ but users need to keep in mind that defaults sometimes differ, and the
official jEdit documentation does not know about the Isabelle plugin with
its support for continuous checking of formal source text: jEdit is a plain
text editor, but Isabelle/jEdit is a Prover IDE.
@@ -144,16 +144,17 @@
sense how it is meant to work, before loading too many other plugins.
\<^medskip>
- The \<^emph>\<open>Isabelle\<close> plugin provides the main Prover IDE functionality of
- Isabelle/jEdit: it manages the prover session in the background. A few
+ The \<^emph>\<open>Isabelle\<close> plugin is responsible for the main Prover IDE functionality
+ of Isabelle/jEdit: it manages the prover session in the background. A few
additional plugins are bundled with Isabelle/jEdit for convenience or out of
- necessity, notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin
+ necessity, notably \<^emph>\<open>Console\<close> with its \<^emph>\<open>Scala\<close> sub-plugin
(\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
parsers for document tree structure (\secref{sec:sidekick}). The
\<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
(e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
- of bundled plugins, but have no particular use in Isabelle/jEdit. \<close>
+ of bundled plugins, but have no particular use in Isabelle/jEdit.
+\<close>
subsection \<open>Options \label{sec:options}\<close>
@@ -174,11 +175,11 @@
Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable in
Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there
- are various options for rendering of document content, which are
- configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin
- Options~/ Isabelle\<close> in jEdit provides a view on a subset of Isabelle system
- options. Note that some of these options affect general parameters that are
- relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
+ are various options for rendering document content, which are configurable
+ via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin Options~/
+ Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options.
+ Note that some of these options affect general parameters that are relevant
+ outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
@{system_option parallel_proofs} for the Isabelle build tool @{cite
"isabelle-system"}, but it is possible to use the settings variable
@{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds
@@ -189,10 +190,9 @@
\<^medskip>
Options are usually loaded on startup and saved on shutdown of
- Isabelle/jEdit. Editing the machine-generated @{path
- "$JEDIT_SETTINGS/properties"} or @{path
- "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
- running is likely to cause surprise due to lost update!
+ Isabelle/jEdit. Editing the generated @{path "$JEDIT_SETTINGS/properties"}
+ or @{path "$ISABELLE_HOME_USER/etc/preferences"} manually while the
+ application is running may cause surprise due to lost updates!
\<close>
@@ -205,14 +205,12 @@
first start of the editor; afterwards the keymap file takes precedence and
is no longer affected by change of default properties.
- Users may change their keymap later, but need to keep its content @{path
- "$JEDIT_SETTINGS/keymaps"} in sync with \<^verbatim>\<open>shortcut\<close> properties in
- \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
+ Users may change their keymap later, but this may lead to conflicts with
+ \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
- \<^medskip>
The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
Isabelle keymap changes that are in conflict with the current jEdit keymap;
- non-conflicting changes are always applied implicitly. This action is
+ while non-conflicting changes are applied implicitly. This action is
automatically invoked on Isabelle/jEdit startup.
\<close>
@@ -232,11 +230,13 @@
Options are:
-D NAME=X set JVM system property
-J OPTION add JVM runtime option
+ (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
-R open ROOT entry of logic session and use its parent
-b build only
-d DIR include session directory
-f fresh build
-j OPTION add jEdit runtime option
+ (default $JEDIT_OPTIONS)
-l NAME logic image name
-m MODE add print mode for output
-n no build of session image on startup
@@ -248,8 +248,8 @@
The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used
for proof processing. Additional session root directories may be included
- via option \<^verbatim>\<open>-d\<close> to augment that name space of @{tool build} @{cite
- "isabelle-system"}.
+ via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
+ "isabelle-system"}).
By default, the specified image is checked and built on demand. The \<^verbatim>\<open>-s\<close>
option determines where to store the result session image of @{tool build}.
@@ -266,11 +266,10 @@
do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
Isabelle/jEdit), without requiring command-line invocation.
- The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options allow to pass additional low-level options to
- the JVM or jEdit, respectively. The defaults are provided by the Isabelle
- settings environment @{cite "isabelle-system"}, but note that these only
- work for the command-line tool described here, and not the regular
- application.
+ The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or
+ jEdit, respectively. The defaults are provided by the Isabelle settings
+ environment @{cite "isabelle-system"}, but note that these only work for the
+ command-line tool described here, and not the regular application.
The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
directly to the underlying \<^verbatim>\<open>java\<close> process.
@@ -299,7 +298,7 @@
The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
different server name. The default server name is the official distribution
- name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<close>). Thus @{tool jedit_client} can connect to the
+ name (e.g.\ \<^verbatim>\<open>Isabelle2017\<close>). Thus @{tool jedit_client} can connect to the
Isabelle desktop application without further options.
The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
@@ -317,7 +316,7 @@
subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close>
text \<open>
- jEdit is a Java/AWT/Swing application with some ambition to support
+ jEdit is a Java/AWT/Swing application with the ambition to support
``native'' look-and-feel on all platforms, within the limits of what Oracle
as Java provider and major operating system distributors allow (see also
\secref{sec:problems}).
@@ -327,9 +326,9 @@
\<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.
- The Linux-specific \<^emph>\<open>GTK+\<close> also works under the side-condition that the
- overall GTK theme and options are selected in a way that works with Java
- AWT/Swing. The JVM has no direct influence of GTK rendering.
+ The Linux-specific \<^emph>\<open>GTK+\<close> often works as well, but the overall GTK theme
+ and options need to be selected to suite Java/AWT/Swing. Note that Java
+ Virtual Machine has no direct influence of GTK rendering.
\<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
@@ -342,13 +341,13 @@
\<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
Users may experiment with different Swing look-and-feels, but need to keep
- in mind that this extra variance of GUI functionality is unlikely to work in
- arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close>
- should always work on all platforms, although they are technically and
- stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
+ in mind that this extra variance of GUI functionality often causes problems.
+ The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work on all
+ platforms, although they are technically and stylistically outdated. The
+ historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
- After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>,
- Isabelle/jEdit should be restarted to take full effect.
+ Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the
+ GUI only partially: proper restart of Isabelle/jEdit is usually required.
\<close>
@@ -357,7 +356,7 @@
text \<open>
In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
- pixels as adequate for text rendering. In 2016, we routinely see much higher
+ pixels as adequate for text rendering. In 2017, we routinely see much higher
resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' /
``4K'' at $3840 \times 2160$.
@@ -720,6 +719,10 @@
alignment of the main Isar language elements. This depends on option
@{system_option_def "jedit_indent_newline"} (enabled by default).
+ Regular input (via keyboard or completion) indents the current line
+ whenever an new keyword is emerging at the start of the line. This depends
+ on option @{system_option_def "jedit_indent_input"} (enabled by default).
+
\<^descr>[Semantic indentation] adds additional white space to unstructured proof
scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
of ongoing document processing and may thus lag behind, when the user is
@@ -728,12 +731,9 @@
"jedit_script_indent_limit"}.
The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
- Isabelle / General\<close>.
-
- \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That
- can be purged manually with the jEdit action @{action "remove-trailing-ws"}
- (shortcut \<^verbatim>\<open>C+e r\<close>). Moreover, the \<^emph>\<open>WhiteSpace\<close> plugin provides some
- aggressive options to trim whitespace on buffer-save.
+ Isabelle / General\<close>. A prerequisite for advanced indentation is \<^emph>\<open>Utilities
+ / Buffer Options / Automatic indentation\<close>: it needs to be set to \<^verbatim>\<open>full\<close>
+ (default).
\<close>
@@ -820,7 +820,7 @@
concrete syntax of the @{command_ref theory} command @{cite
"isabelle-isar-ref"};
- \<^enum> via \<^bold>\<open>auxiliary files\<close> that are loaded into a theory by special \<^emph>\<open>load
+ \<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>load
commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}
@{cite "isabelle-isar-ref"}.
@@ -836,10 +836,7 @@
text \<open>
The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview
of the status of continuous checking of theory nodes within the document
- model. Unlike batch sessions of @{tool build} @{cite "isabelle-system"},
- theory nodes are identified by full path names; this allows to work with
- multiple (disjoint) Isabelle sessions simultaneously within the same editor
- session.
+ model.
\begin{figure}[!htb]
\begin{center}
@@ -853,13 +850,13 @@
Theory imports are resolved automatically by the PIDE document model: all
required files are loaded and stored internally, without the need to open
corresponding jEdit buffers. Opening or closing editor buffers later on has
- no impact on the formal document content: it only affects visibility.
+ no direct impact on the formal document content: it only affects visibility.
- In contrast, auxiliary files (e.g.\ from \<^verbatim>\<open>ML_file\<close> commands) are \<^emph>\<open>not\<close>
- resolved within the editor by default, but the prover process takes care of
- that. This may be changed by enabling the system option @{system_option
- jedit_auto_resolve}: it ensures that all files are uniformly provided by the
- editor.
+ In contrast, auxiliary files (e.g.\ from @{command ML_file} commands) are
+ \<^emph>\<open>not\<close> resolved within the editor by default, but the prover process takes
+ care of that. This may be changed by enabling the system option
+ @{system_option jedit_auto_resolve}: it ensures that all files are uniformly
+ provided by the editor.
\<^medskip>
The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective
@@ -877,6 +874,10 @@
visibility status (if continuous checking is enabled). Big theory libraries
that are marked as required can have significant impact on performance!
+ The \<^emph>\<open>Purge\<close> button restricts the document model to theories that are
+ required for open editor buffers: inaccessible theories are removed and will
+ be rechecked when opened or imported later.
+
\<^medskip>
Formal markup of checked theory content is turned into GUI rendering, based
on a standard repertoire known from mainstream IDEs for programming
@@ -912,7 +913,9 @@
edited conveniently in the Prover IDE on small machines with only 8\,GB of
main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
- \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example.
+ \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example. It is also possible to
+ explore the Isabelle/Pure bootstrap process (a virtual copy) by opening
+ \<^file>\<open>$ISABELLE_HOME/src/Pure/ROOT.ML\<close> like a theory in the Prover IDE.
Initially, before an auxiliary file is opened in the editor, the prover
reads its content from the physical file-system. After the file is opened
@@ -980,9 +983,11 @@
The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but without
direct correspondence to text positions. The coloured rectangles represent
the amount of messages of a certain kind (warnings, errors, etc.) and the
- execution status of commands. A double-click on one of the theory entries
- with their status overview opens the corresponding text buffer, without
- moving the cursor to a specific point.
+ execution status of commands. The border of each rectangle indicates the
+ overall status of processing: a thick border means it is \<^emph>\<open>finished\<close> or
+ \<^emph>\<open>failed\<close> (with color for errors). A double-click on one of the theory
+ entries with their status overview opens the corresponding text buffer,
+ without moving the cursor to a specific point.
\<^medskip>
The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given
@@ -1877,6 +1882,16 @@
\<close>
+section \<open>Document preview\<close>
+
+text \<open>
+ The action @{action_def isabelle.preview} opens an HTML preview of the
+ current theory document in the default web browser. The content is derived
+ from the semantic markup produced by the prover, and thus depends on the
+ status of formal processing.
+\<close>
+
+
chapter \<open>ML debugging within the Prover IDE\<close>
text \<open>
@@ -2064,12 +2079,6 @@
\<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable
continuous checking temporarily.
- \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the collection
- of theories.
-
- \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close \<^emph>\<open>without\<close>
- saving changes.
-
\<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
editor font size depend on platform details and national keyboards.
@@ -2095,15 +2104,6 @@
\<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
- \<^item> \<^bold>\<open>Problem:\<close> Mac OS X with Retina display has problems to determine the
- font metrics of \<^verbatim>\<open>IsabelleText\<close> accurately, notably in plain Swing text
- fields (e.g.\ in the \<^emph>\<open>Search and Replace\<close> dialog).
-
- \<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system
- with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against
- that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{path
- "$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.
-
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
event handling of Java/AWT/Swing.
@@ -2135,7 +2135,7 @@
\<^bold>\<open>Workaround:\<close> On a 64bit platform, ensure that the JVM runs in 64bit mode,
but the Isabelle/ML process remains in 32bit mode! Do not switch Isabelle/ML
into 64bit mode in the expectation to be ``more efficient'' --- this
- requires approx.\ 32\,GB to make sense.
+ requires 16--32\,GB to make sense.
For the JVM, always use the 64bit version. That is the default on all
platforms, except for Windows: the standard download is for win32, but there
Binary file src/Doc/JEdit/document/output-and-state.png has changed
Binary file src/Doc/JEdit/document/output-including-state.png has changed
Binary file src/Doc/JEdit/document/output.png has changed
Binary file src/Doc/JEdit/document/theories.png has changed
--- a/src/Doc/System/Sessions.thy Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Doc/System/Sessions.thy Sat Sep 23 20:09:16 2017 +0200
@@ -440,4 +440,82 @@
@{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
\<close>
+
+section \<open>Maintain theory imports wrt.\ session structure\<close>
+
+text \<open>
+ The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
+ session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
+ \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
+\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
+
+ Options are:
+ -D DIR include session directory and select its sessions
+ -I operation: report potential session imports
+ -M operation: Mercurial repository check for theory files
+ -R operate on requirements of selected sessions
+ -U operation: update theory imports to use session qualifiers
+ -X NAME exclude sessions from group NAME and all descendants
+ -a select all sessions
+ -d DIR include session directory
+ -g NAME select session group NAME
+ -i incremental update according to session graph structure
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose
+ -x NAME exclude session NAME and all descendants
+
+ Maintain theory imports wrt. session structure. At least one operation
+ needs to be specified (see options -I -M -U).\<close>}
+
+ \<^medskip>
+ The selection of sessions and session directories works as for @{tool build}
+ 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
+ \secref{sec:tool-build}).
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
+ (see \secref{sec:tool-build}).
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-I\<close> determines potential session imports, which may be turned into
+ \isakeyword{sessions} within the corresponding \<^verbatim>\<open>ROOT\<close> file entry. Thus
+ theory imports from other sessions may use session-qualified names. For
+ example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> may become formal
+ \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
+ \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
+ the underlying session directories; non-repository directories are ignored.
+ This helps to find files that are accidentally ignored, e.g.\ due to
+ rearrangements of the session structure.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
+ to canonical session-qualified theory names, according to the theory name
+ space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
+
+ Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
+ following to the session graph structure in bottom-up order. This may
+ lead to more accurate results in complex session hierarchies.
+\<close>
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Determine potential session imports for some project directory:
+ @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
+
+ \<^smallskip>
+ Mercurial repository check for some project directory:
+ @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
+
+ \<^smallskip>
+ Incremental update of theory imports for some project directory:
+ @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
+\<close>
+
end
--- a/src/Doc/antiquote_setup.ML Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Doc/antiquote_setup.ML Sat Sep 23 20:09:16 2017 +0200
@@ -177,7 +177,8 @@
NONE => ""
| SOME is_def =>
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
- val _ = check ctxt (name, pos);
+ val _ =
+ if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
in
idx ^
(Output.output name
--- a/src/HOL/Analysis/Summation_Tests.thy Fri Sep 22 14:14:41 2017 -0300
+++ b/src/HOL/Analysis/Summation_Tests.thy Sat Sep 23 20:09:16 2017 +0200
@@ -10,7 +10,7 @@
"HOL-Library.Discrete"
"HOL-Library.Extended_Real"
"HOL-Library.Liminf_Limsup"
- "Extended_Real_Limits"
+ Extended_Real_Limits
begin
text \<open>
--- a/src/HOL/Data_Structures/Base_FDS.thy Fri Sep 22 14:14:41 2017 -0300
+++ b/src/HOL/Data_Structures/Base_FDS.thy Sat Sep 23 20:09:16 2017 +0200
@@ -1,5 +1,5 @@
theory Base_FDS
-imports "../Library/Pattern_Aliases"
+imports "HOL-Library.Pattern_Aliases"
begin
declare Let_def [simp]
--- a/src/Pure/PIDE/protocol.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Pure/PIDE/protocol.scala Sat Sep 23 20:09:16 2017 +0200
@@ -316,11 +316,14 @@
Symbol.encode_yxml(list(pair(string, string))(table))
}
- def session_base(resources: Resources): Unit =
+ def session_base(resources: Resources)
+ {
+ val base = resources.session_base.standard_path
protocol_command("Prover.session_base",
- encode_table(resources.session_base.global_theories.toList),
- encode_table(resources.session_base.loaded_theories.toList),
- encode_table(resources.session_base.dest_known_theories))
+ encode_table(base.global_theories.toList),
+ encode_table(base.loaded_theories.toList),
+ encode_table(base.dest_known_theories))
+ }
/* interned items */
--- a/src/Pure/System/isabelle_system.ML Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Pure/System/isabelle_system.ML Sat Sep 23 20:09:16 2017 +0200
@@ -6,6 +6,7 @@
signature ISABELLE_SYSTEM =
sig
+ val rm_tree: Path.T -> unit
val mkdirs: Path.T -> unit
val mkdir: Path.T -> unit
val copy_dir: Path.T -> Path.T -> unit
--- a/src/Pure/System/options.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Pure/System/options.scala Sat Sep 23 20:09:16 2017 +0200
@@ -147,7 +147,7 @@
/* Isabelle tool wrapper */
- val isabelle_tool = Isabelle_Tool("option", "print Isabelle system options", args =>
+ val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options", args =>
{
var build_options = false
var get_option = ""
--- a/src/Pure/Thy/present.ML Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Pure/Thy/present.ML Sat Sep 23 20:09:16 2017 +0200
@@ -196,7 +196,7 @@
fun isabelle_document {verbose, purge} format name tags dir =
let
- val s = "isabelle document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
+ val s = "isabelle document -o '" ^ format ^ "' \
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
val _ = if verbose then writeln s else ();
@@ -206,6 +206,7 @@
cat_error out ("Failed to build document " ^ quote (show_path doc_path))
else if verbose then writeln out
else ();
+ val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
in doc_path end;
--- a/src/Pure/Thy/sessions.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Pure/Thy/sessions.scala Sat Sep 23 20:09:16 2017 +0200
@@ -81,6 +81,11 @@
theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+ def standard_path: Known =
+ copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))),
+ theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
+ files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
+
def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
{
val res = files.getOrElse(File.canonical(file), Nil).headOption
@@ -114,6 +119,7 @@
def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
def platform_path: Base = copy(known = known.platform_path)
+ def standard_path: Base = copy(known = known.standard_path)
def loaded_theory(name: Document.Node.Name): Boolean =
loaded_theories.isDefinedAt(name.theory)
--- a/src/Pure/Tools/build.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Pure/Tools/build.scala Sat Sep 23 20:09:16 2017 +0200
@@ -455,9 +455,6 @@
//{{{ finish job
val process_result = job.join
- process_result.err_lines.foreach(progress.echo(_))
- if (process_result.ok)
- progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
val process_result_tail =
@@ -469,6 +466,8 @@
(if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
}
+
+ // write log file
val heap_stamp =
if (process_result.ok) {
(store.output_dir + store.log(name)).file.delete
@@ -485,8 +484,6 @@
(store.output_dir + store.log_gz(name)).file.delete
File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
- progress.echo(name + " FAILED")
- if (!process_result.interrupted) progress.echo(process_result_tail.out)
None
}
@@ -506,6 +503,16 @@
Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
}
+ // messages
+ process_result.err_lines.foreach(progress.echo(_))
+
+ if (process_result.ok)
+ progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
+ else {
+ progress.echo(name + " FAILED")
+ if (!process_result.interrupted) progress.echo(process_result_tail.out)
+ }
+
loop(pending - name, running - name,
results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
//}}}
--- a/src/Pure/Tools/imports.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Pure/Tools/imports.scala Sat Sep 23 20:09:16 2017 +0200
@@ -119,7 +119,7 @@
}
if (operation_repository_files) {
- progress.echo("\nMercurial files check:")
+ progress.echo("\nMercurial repository check:")
val unused_files =
for {
(_, dir) <- Sessions.directories(dirs, select_dirs)
@@ -235,7 +235,7 @@
Options are:
-D DIR include session directory and select its sessions
-I operation: report potential session imports
- -M operation: Mercurial files check for imported theory files
+ -M operation: Mercurial repository check for theory files
-R operate on requirements of selected sessions
-U operation: update theory imports to use session qualifiers
-X NAME exclude sessions from group NAME and all descendants
--- a/src/Pure/Tools/jedit.ML Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Pure/Tools/jedit.ML Sat Sep 23 20:09:16 2017 +0200
@@ -32,7 +32,8 @@
Lazy.lazy (fn () =>
(case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) of
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
- | _ => []));
+ | _ => [])
+ |> maps (fn a => [a, a ^ "-toggle", a ^ "-float"]));
val jedit_actions =
Lazy.lazy (fn () =>
--- a/src/Tools/VSCode/extension/package.json Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Tools/VSCode/extension/package.json Sat Sep 23 20:09:16 2017 +0200
@@ -10,7 +10,7 @@
"document preparation"
],
"icon": "isabelle.png",
- "version": "0.23.0",
+ "version": "1.0.0",
"publisher": "makarius",
"license": "MIT",
"repository": {
@@ -492,9 +492,9 @@
"postinstall": "node ./node_modules/vscode/bin/install"
},
"devDependencies": {
- "@types/mocha": "^2.2.42",
+ "@types/mocha": "^2.2.43",
"@types/node": "^7.0.43",
- "mocha": "^3.5.0",
+ "mocha": "^3.5.3",
"typescript": "^2.5.2",
"vscode": "^1.1.5"
},
--- a/src/Tools/VSCode/src/document_model.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Tools/VSCode/src/document_model.scala Sat Sep 23 20:09:16 2017 +0200
@@ -45,6 +45,16 @@
lazy val bibtex_entries: List[Text.Info[String]] =
try { Bibtex.entries(text) }
catch { case ERROR(_) => Nil }
+
+ def recode_symbols: List[Protocol.TextEdit] =
+ (for {
+ (line, l) <- doc.lines.iterator.zipWithIndex
+ text1 = Symbol.encode(line.text)
+ if (line.text != text1)
+ } yield {
+ val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length))
+ Protocol.TextEdit(range, text1)
+ }).toList
}
def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
@@ -56,6 +66,7 @@
editor: Server.Editor,
node_name: Document.Node.Name,
content: Document_Model.Content,
+ version: Option[Long] = None,
external_file: Boolean = false,
node_required: Boolean = false,
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
@@ -66,10 +77,12 @@
model =>
- /* text */
+ /* content */
def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
+ def set_version(new_version: Long): Document_Model = copy(version = Some(new_version))
+
/* external file */
@@ -163,12 +176,27 @@
}
}
- def flush_edits(doc_blobs: Document.Blobs, caret: Option[Line.Position])
- : Option[(List[Document.Edit_Text], Document_Model)] =
+ def flush_edits(
+ unicode_symbols: Boolean,
+ doc_blobs: Document.Blobs,
+ file: JFile,
+ caret: Option[Line.Position])
+ : Option[((List[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] =
{
+ val workspace_edits =
+ if (unicode_symbols && version.isDefined) {
+ val edits = content.recode_symbols
+ if (edits.nonEmpty) List(Protocol.TextDocumentEdit(file, version.get, edits))
+ else Nil
+ }
+ else Nil
+
val (reparse, perspective) = node_perspective(doc_blobs, caret)
- if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
- val edits = node_edits(node_header, pending_edits, perspective)
+ if (reparse || pending_edits.nonEmpty || last_perspective != perspective ||
+ workspace_edits.nonEmpty)
+ {
+ val prover_edits = node_edits(node_header, pending_edits, perspective)
+ val edits = (workspace_edits, prover_edits)
Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
}
else None
--- a/src/Tools/VSCode/src/protocol.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Tools/VSCode/src/protocol.scala Sat Sep 23 20:09:16 2017 +0200
@@ -62,6 +62,11 @@
/* request message */
+ object Id
+ {
+ def empty: Id = Id("")
+ }
+
sealed case class Id(id: Any)
{
require(
@@ -118,6 +123,9 @@
def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
if (error == "") apply(id, result = result)
else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
+
+ def is_empty(json: JSON.T): Boolean =
+ JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined
}
sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
@@ -324,6 +332,28 @@
object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
+ /* workspace edits */
+
+ sealed case class TextEdit(range: Line.Range, new_text: String)
+ {
+ def json: JSON.T = Map("range" -> Range(range), "newText" -> new_text)
+ }
+
+ sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit])
+ {
+ def json: JSON.T =
+ Map("textDocument" -> Map("uri" -> Url.print_file(file), "version" -> version),
+ "edits" -> edits.map(_.json))
+ }
+
+ object WorkspaceEdit
+ {
+ def apply(edits: List[TextDocumentEdit]): JSON.T =
+ RequestMessage(Id.empty, "workspace/applyEdit",
+ Map("edit" -> Map("documentChanges" -> edits.map(_.json))))
+ }
+
+
/* completion */
sealed case class CompletionItem(
@@ -342,8 +372,7 @@
JSON.optional("documentation" -> documentation) ++
JSON.optional("insertText" -> text) ++
JSON.optional("range" -> range.map(Range(_))) ++
- JSON.optional("textEdit" ->
- range.map(r => Map("range" -> Range(r), "newText" -> text.getOrElse(label)))) ++
+ JSON.optional("textEdit" -> range.map(r => TextEdit(r, text.getOrElse(label)).json)) ++
JSON.optional("command" -> command.map(_.json))
}
--- a/src/Tools/VSCode/src/server.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Tools/VSCode/src/server.scala Sat Sep 23 20:09:16 2017 +0200
@@ -123,7 +123,7 @@
private val delay_input: Standard_Thread.Delay =
Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
- { resources.flush_input(session) }
+ { resources.flush_input(session, channel) }
private val delay_load: Standard_Thread.Delay =
Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
@@ -153,7 +153,7 @@
delay_output.invoke()
}
- private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
+ private def change_document(file: JFile, version: Long, changes: List[Protocol.TextDocumentChange])
{
val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange]
@tailrec def norm(chs: List[Protocol.TextDocumentChange])
@@ -168,7 +168,7 @@
}
norm(changes)
norm_changes.foreach(change =>
- resources.change_model(session, editor, file, change.text, change.range))
+ resources.change_model(session, editor, file, version, change.text, change.range))
delay_input.invoke()
delay_output.invoke()
@@ -326,8 +326,8 @@
delay_caret_update.revoke()
delay_preview.revoke()
- val rc = session.stop()
- if (rc == 0) reply("") else reply("Prover shutdown failed: return code " + rc)
+ val result = session.stop()
+ if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc)
None
case None =>
reply("Prover inactive")
@@ -436,9 +436,10 @@
case Protocol.Initialized(()) =>
case Protocol.Shutdown(id) => shutdown(id)
case Protocol.Exit(()) => exit()
- case Protocol.DidOpenTextDocument(file, _, _, text) =>
- change_document(file, List(Protocol.TextDocumentChange(None, text)))
- case Protocol.DidChangeTextDocument(file, _, changes) => change_document(file, changes)
+ case Protocol.DidOpenTextDocument(file, _, version, text) =>
+ change_document(file, version, List(Protocol.TextDocumentChange(None, text)))
+ case Protocol.DidChangeTextDocument(file, version, changes) =>
+ change_document(file, version, changes)
case Protocol.DidCloseTextDocument(file) => close_document(file)
case Protocol.Completion(id, node_pos) => completion(id, node_pos)
case Protocol.Include_Word(()) => update_dictionary(true, false)
@@ -457,7 +458,7 @@
case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled)
case Protocol.Preview_Request(file, column) => request_preview(file, column)
case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
- case _ => log("### IGNORED")
+ case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED")
}
}
catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
@@ -486,7 +487,7 @@
/* session */
override def session: Session = server.session
- override def flush(): Unit = resources.flush_input(session)
+ override def flush(): Unit = resources.flush_input(session, channel)
override def invoke(): Unit = delay_input.invoke()
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Sep 23 20:09:16 2017 +0200
@@ -155,13 +155,15 @@
session: Session,
editor: Server.Editor,
file: JFile,
+ version: Long,
text: String,
range: Option[Line.Range] = None)
{
state.change(st =>
{
val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
- val model1 = (model.change_text(text, range) getOrElse model).external(false)
+ val model1 =
+ (model.change_text(text, range) getOrElse model).set_version(version).external(false)
st.update_models(Some(file -> model1))
})
}
@@ -256,7 +258,7 @@
/* pending input */
- def flush_input(session: Session)
+ def flush_input(session: Session, channel: Channel)
{
state.change(st =>
{
@@ -264,10 +266,15 @@
(for {
file <- st.pending_input.iterator
model <- st.models.get(file)
- (edits, model1) <- model.flush_edits(st.document_blobs, st.get_caret(file))
+ (edits, model1) <-
+ model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
} yield (edits, (file, model1))).toList
- session.update(st.document_blobs, changed_models.flatMap(_._1))
+ for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
+ channel.write(Protocol.WorkspaceEdit(workspace_edits))
+
+ session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
+
st.copy(
models = st.models ++ changed_models.iterator.map(_._2),
pending_input = Set.empty)
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Sep 22 14:14:41 2017 -0300
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Sep 23 20:09:16 2017 +0200
@@ -110,13 +110,14 @@
echo
echo " Options are:"
echo " -D NAME=X set JVM system property"
- echo " -J OPTION add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
+ echo " -J OPTION add JVM runtime option"
+ echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
echo " -R open ROOT entry of logic session and use its parent"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
echo " -j OPTION add jEdit runtime option"
- echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
+ echo " (default $JEDIT_OPTIONS)"
echo " -l NAME logic session name"
echo " -m MODE add print mode for output"
echo " -n no build of session image on startup"