--- a/.hgtags Thu Nov 24 15:04:05 2016 +0100
+++ b/.hgtags Sun Nov 27 20:25:38 2016 +0100
@@ -34,3 +34,6 @@
d3996d5873ddcf1115ec8d3d511a0bb5dbd1cfc4 Isabelle2016
666c7475f4f7e9ba46c59170026230787c504ca7 Isabelle2016-1-RC0
9ee2480d10b7404683aa7f4c3a30d44cbb6a21b9 Isabelle2016-1-RC1
+2bf4fdcebd495516947e5e85f3b3db01d5fbe1a4 Isabelle2016-1-RC2
+51be997d0698583bf2d3f5a99f37381a146d3a6c Isabelle2016-1-RC3
+49708cffb98dc6ced89f66b10662e6af2808bebd Isabelle2016-1-RC4
--- a/Admin/Release/CHECKLIST Thu Nov 24 15:04:05 2016 +0100
+++ b/Admin/Release/CHECKLIST Sun Nov 27 20:25:38 2016 +0100
@@ -88,6 +88,9 @@
- Admin/cronjob/self_update:
http://bitbucket.org/isabelle_project/isabelle-release
+- src/Pure/Admin/isabelle_cronjon.scala:
+ isabelle_repos_source = isabelle_release_source
+
Post-release
============
--- a/Admin/components/components.sha1 Thu Nov 24 15:04:05 2016 +0100
+++ b/Admin/components/components.sha1 Sun Nov 27 20:25:38 2016 +0100
@@ -115,6 +115,7 @@
377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz
+26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
@@ -136,6 +137,7 @@
bd6a448f0e0d5787747f4f30ca661f9c1868e4a7 polyml-5.6-20151223.tar.gz
5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz
5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz
+853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
--- a/Admin/components/main Thu Nov 24 15:04:05 2016 +0100
+++ b/Admin/components/main Sun Nov 27 20:25:38 2016 +0100
@@ -9,6 +9,7 @@
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
+nunchaku-0.3
polyml-5.6-1
scala-2.11.8
ssh-java-20161009
--- a/Admin/cronjob/main Thu Nov 24 15:04:05 2016 +0100
+++ b/Admin/cronjob/main Sun Nov 27 20:25:38 2016 +0100
@@ -9,4 +9,4 @@
export ISABELLE_IDENTIFIER="cronjob"
"$THIS/../build" jars_fresh || exit $?
-exec "$THIS/../../bin/isabelle_java" "-Duser.timezone=Europe/Berlin" isabelle.Isabelle_Cronjob "$@"
+exec "$THIS/../../bin/isabelle_java" isabelle.Isabelle_Cronjob "$@"
--- a/Admin/cronjob/self_update Thu Nov 24 15:04:05 2016 +0100
+++ b/Admin/cronjob/self_update Sun Nov 27 20:25:38 2016 +0100
@@ -10,5 +10,5 @@
cd "$HOME/cronjob"
mkdir -p run log
-hg -R isabelle pull "http://isabelle.in.tum.de/repos/isabelle" -q || echo "self_update pull failed"
+hg -R isabelle pull "http://bitbucket.org/isabelle_project/isabelle-release" -q || echo "self_update pull failed"
hg -R isabelle update -C -q || echo "self_update update failed"
--- a/NEWS Thu Nov 24 15:04:05 2016 +0100
+++ b/NEWS Sun Nov 27 20:25:38 2016 +0100
@@ -70,6 +70,11 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* More aggressive flushing of machine-generated input, according to
+system option editor_generated_input_delay (in addition to existing
+editor_input_delay for regular user edits). This may affect overall PIDE
+reactivity and CPU usage.
+
* Syntactic indentation according to Isabelle outer syntax. Action
"indent-lines" (shortcut C+i) indents the current line according to
command keywords and some command substructure. Action
@@ -99,7 +104,7 @@
* Highlighting of entity def/ref positions wrt. cursor.
* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
-occurences of the formal entity at the caret position. This facilitates
+occurrences of the formal entity at the caret position. This facilitates
systematic renaming.
* PIDE document markup works across multiple Isar commands, e.g. the
@@ -910,11 +915,12 @@
support for monotonicity and continuity in chain-complete partial orders
and about admissibility conditions for fixpoint inductions.
-* Session HOL-Library: theory Polynomial contains also derivation of
-polynomials but not gcd/lcm on polynomials over fields. This has been
-moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave
-way for a possible future different type class instantiation for
-polynomials over factorial rings. INCOMPATIBILITY.
+* Session HOL-Library: theory Library/Polynomial contains also
+derivation of polynomials (formerly in Library/Poly_Deriv) but not
+gcd/lcm on polynomials over fields. This has been moved to a separate
+theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
+future different type class instantiation for polynomials over factorial
+rings. INCOMPATIBILITY.
* Session HOL-Library: theory Sublist provides function "prefixes" with
the following renaming
--- a/etc/options Thu Nov 24 15:04:05 2016 +0100
+++ b/etc/options Sun Nov 27 20:25:38 2016 +0100
@@ -144,6 +144,9 @@
public option editor_input_delay : real = 0.3
-- "delay for user input (text edits, cursor movement etc.)"
+public option editor_generated_input_delay : real = 1.0
+ -- "delay for machine-generated input that may outperform user edits"
+
public option editor_output_delay : real = 0.1
-- "delay for prover output (markup, common messages etc.)"
--- a/lib/texinputs/isabelle.sty Thu Nov 24 15:04:05 2016 +0100
+++ b/lib/texinputs/isabelle.sty Sun Nov 27 20:25:38 2016 +0100
@@ -73,7 +73,7 @@
\newcommand{\isadigit}[1]{#1}
\newcommand{\isachardefaults}{%
-\def\isacharbell{\isamath{\bigbox}} %requires stmaryrd
+\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
\chardef\isacharbang=`\!%
\chardef\isachardoublequote=`\"%
\chardef\isachardoublequoteopen=`\"%
--- a/src/Doc/Implementation/ML.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Doc/Implementation/ML.thy Sun Nov 27 20:25:38 2016 +0100
@@ -138,7 +138,7 @@
@{ML_text foo1}, @{ML_text foo42}.
\<close>
-paragraph\<open>Scopes.\<close>
+paragraph \<open>Scopes.\<close>
text \<open>
Apart from very basic library modules, ML structures are not ``opened'', but
names are referenced with explicit qualification, as in @{ML
@@ -1192,11 +1192,43 @@
text %mlantiq \<open>
\begin{matharray}{rcl}
@{ML_antiquotation_def "assert"} & : & \<open>ML_antiquotation\<close> \\
+ @{ML_antiquotation_def "undefined"} & : & \<open>ML_antiquotation\<close> \\
\end{matharray}
\<^descr> \<open>@{assert}\<close> inlines a function @{ML_type "bool -> unit"} that raises @{ML
Fail} if the argument is @{ML false}. Due to inlining the source position of
failed assertions is included in the error output.
+
+ \<^descr> \<open>@{undefined}\<close> inlines @{verbatim raise}~@{ML Match}, i.e.\ the ML program
+ behaves as in some function application of an undefined case.
+\<close>
+
+text %mlex \<open>
+ The ML function @{ML undefined} is defined in \<^file>\<open>~~/src/Pure/library.ML\<close>
+ as follows:
+\<close>
+
+ML \<open>fun undefined _ = raise Match\<close>
+
+text \<open>
+ \<^medskip>
+ The following variant uses the antiquotation @{ML_antiquotation undefined}
+ instead:
+\<close>
+
+ML \<open>fun undefined _ = @{undefined}\<close>
+
+text \<open>
+ \<^medskip>
+ Here is the same, using control-symbol notation for the antiquotation, with
+ special rendering of \<^verbatim>\<open>\<^undefined>\<close>:
+\<close>
+
+ML \<open>fun undefined _ = \<^undefined>\<close>
+
+text \<open>
+ \medskip Semantically, all forms are equivalent to a function definition
+ without any clauses, but that is syntactically not allowed in ML.
\<close>
--- a/src/Doc/Isar_Ref/Framework.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy Sun Nov 27 20:25:38 2016 +0100
@@ -485,11 +485,58 @@
entities of Pure (propositions, facts, and goals). The Isar proof language
allows to organize reasoning within the underlying rule calculus of Pure,
but Isar is not another logical calculus. Isar merely imposes certain
- structure and policies on Pure inferences.
+ structure and policies on Pure inferences. The main grammar of the Isar
+ proof language is given in \figref{fig:isar-syntax}.
- Isar is intended as an exercise in minimalism. Approximately half of the
- language is introduced as primitive, the rest defined as derived concepts.
- The grammar in \appref{ap:main-grammar} describes the core language
+ \begin{figure}[htb]
+ \begin{center}
+ \begin{tabular}{rcl}
+ \<open>main\<close> & \<open>=\<close> & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if name: props for vars\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
+ & & \quad\<^theory_text>\<open>fixes vars\<close> \\
+ & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
+ & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
+ & & \quad\<^theory_text>\<open>fixes vars\<close> \\
+ & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
+ & & \quad\<^theory_text>\<open>obtains (name) clause "\<^bold>|" \<dots> "proof"\<close> \\
+ \<open>proof\<close> & \<open>=\<close> & \<^theory_text>\<open>"refinement\<^sup>* proper_proof"\<close> \\
+ \<open>refinement\<close> & \<open>=\<close> & \<^theory_text>\<open>apply method\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
+ \<open>proper_proof\<close> & \<open>=\<close> & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>by method method\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>..\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>.\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>sorry\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>done\<close> \\
+ \<open>statement\<close> & \<open>=\<close> & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>next\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>write name (mixfix)\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>presume name: props if props for vars\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>define clause\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>case name: "case"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>from thms goal\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>with thms goal\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>also\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>finally goal\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>moreover\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>ultimately goal\<close> \\
+ \<open>goal\<close> & \<open>=\<close> & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>show name: props when name: props for vars "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>consider (name) clause "\<^bold>|" \<dots> "proof"\<close> \\
+ & \<open>|\<close> & \<^theory_text>\<open>obtain (name) clause "proof"\<close> \\
+ \<open>clause\<close> & \<open>=\<close> & \<^theory_text>\<open>vars where name: props if props for vars\<close> \\
+ \end{tabular}
+ \end{center}
+ \caption{Main grammar of the Isar proof language}\label{fig:isar-syntax}
+ \end{figure}
+
+ The construction of the Isar proof language proceeds in a bottom-up fashion,
+ as an exercise in purity and minimalism. The grammar in
+ \appref{ap:main-grammar} describes the primitive parts of the core language
(category \<open>proof\<close>), which is embedded into the main outer theory syntax via
elements that require a proof (e.g.\ \<^theory_text>\<open>theorem\<close>, \<^theory_text>\<open>lemma\<close>, \<^theory_text>\<open>function\<close>,
\<^theory_text>\<open>termination\<close>).
--- a/src/Doc/Isar_Ref/document/root.tex Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Doc/Isar_Ref/document/root.tex Sun Nov 27 20:25:38 2016 +0100
@@ -64,6 +64,7 @@
\chapter*{Preface}
\input{Preface.tex}
\tableofcontents
+\listoffigures
\clearfirst
\part{Basic Concepts}
--- a/src/Doc/JEdit/JEdit.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy Sun Nov 27 20:25:38 2016 +0100
@@ -141,8 +141,7 @@
done with the usual care for such an open bazaar of contributions. Arbitrary
combinations of add-on features are apt to cause problems. It is advisable
to start with the default configuration of Isabelle/jEdit and develop some
- understanding how it is supposed to work, before loading too many other
- plugins.
+ sense how it is meant to work, before loading too many other plugins.
\<^medskip>
The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs
@@ -207,12 +206,15 @@
first start of the editor; afterwards the keymap file takes precedence and
is no longer affected by change of default properties.
- This subtle difference of jEdit keymaps versus properties is relevant for
- Isabelle/jEdit due to various fine-tuning of global defaults, with
- additional keyboard shortcuts for Isabelle-specific functionality. Users may
- change their keymap later, but need to copy some keyboard shortcuts manually
- (see also @{path "$JEDIT_SETTINGS/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in
- \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>).
+ 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>.
+
+ \<^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
+ automatically invoked on Isabelle/jEdit startup.
\<close>
@@ -292,7 +294,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\<close>). Thus @{tool jedit_client} can connect to the
+ name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<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
@@ -694,14 +696,44 @@
\<close>
+section \<open>Indentation\<close>
+
+text \<open>
+ Isabelle/jEdit augments the existing indentation facilities of jEdit to take
+ the structure of theory and proof texts into account. There is also special
+ support for unstructured proof scripts.
+
+ \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar.
+
+ Action @{action "indent-lines"} (shortcut \<^verbatim>\<open>C+i\<close>) indents the current line
+ according to command keywords and some command substructure: this
+ approximation may need further manual tuning.
+
+ Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the old
+ and the new line according to command keywords only: this leads to precise
+ alignment of the main Isar language elements. This depends on option
+ @{system_option_def "jedit_indent_newline"} (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
+ editing too quickly; see also option @{system_option_def
+ "jedit_script_indent"} and @{system_option_def
+ "jedit_script_indent_limit"}.
+
+ The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
+ Isabelle / General\<close>.
+\<close>
+
+
section \<open>SideKick parsers \label{sec:sidekick}\<close>
text \<open>
The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer
structure in a tree view. Isabelle/jEdit provides SideKick parsers for its
- main mode for theory files, as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file
- (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system \<^verbatim>\<open>options\<close>, and
- Bib{\TeX} files (\secref{sec:bibtex}).
+ main mode for theory files, ML files, as well as some minor modes for the
+ \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system
+ \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}).
\begin{figure}[!htb]
\begin{center}
@@ -711,6 +743,19 @@
\label{fig:sidekick}
\end{figure}
+ The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides a
+ tree-view on the formal document structure, with section headings at the top
+ and formal specification elements at the bottom. The alternative parser
+ \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>
+ end\<close> structure.
+
+ \<^medskip>
+ Isabelle/ML files are structured according to semi-formal comments that are
+ explained in @{cite "isabelle-implementation"}. This outline is turned into
+ a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a
+ folding mode of the same name, for hierarchic text folds within ML files.
+
+ \<^medskip>
The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpreted
markup tree of the PIDE document model of the current buffer. This is
occasionally useful for informative purposes, but the amount of displayed
@@ -1155,6 +1200,40 @@
\<close>
+section \<open>Formal scopes and semantic selection\<close>
+
+text \<open>
+ Formal entities are semantically annotated in the source text as explained
+ in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the
+ defining position with all its referencing positions. This correspondence is
+ highlighted in the text according to the cursor position, see also
+ \figref{fig:scope1}. Here the referencing positions are rendered with an
+ additional border, in reminiscence to a hyperlink: clicking there moves the
+ cursor to the original defining position.
+
+ \begin{figure}[!htb]
+ \begin{center}
+ \includegraphics[scale=0.5]{scope1}
+ \end{center}
+ \caption{Scope of formal entity: defining vs.\ referencing positions}
+ \label{fig:scope1}
+ \end{figure}
+
+ The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
+ supports semantic selection of all occurrences of the formal entity at the
+ caret position. This facilitates systematic renaming, using regular jEdit
+ editing of a multi-selection, see also \figref{fig:scope2}.
+
+ \begin{figure}[!htb]
+ \begin{center}
+ \includegraphics[scale=0.5]{scope2}
+ \end{center}
+ \caption{The result of semantic selection and systematic renaming}
+ \label{fig:scope2}
+ \end{figure}
+\<close>
+
+
section \<open>Completion \label{sec:completion}\<close>
text \<open>
@@ -1199,12 +1278,12 @@
kinds and purposes. The completion mechanism supports this by the following
built-in templates:
- \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) supports \<^emph>\<open>quotations\<close> via text
- cartouches. There are three selections, which are always presented in the
- same order and do not depend on any context information. The default
- choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the box indicates the cursor
- position after insertion; the other choices help to repair the block
- structure of unbalanced text cartouches.
+ \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) or \<^verbatim>\<open>"\<close> (double ASCII quote) support
+ \<^emph>\<open>quotations\<close> via text cartouches. There are three selections, which are
+ always presented in the same order and do not depend on any context
+ information. The default choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the
+ box indicates the cursor position after insertion; the other choices help
+ to repair the block structure of unbalanced text cartouches.
\<^descr> \<^verbatim>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'', where the box indicates
the cursor position after insertion. Here it is convenient to use the
@@ -1213,8 +1292,8 @@
With some practice, input of quoted sub-languages and antiquotations of
embedded languages should work fluently. Note that national keyboard layouts
- might cause problems with back-quote as dead key: if possible, dead keys
- should be disabled.
+ might cause problems with back-quote as dead key, but double quote can be
+ used instead.
\<close>
@@ -1274,6 +1353,20 @@
\<close>
+subsubsection \<open>User-defined abbreviations\<close>
+
+text \<open>
+ The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword
+ @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in
+ templates and abbreviations for Isabelle symbols, as explained above.
+ Examples may be found in the Isabelle sources, by searching for
+ ``\<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.
+
+ The \<^emph>\<open>Symbols\<close> panel shows the abbreviations that are available in the
+ current theory buffer (according to its \<^theory_text>\<open>imports\<close>) in the \<^verbatim>\<open>Abbrevs\<close> tab.
+\<close>
+
+
subsubsection \<open>Name-space entries\<close>
text \<open>
@@ -2020,6 +2113,27 @@
\<^bold>\<open>Workaround:\<close> Use native full-screen control of the window manager (notably
on Mac OS X).
+
+ \<^item> \<^bold>\<open>Problem:\<close> Heap space of the JVM may fill up and render the Prover IDE
+ unresponsive, e.g.\ when editing big Isabelle sessions with many theories.
+
+ \<^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.
+
+ 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
+ is a separate download for win64. This implicitly provides a larger default
+ heap for the JVM.
+
+ Moreover, it is possible to increase JVM heap parameters explicitly, by
+ editing platform-specific files (for ``properties'' or ``options'') that are
+ associated with the main app bundle.
+
+ Also note that jEdit provides a heap space monitor in the status line
+ (bottom-right). Double-clicking on that causes full garbage-collection,
+ which sometimes helps in low-memory situations.
\<close>
end
\ No newline at end of file
Binary file src/Doc/JEdit/document/scope1.png has changed
Binary file src/Doc/JEdit/document/scope2.png has changed
--- a/src/Doc/ROOT Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Doc/ROOT Sun Nov 27 20:25:38 2016 +0100
@@ -234,6 +234,8 @@
"popup2.png"
"query.png"
"root.tex"
+ "scope1.png"
+ "scope2.png"
"sidekick-document.png"
"sidekick.png"
"sledgehammer.png"
--- a/src/Doc/System/Environment.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Doc/System/Environment.thy Sun Nov 27 20:25:38 2016 +0100
@@ -214,8 +214,8 @@
\<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
- usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
- component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
+ usual, the content is interpreted as a GNU bash script. It may refer to
+ the component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
For example, the following setting allows to refer to files within the
component later on, without having to hardwire absolute paths:
@@ -260,9 +260,12 @@
text \<open>
The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
- Isabelle related utilities, user interfaces etc. Such tools automatically
- benefit from the settings mechanism. All Isabelle command-line tools are
- invoked via a common wrapper --- @{executable_ref isabelle}:
+ Isabelle-related utilities, user interfaces, add-on applications etc. Such
+ tools automatically benefit from the settings mechanism
+ (\secref{sec:settings}). Moreover, this is the standard way to invoke
+ Isabelle/Scala functionality as a separate operating-system process.
+ Isabelle command-line tools are run uniformly via a common wrapper ---
+ @{executable_ref isabelle}:
@{verbatim [display]
\<open>Usage: isabelle TOOL [ARGS ...]
@@ -271,12 +274,32 @@
Available tools:
...\<close>}
- In principle, Isabelle tools are ordinary executable scripts that are run
- within the Isabelle settings environment, see \secref{sec:settings}. The set
- of available tools is collected by @{executable isabelle} from the
- directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
- call the scripts directly from the shell. Neither should you add the tool
- directories to your shell's search path!
+ Tools may be implemented in Isabelle/Scala or as stand-alone executables
+ (usually as GNU bash scripts). In the invocation of ``@{executable
+ isabelle}~\<open>tool\<close>'', the named \<open>tool\<close> is resolved as follows (and in the
+ given order).
+
+ \<^enum> An external tool found on the directories listed in the @{setting
+ ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX
+ notation).
+
+ \<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define
+ some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala
+ compiler is invoked on the spot (which may take some time), and the body
+ function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>.
+
+ \<^enum> If an executable file ``\<open>tool\<close>'' is found, it is invoked as
+ stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close>
+ array.
+
+ \<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close>
+ within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred
+ entry-point for high-end tools implemented in Isabelle/Scala --- compiled
+ once when the Isabelle distribution is built. These tools are provided by
+ Isabelle/Pure and cannot be augmented in user-space.
+
+ There are also some administrative tools that are available from a bare
+ repository clone of Isabelle, but not in regular distributions.
\<close>
@@ -346,7 +369,7 @@
loader within ML:
@{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
- Observe the delicate quoting rules for the Bash shell vs.\ ML. The
+ Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
Isabelle/ML and Scala libraries provide functions for that, but here we need
to do it manually.
\<close>
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Sun Nov 27 20:25:38 2016 +0100
@@ -3265,8 +3265,8 @@
lemma homotopic_circlemaps_imp_homotopic_loops:
assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
- shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))
- (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))"
+ shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))
+ (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
proof -
have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
using assms by (auto simp: sphere_def)
@@ -3347,7 +3347,7 @@
and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
proof -
- have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * ii)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * ii))"
+ have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>))"
apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
done
--- a/src/HOL/Analysis/Further_Topology.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Sun Nov 27 20:25:38 2016 +0100
@@ -3240,7 +3240,7 @@
have inj_exp: "inj_on exp (ball (Ln z) 1)"
apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
using pi_ge_two by (simp add: ball_subset_ball_iff)
- define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1))"
+ define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * \<i>) ` (ball(Ln z) 1))"
show ?thesis
proof (intro exI conjI)
show "z \<in> exp ` (ball(Ln z) 1)"
@@ -3286,7 +3286,7 @@
proof
fix u
assume "u \<in> \<V>"
- then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1)"
+ then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * \<i>) ` (ball(Ln z) 1)"
by (auto simp: \<V>_def)
have "compact (cball (Ln z) 1)"
by simp
@@ -3325,7 +3325,7 @@
apply (force simp:)
done
show "\<exists>q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
- apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * ii) \<circ> \<gamma>" in exI)
+ apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * \<i>) \<circ> \<gamma>" in exI)
unfolding homeomorphism_def
apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id])
apply (auto simp: \<gamma>exp exp2n cont n)
--- a/src/HOL/Decision_Procs/approximation_generator.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Sun Nov 27 20:25:38 2016 +0100
@@ -52,6 +52,8 @@
| mapprox_floatarith @{term Pi} _ = Math.pi
| mapprox_floatarith (@{term Sqrt} $ a) xs = Math.sqrt (mapprox_floatarith a xs)
| mapprox_floatarith (@{term Exp} $ a) xs = Math.exp (mapprox_floatarith a xs)
+ | mapprox_floatarith (@{term Powr} $ a $ b) xs =
+ Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)
| mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs)
| mapprox_floatarith (@{term Power} $ a $ n) xs =
Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy Sun Nov 27 20:25:38 2016 +0100
@@ -300,7 +300,7 @@
theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
- assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
+ assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
show A
proof (rule classical)
assume "\<not> A"
@@ -309,7 +309,7 @@
assume A
with \<open>\<not> A\<close> show B by (rule contradiction)
qed
- with a show A ..
+ with * show A ..
qed
qed
--- a/src/HOL/Nunchaku/Nunchaku.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Nunchaku/Nunchaku.thy Sun Nov 27 20:25:38 2016 +0100
@@ -9,9 +9,9 @@
https://github.com/nunchaku-inria
-The "$NUNCHAKU" environment variable must be set to the absolute file name of
-the "nunchaku" executable. The Isabelle components for CVC4 and Kodkodi are
-necessary to use these backends.
+The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
+the directory containing the "nunchaku" executable. The Isabelle components
+for CVC4 and Kodkodi are necessary to use these backends.
*)
theory Nunchaku
--- a/src/HOL/Nunchaku/Tools/nunchaku.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Nunchaku/Tools/nunchaku.ML Sun Nov 27 20:25:38 2016 +0100
@@ -256,7 +256,7 @@
| Unknown (SOME (output, _)) => sat_or_maybe_sat false output
| Timeout => (print_n "Time out"; (unknownN, NONE))
| Nunchaku_Var_Not_Set =>
- (print_n ("Variable $" ^ nunchaku_env_var ^ " not set"); (unknownN, NONE))
+ (print_n ("Variable $" ^ nunchaku_home_env_var ^ " not set"); (unknownN, NONE))
| Nunchaku_Cannot_Execute =>
(print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
| Nunchaku_Not_Found =>
--- a/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML Sun Nov 27 20:25:38 2016 +0100
@@ -33,7 +33,7 @@
| CVC4_Not_Found
| Unknown_Error of int * string
- val nunchaku_env_var: string
+ val nunchaku_home_env_var: string
val solve_nun_problem: tool_params -> nun_problem -> nun_outcome
end;
@@ -71,7 +71,7 @@
((out, err), rc)
end;
-val nunchaku_env_var = "NUNCHAKU";
+val nunchaku_home_env_var = "NUNCHAKU_HOME";
val cached_outcome =
Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option);
@@ -79,13 +79,13 @@
fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
(problem as {sound, complete, ...}) =
with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
- if getenv nunchaku_env_var = "" then
+ if getenv nunchaku_home_env_var = "" then
Nunchaku_Var_Not_Set
else
let
val bash_cmd =
- "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^ nunchaku_env_var ^ "\" \
- \--skolems-in-model --no-color " ^
+ "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
+ nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
(if specialize then "" else "--no-specialize ") ^
"--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
File.bash_path prob_path;
@@ -99,10 +99,12 @@
(if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []})
else if String.isPrefix "UNSAT" output then
if complete then Unsat else Unknown NONE
+ else if String.isSubstring "TIMEOUT" output
+ (* FIXME: temporary *)
+ orelse String.isSubstring "kodkod failed (errcode 152)" error then
+ Timeout
else if String.isPrefix "UNKNOWN" output then
Unknown NONE
- else if String.isPrefix "TIMEOUT" output then
- Timeout
else if code = 126 then
Nunchaku_Cannot_Execute
else if code = 127 then
--- a/src/HOL/Probability/Fin_Map.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Sun Nov 27 20:25:38 2016 +0100
@@ -5,7 +5,7 @@
section \<open>Finite Maps\<close>
theory Fin_Map
- imports Finite_Product_Measure "~~/src/HOL/Library/Finite_Map"
+ imports "~~/src/HOL/Analysis/Finite_Product_Measure" "~~/src/HOL/Library/Finite_Map"
begin
text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of
--- a/src/HOL/Proofs/ex/Hilbert_Classical.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Proofs/ex/Hilbert_Classical.thy Sun Nov 27 20:25:38 2016 +0100
@@ -1,11 +1,12 @@
(* Title: HOL/Proofs/ex/Hilbert_Classical.thy
- Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
+ Author: Stefan Berghofer
+ Author: Makarius Wenzel
*)
section \<open>Hilbert's choice and classical logic\<close>
theory Hilbert_Classical
-imports Main
+ imports Main
begin
text \<open>
@@ -16,145 +17,220 @@
subsection \<open>Proof text\<close>
-theorem tnd: "A \<or> \<not> A"
+theorem tertium_non_datur: "A \<or> \<not> A"
proof -
- let ?P = "\<lambda>X. X = False \<or> X = True \<and> A"
- let ?Q = "\<lambda>X. X = False \<and> A \<or> X = True"
+ let ?P = "\<lambda>x. (A \<and> x) \<or> \<not> x"
+ let ?Q = "\<lambda>x. (A \<and> \<not> x) \<or> x"
have a: "?P (Eps ?P)"
proof (rule someI)
- have "False = False" ..
- thus "?P False" ..
+ have "\<not> False" ..
+ then show "?P False" ..
qed
have b: "?Q (Eps ?Q)"
proof (rule someI)
- have "True = True" ..
- thus "?Q True" ..
+ have True ..
+ then show "?Q True" ..
qed
from a show ?thesis
proof
- assume "Eps ?P = True \<and> A"
- hence A ..
- thus ?thesis ..
+ assume "A \<and> Eps ?P"
+ then have A ..
+ then show ?thesis ..
next
- assume P: "Eps ?P = False"
+ assume "\<not> Eps ?P"
from b show ?thesis
proof
- assume "Eps ?Q = False \<and> A"
- hence A ..
- thus ?thesis ..
+ assume "A \<and> \<not> Eps ?Q"
+ then have A ..
+ then show ?thesis ..
next
- assume Q: "Eps ?Q = True"
+ assume "Eps ?Q"
have neq: "?P \<noteq> ?Q"
proof
assume "?P = ?Q"
- hence "Eps ?P = Eps ?Q" by (rule arg_cong)
+ then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
+ also note \<open>Eps ?Q\<close>
+ finally have "Eps ?P" .
+ with \<open>\<not> Eps ?P\<close> show False by contradiction
+ qed
+ have "\<not> A"
+ proof
+ assume A
+ have "?P = ?Q"
+ proof (rule ext)
+ show "?P x \<longleftrightarrow> ?Q x" for x
+ proof
+ assume "?P x"
+ then show "?Q x"
+ proof
+ assume "\<not> x"
+ with \<open>A\<close> have "A \<and> \<not> x" ..
+ then show ?thesis ..
+ next
+ assume "A \<and> x"
+ then have x ..
+ then show ?thesis ..
+ qed
+ next
+ assume "?Q x"
+ then show "?P x"
+ proof
+ assume "A \<and> \<not> x"
+ then have "\<not> x" ..
+ then show ?thesis ..
+ next
+ assume x
+ with \<open>A\<close> have "A \<and> x" ..
+ then show ?thesis ..
+ qed
+ qed
+ qed
+ with neq show False by contradiction
+ qed
+ then show ?thesis ..
+ qed
+ qed
+qed
+
+
+subsection \<open>Old proof text\<close>
+
+theorem tertium_non_datur1: "A \<or> \<not> A"
+proof -
+ let ?P = "\<lambda>x. (x \<longleftrightarrow> False) \<or> (x \<longleftrightarrow> True) \<and> A"
+ let ?Q = "\<lambda>x. (x \<longleftrightarrow> False) \<and> A \<or> (x \<longleftrightarrow> True)"
+
+ have a: "?P (Eps ?P)"
+ proof (rule someI)
+ show "?P False" using refl ..
+ qed
+ have b: "?Q (Eps ?Q)"
+ proof (rule someI)
+ show "?Q True" using refl ..
+ qed
+
+ from a show ?thesis
+ proof
+ assume "(Eps ?P \<longleftrightarrow> True) \<and> A"
+ then have A ..
+ then show ?thesis ..
+ next
+ assume P: "Eps ?P \<longleftrightarrow> False"
+ from b show ?thesis
+ proof
+ assume "(Eps ?Q \<longleftrightarrow> False) \<and> A"
+ then have A ..
+ then show ?thesis ..
+ next
+ assume Q: "Eps ?Q \<longleftrightarrow> True"
+ have neq: "?P \<noteq> ?Q"
+ proof
+ assume "?P = ?Q"
+ then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
also note P
also note Q
finally show False by (rule False_neq_True)
qed
have "\<not> A"
proof
- assume a: A
+ assume A
have "?P = ?Q"
proof (rule ext)
- fix x show "?P x = ?Q x"
+ show "?P x \<longleftrightarrow> ?Q x" for x
proof
assume "?P x"
- thus "?Q x"
+ then show "?Q x"
proof
- assume "x = False"
- from this and a have "x = False \<and> A" ..
- thus "?Q x" ..
+ assume "x \<longleftrightarrow> False"
+ from this and \<open>A\<close> have "(x \<longleftrightarrow> False) \<and> A" ..
+ then show ?thesis ..
next
- assume "x = True \<and> A"
- hence "x = True" ..
- thus "?Q x" ..
+ assume "(x \<longleftrightarrow> True) \<and> A"
+ then have "x \<longleftrightarrow> True" ..
+ then show ?thesis ..
qed
next
assume "?Q x"
- thus "?P x"
+ then show "?P x"
proof
- assume "x = False \<and> A"
- hence "x = False" ..
- thus "?P x" ..
+ assume "(x \<longleftrightarrow> False) \<and> A"
+ then have "x \<longleftrightarrow> False" ..
+ then show ?thesis ..
next
- assume "x = True"
- from this and a have "x = True \<and> A" ..
- thus "?P x" ..
+ assume "x \<longleftrightarrow> True"
+ from this and \<open>A\<close> have "(x \<longleftrightarrow> True) \<and> A" ..
+ then show ?thesis ..
qed
qed
qed
with neq show False by contradiction
qed
- thus ?thesis ..
+ then show ?thesis ..
qed
qed
qed
-subsection \<open>Proof term of text\<close>
-
-prf tnd
-
+subsection \<open>Old proof script\<close>
-subsection \<open>Proof script\<close>
-
-theorem tnd': "A \<or> \<not> A"
+theorem tertium_non_datur2: "A \<or> \<not> A"
apply (subgoal_tac
- "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
+ "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and>
- (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
+ (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
((SOME x. x = False \<and> A \<or> x = True) = True))")
- prefer 2
- apply (rule conjI)
- apply (rule someI)
- apply (rule disjI1)
- apply (rule refl)
- apply (rule someI)
- apply (rule disjI2)
- apply (rule refl)
+ prefer 2
+ apply (rule conjI)
+ apply (rule someI)
+ apply (rule disjI1)
+ apply (rule refl)
+ apply (rule someI)
+ apply (rule disjI2)
+ apply (rule refl)
apply (erule conjE)
apply (erule disjE)
- apply (erule disjE)
- apply (erule conjE)
- apply (erule disjI1)
- prefer 2
- apply (erule conjE)
- apply (erule disjI1)
+ apply (erule disjE)
+ apply (erule conjE)
+ apply (erule disjI1)
+ prefer 2
+ apply (erule conjE)
+ apply (erule disjI1)
apply (subgoal_tac
- "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
- (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
- prefer 2
- apply (rule notI)
- apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
- apply (drule trans, assumption)
- apply (drule sym)
- apply (drule trans, assumption)
- apply (erule False_neq_True)
+ "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
+ (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
+ prefer 2
+ apply (rule notI)
+ apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
+ apply (drule trans, assumption)
+ apply (drule sym)
+ apply (drule trans, assumption)
+ apply (erule False_neq_True)
apply (rule disjI2)
apply (rule notI)
apply (erule notE)
apply (rule ext)
apply (rule iffI)
+ apply (erule disjE)
+ apply (rule disjI1)
+ apply (erule conjI)
+ apply assumption
+ apply (erule conjE)
+ apply (erule disjI2)
apply (erule disjE)
- apply (rule disjI1)
- apply (erule conjI)
- apply assumption
- apply (erule conjE)
- apply (erule disjI2)
- apply (erule disjE)
- apply (erule conjE)
- apply (erule disjI1)
+ apply (erule conjE)
+ apply (erule disjI1)
apply (rule disjI2)
apply (erule conjI)
apply assumption
done
-subsection \<open>Proof term of script\<close>
+subsection \<open>Proof terms\<close>
-prf tnd'
+prf tertium_non_datur
+prf tertium_non_datur1
+prf tertium_non_datur2
end
--- a/src/HOL/TPTP/mash_export.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/TPTP/mash_export.ML Sun Nov 27 20:25:38 2016 +0100
@@ -286,16 +286,16 @@
not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
#> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
-fun generate_mash_suggestions algorithm =
+fun generate_mash_suggestions algorithm ctxt =
(Options.put_default @{system_option MaSh} algorithm;
- Sledgehammer_MaSh.mash_unlearn ();
+ Sledgehammer_MaSh.mash_unlearn ctxt;
generate_mepo_or_mash_suggestions
(fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} =>
fn max_suggs => fn hyp_ts => fn concl_t =>
tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false
Sledgehammer_Util.one_year)
#> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t
- #> fst))
+ #> fst) ctxt)
fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
let
--- a/src/HOL/Tools/SMT/smt_systems.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Sun Nov 27 20:25:38 2016 +0100
@@ -68,6 +68,7 @@
local
fun cvc4_options ctxt = [
+ "--no-statistics",
"--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
"--lang=smt2",
"--continued-execution",
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sun Nov 27 20:25:38 2016 +0100
@@ -324,10 +324,10 @@
else if subcommand = supported_proversN then
supported_provers ctxt
else if subcommand = unlearnN then
- mash_unlearn ()
+ mash_unlearn ctxt
else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
subcommand = relearn_isarN orelse subcommand = relearn_proverN then
- (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ()
+ (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt
else ();
mash_learn ctxt
(* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Nov 27 20:25:38 2016 +0100
@@ -69,13 +69,13 @@
val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term ->
raw_fact list -> fact list * fact list
- val mash_unlearn : unit -> unit
+ val mash_unlearn : Proof.context -> unit
val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time ->
raw_fact list -> string
val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
val mash_can_suggest_facts : Proof.context -> bool
- val mash_can_suggest_facts_fast : unit -> bool
+ val mash_can_suggest_facts_fast : Proof.context -> bool
val generous_max_suggestions : int -> int
val mepo_weight : real
@@ -274,6 +274,18 @@
end
+(*** Convenience functions for synchronized access ***)
+
+fun synchronized_timed_value var time_limit =
+ Synchronized.timed_access var time_limit (fn value => SOME (value, value))
+fun synchronized_timed_change_result var time_limit f =
+ Synchronized.timed_access var time_limit (SOME o f)
+fun synchronized_timed_change var time_limit f =
+ synchronized_timed_change_result var time_limit (fn x => ((), f x))
+
+fun mash_time_limit _ = SOME (seconds 0.1)
+
+
(*** Isabelle-agnostic machine learning ***)
structure MaSh =
@@ -640,7 +652,7 @@
local
-val version = "*** MaSh version 20160805 ***"
+val version = "*** MaSh version 20161123 ***"
exception FILE_VERSION_TOO_NEW of unit
@@ -734,42 +746,49 @@
in
fun map_state ctxt f =
- Synchronized.change global_state (load_state ctxt ##> f #> save_state ctxt)
+ (trace_msg ctxt (fn () => "Changing MaSh state");
+ synchronized_timed_change global_state mash_time_limit
+ (load_state ctxt ##> f #> save_state ctxt))
+ |> ignore
handle FILE_VERSION_TOO_NEW () => ()
-fun peek_state () =
- let val state = Synchronized.value global_state in
- if would_load_state state then NONE else SOME state
- end
+fun peek_state ctxt =
+ (trace_msg ctxt (fn () => "Peeking at MaSh state");
+ (case synchronized_timed_value global_state mash_time_limit of
+ NONE => NONE
+ | SOME state => if would_load_state state then NONE else SOME state))
fun get_state ctxt =
- Synchronized.change_result global_state (perhaps (try (load_state ctxt)) #> `snd)
+ (trace_msg ctxt (fn () => "Retrieving MaSh state");
+ synchronized_timed_change_result global_state mash_time_limit
+ (perhaps (try (load_state ctxt)) #> `snd))
-fun clear_state () =
- Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state)))
+fun clear_state ctxt =
+ (trace_msg ctxt (fn () => "Clearing MaSh state");
+ Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state))))
end
(*** Isabelle helpers ***)
-fun crude_printed_term depth t =
+fun crude_printed_term size t =
let
fun term _ (res, 0) = (res, 0)
- | term (t $ u) (res, depth) =
+ | term (t $ u) (res, size) =
let
- val (res, depth) = term t (res ^ "(", depth)
- val (res, depth) = term u (res ^ " ", depth)
+ val (res, size) = term t (res ^ "(", size)
+ val (res, size) = term u (res ^ " ", size)
in
- (res ^ ")", depth)
+ (res ^ ")", size)
end
- | term (Abs (s, _, t)) (res, depth) = term t (res ^ "%" ^ s ^ ".", depth - 1)
- | term (Bound n) (res, depth) = (res ^ "#" ^ string_of_int n, depth - 1)
- | term (Const (s, _)) (res, depth) = (res ^ Long_Name.base_name s, depth - 1)
- | term (Free (s, _)) (res, depth) = (res ^ s, depth - 1)
- | term (Var ((s, _), _)) (res, depth) = (res ^ s, depth - 1)
+ | term (Abs (s, _, t)) (res, size) = term t (res ^ "%" ^ s ^ ".", size - 1)
+ | term (Bound n) (res, size) = (res ^ "#" ^ string_of_int n, size - 1)
+ | term (Const (s, _)) (res, size) = (res ^ Long_Name.base_name s, size - 1)
+ | term (Free (s, _)) (res, size) = (res ^ s, size - 1)
+ | term (Var ((s, _), _)) (res, size) = (res ^ s, size - 1)
in
- fst (term t ("", depth))
+ fst (term t ("", size))
end
fun nickname_of_thm th =
@@ -778,11 +797,11 @@
(* There must be a better way to detect local facts. *)
(case Long_Name.dest_local hint of
SOME suf =>
- Long_Name.implode [Thm.theory_name_of_thm th, suf, crude_printed_term 50 (Thm.prop_of th)]
+ Long_Name.implode [Thm.theory_name_of_thm th, suf, crude_printed_term 25 (Thm.prop_of th)]
| NONE => hint)
end
else
- crude_printed_term 100 (Thm.prop_of th)
+ crude_printed_term 50 (Thm.prop_of th)
fun find_suggested_facts ctxt facts =
let
@@ -857,23 +876,17 @@
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
-val pat_tvar_prefix = "_"
-val pat_var_prefix = "_"
+val crude_str_of_sort = space_implode "," o map Long_Name.base_name o subtract (op =) @{sort type}
-(* try "Long_Name.base_name" for shorter names *)
-fun massage_long_name s = s
-
-val crude_str_of_sort = space_implode "," o map massage_long_name o subtract (op =) @{sort type}
-
-fun crude_str_of_typ (Type (s, [])) = massage_long_name s
- | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts)
+fun crude_str_of_typ (Type (s, [])) = Long_Name.base_name s
+ | crude_str_of_typ (Type (s, Ts)) = Long_Name.base_name s ^ implode (map crude_str_of_typ Ts)
| crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S
| crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S
-fun maybe_singleton_str _ "" = []
- | maybe_singleton_str pref s = [pref ^ s]
+fun maybe_singleton_str "" = []
+ | maybe_singleton_str s = [s]
-val max_pat_breadth = 10 (* FUDGE *)
+val max_pat_breadth = 5 (* FUDGE *)
fun term_features_of ctxt thy_name term_max_depth type_max_depth ts =
let
@@ -886,13 +899,12 @@
| add_classes S =
fold (`(Sorts.super_classes classes)
#> swap #> op ::
- #> subtract (op =) @{sort type} #> map massage_long_name
+ #> subtract (op =) @{sort type}
#> map class_feature_of
#> union (op =)) S
fun pattify_type 0 _ = []
- | pattify_type _ (Type (s, [])) =
- if member (op =) bad_types s then [] else [massage_long_name s]
+ | pattify_type depth (Type (s, [])) = if member (op =) bad_types s then [] else [s]
| pattify_type depth (Type (s, U :: Ts)) =
let
val T = Type (s, Ts)
@@ -901,8 +913,8 @@
in
map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
end
- | pattify_type _ (TFree (_, S)) = maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
- | pattify_type _ (TVar (_, S)) = maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
+ | pattify_type _ (TFree (_, S)) = maybe_singleton_str (crude_str_of_sort S)
+ | pattify_type _ (TVar (_, S)) = maybe_singleton_str (crude_str_of_sort S)
fun add_type_pat depth T =
union (op =) (map type_feature_of (pattify_type depth T))
@@ -918,17 +930,16 @@
| add_subtypes T = add_type T
fun pattify_term _ 0 _ = []
- | pattify_term _ _ (Const (s, _)) =
- if is_widely_irrelevant_const s then [] else [massage_long_name s]
+ | pattify_term _ depth (Const (s, _)) =
+ if is_widely_irrelevant_const s then [] else [s]
| pattify_term _ _ (Free (s, T)) =
- maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
- |> (if member (op =) fixes s then
- cons (free_feature_of (massage_long_name (Long_Name.append thy_name s)))
- else
- I)
- | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
+ maybe_singleton_str (crude_str_of_typ T)
+ |> (if member (op =) fixes s then cons (free_feature_of (Long_Name.append thy_name s))
+ else I)
+ | pattify_term _ _ (Var (_, T)) =
+ maybe_singleton_str (crude_str_of_typ T)
| pattify_term Ts _ (Bound j) =
- maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
+ maybe_singleton_str (crude_str_of_typ (nth Ts j))
| pattify_term Ts depth (t $ u) =
let
val ps = take max_pat_breadth (pattify_term Ts depth t)
@@ -972,9 +983,9 @@
(* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn
from such proofs. *)
-val max_dependencies = 20
+val max_dependencies = 20 (* FUDGE *)
-val prover_default_max_facts = 25
+val prover_default_max_facts = 25 (* FUDGE *)
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
val typedef_dep = nickname_of_thm @{thm CollectI}
@@ -1161,7 +1172,7 @@
fun maximal_wrt_access_graph _ [] = []
| maximal_wrt_access_graph access_G (fact :: facts) =
let
- fun cleanup_wrt (fact as (_, th)) =
+ fun cleanup_wrt (_, th) =
let val thy_id = Thm.theory_id_of_thm th in
filter_out (fn (_, th') =>
Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id))
@@ -1224,54 +1235,57 @@
[Thm.prop_of th]
|> features_of ctxt (Thm.theory_name_of_thm th) stature
|> map (rpair (weight * factor))
-
- val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =
- get_state ctxt
+ in
+ (case get_state ctxt of
+ NONE => ([], [])
+ | SOME {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =>
+ let
+ val goal_feats0 =
+ features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts)
+ val chained_feats = chained
+ |> map (rpair 1.0)
+ |> map (chained_or_extra_features_of chained_feature_factor)
+ |> rpair [] |-> fold (union (eq_fst (op =)))
+ val extra_feats = facts
+ |> take (Int.max (0, num_extra_feature_facts - length chained))
+ |> filter fact_has_right_theory
+ |> weight_facts_steeply
+ |> map (chained_or_extra_features_of extra_feature_factor)
+ |> rpair [] |-> fold (union (eq_fst (op =)))
- val goal_feats0 =
- features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts)
- val chained_feats = chained
- |> map (rpair 1.0)
- |> map (chained_or_extra_features_of chained_feature_factor)
- |> rpair [] |-> fold (union (eq_fst (op =)))
- val extra_feats = facts
- |> take (Int.max (0, num_extra_feature_facts - length chained))
- |> filter fact_has_right_theory
- |> weight_facts_steeply
- |> map (chained_or_extra_features_of extra_feature_factor)
- |> rpair [] |-> fold (union (eq_fst (op =)))
-
- val goal_feats =
- fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
- |> debug ? sort (Real.compare o swap o apply2 snd)
+ val goal_feats =
+ fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
+ |> debug ? sort (Real.compare o swap o apply2 snd)
- val parents = maximal_wrt_access_graph access_G facts
- val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
+ val parents = maximal_wrt_access_graph access_G facts
+ val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
- val suggs =
- if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then
- let
- val learns =
- Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
- in
- MaSh.query_external ctxt algorithm max_suggs learns goal_feats
- end
- else
- let
- val int_goal_feats =
- map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
- in
- MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts max_suggs
- goal_feats int_goal_feats
- end
+ val suggs =
+ if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then
+ let
+ val learns =
+ Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps))
+ access_G
+ in
+ MaSh.query_external ctxt algorithm max_suggs learns goal_feats
+ end
+ else
+ let
+ val int_goal_feats =
+ map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
+ in
+ MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts
+ max_suggs goal_feats int_goal_feats
+ end
- val unknown = filter_out (is_fact_in_graph access_G o snd) facts
- in
- find_mash_suggestions ctxt max_suggs suggs facts chained unknown
- |> apply2 (map fact_of_raw_fact)
+ val unknown = filter_out (is_fact_in_graph access_G o snd) facts
+ in
+ find_mash_suggestions ctxt max_suggs suggs facts chained unknown
+ |> apply2 (map fact_of_raw_fact)
+ end)
end
-fun mash_unlearn () = (clear_state (); writeln "Reset MaSh")
+fun mash_unlearn ctxt = (clear_state ctxt; writeln "Reset MaSh")
fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
(accum as (access_G, (fact_xtab, feat_xtab))) =
@@ -1363,164 +1377,169 @@
let
val timer = Timer.startRealTimer ()
fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout
-
- val {access_G, ...} = get_state ctxt
- val is_in_access_G = is_fact_in_graph access_G o snd
- val no_new_facts = forall is_in_access_G facts
in
- if no_new_facts andalso not run_prover then
- if auto_level < 2 then
- "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^
- (if auto_level = 0 andalso not run_prover then
- "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover"
- else
- "")
- else
- ""
- else
+ (case get_state ctxt of
+ NONE => "MaSh is busy\nPlease try again later"
+ | SOME {access_G, ...} =>
let
- val name_tabs = build_name_tables nickname_of_thm facts
+ val is_in_access_G = is_fact_in_graph access_G o snd
+ val no_new_facts = forall is_in_access_G facts
+ in
+ if no_new_facts andalso not run_prover then
+ if auto_level < 2 then
+ "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^
+ (if auto_level = 0 andalso not run_prover then
+ "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover"
+ else
+ "")
+ else
+ ""
+ else
+ let
+ val name_tabs = build_name_tables nickname_of_thm facts
- fun deps_of status th =
- if status = Non_Rec_Def orelse status = Rec_Def then
- SOME []
- else if run_prover then
- prover_dependencies_of ctxt params prover auto_level facts name_tabs th
- |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
- else
- isar_dependencies_of name_tabs th
+ fun deps_of status th =
+ if status = Non_Rec_Def orelse status = Rec_Def then
+ SOME []
+ else if run_prover then
+ prover_dependencies_of ctxt params prover auto_level facts name_tabs th
+ |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
+ else
+ isar_dependencies_of name_tabs th
- fun do_commit [] [] [] state = state
- | do_commit learns relearns flops
- {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =
- let
- val was_empty = Graph.is_empty access_G
+ fun do_commit [] [] [] state = state
+ | do_commit learns relearns flops
+ {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =
+ let
+ val was_empty = Graph.is_empty access_G
- val (learns, (access_G', xtabs')) =
- fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
- |>> map_filter I
- val (relearns, access_G'') =
- fold_map (relearn_wrt_access_graph ctxt) relearns access_G'
+ val (learns, (access_G', xtabs')) =
+ fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
+ |>> map_filter I
+ val (relearns, access_G'') =
+ fold_map (relearn_wrt_access_graph ctxt) relearns access_G'
- val access_G''' = access_G'' |> fold flop_wrt_access_graph flops
- val dirty_facts' =
- (case (was_empty, dirty_facts) of
- (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
- | _ => NONE)
+ val access_G''' = access_G'' |> fold flop_wrt_access_graph flops
+ val dirty_facts' =
+ (case (was_empty, dirty_facts) of
+ (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
+ | _ => NONE)
- val (ffds', freqs') =
- if null relearns then
- recompute_ffds_freqs_from_learns
- (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' num_facts0
- ffds freqs
- else
- recompute_ffds_freqs_from_access_G access_G''' xtabs'
- in
- {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs',
- dirty_facts = dirty_facts'}
- end
+ val (ffds', freqs') =
+ if null relearns then
+ recompute_ffds_freqs_from_learns
+ (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs'
+ num_facts0 ffds freqs
+ else
+ recompute_ffds_freqs_from_access_G access_G''' xtabs'
+ in
+ {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs',
+ dirty_facts = dirty_facts'}
+ end
- fun commit last learns relearns flops =
- (if debug andalso auto_level = 0 then writeln "Committing..." else ();
- map_state ctxt (do_commit (rev learns) relearns flops);
- if not last andalso auto_level = 0 then
- let val num_proofs = length learns + length relearns in
- writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
- (if run_prover then "automatic" else "Isar") ^ " proof" ^
- plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout)
- end
- else
- ())
+ fun commit last learns relearns flops =
+ (if debug andalso auto_level = 0 then writeln "Committing..." else ();
+ map_state ctxt (do_commit (rev learns) relearns flops);
+ if not last andalso auto_level = 0 then
+ let val num_proofs = length learns + length relearns in
+ writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
+ (if run_prover then "automatic" else "Isar") ^ " proof" ^
+ plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout)
+ end
+ else
+ ())
- fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
- | learn_new_fact (parents, ((_, stature as (_, status)), th))
- (learns, (num_nontrivial, next_commit, _)) =
- let
- val name = nickname_of_thm th
- val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
- val deps = these (deps_of status th)
- val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
- val learns = (name, parents, feats, deps) :: learns
- val (learns, next_commit) =
- if Timer.checkRealTimer timer > next_commit then
- (commit false learns [] []; ([], next_commit_time ()))
- else
- (learns, next_commit)
- val timed_out = Timer.checkRealTimer timer > learn_timeout
- in
- (learns, (num_nontrivial, next_commit, timed_out))
- end
+ fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
+ | learn_new_fact (parents, ((_, stature as (_, status)), th))
+ (learns, (num_nontrivial, next_commit, _)) =
+ let
+ val name = nickname_of_thm th
+ val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
+ val deps = these (deps_of status th)
+ val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
+ val learns = (name, parents, feats, deps) :: learns
+ val (learns, next_commit) =
+ if Timer.checkRealTimer timer > next_commit then
+ (commit false learns [] []; ([], next_commit_time ()))
+ else
+ (learns, next_commit)
+ val timed_out = Timer.checkRealTimer timer > learn_timeout
+ in
+ (learns, (num_nontrivial, next_commit, timed_out))
+ end
- val (num_new_facts, num_nontrivial) =
- if no_new_facts then
- (0, 0)
- else
- let
- val new_facts = facts
- |> sort (crude_thm_ord ctxt o apply2 snd)
- |> attach_parents_to_facts []
- |> filter_out (is_in_access_G o snd)
- val (learns, (num_nontrivial, _, _)) =
- ([], (0, next_commit_time (), false))
- |> fold learn_new_fact new_facts
- in
- commit true learns [] []; (length new_facts, num_nontrivial)
- end
+ val (num_new_facts, num_nontrivial) =
+ if no_new_facts then
+ (0, 0)
+ else
+ let
+ val new_facts = facts
+ |> sort (crude_thm_ord ctxt o apply2 snd)
+ |> attach_parents_to_facts []
+ |> filter_out (is_in_access_G o snd)
+ val (learns, (num_nontrivial, _, _)) =
+ ([], (0, next_commit_time (), false))
+ |> fold learn_new_fact new_facts
+ in
+ commit true learns [] []; (length new_facts, num_nontrivial)
+ end
- fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
- | relearn_old_fact ((_, (_, status)), th)
- ((relearns, flops), (num_nontrivial, next_commit, _)) =
- let
- val name = nickname_of_thm th
- val (num_nontrivial, relearns, flops) =
- (case deps_of status th of
- SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
- | NONE => (num_nontrivial, relearns, name :: flops))
- val (relearns, flops, next_commit) =
- if Timer.checkRealTimer timer > next_commit then
- (commit false [] relearns flops; ([], [], next_commit_time ()))
- else
- (relearns, flops, next_commit)
- val timed_out = Timer.checkRealTimer timer > learn_timeout
- in
- ((relearns, flops), (num_nontrivial, next_commit, timed_out))
- end
+ fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
+ | relearn_old_fact ((_, (_, status)), th)
+ ((relearns, flops), (num_nontrivial, next_commit, _)) =
+ let
+ val name = nickname_of_thm th
+ val (num_nontrivial, relearns, flops) =
+ (case deps_of status th of
+ SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
+ | NONE => (num_nontrivial, relearns, name :: flops))
+ val (relearns, flops, next_commit) =
+ if Timer.checkRealTimer timer > next_commit then
+ (commit false [] relearns flops; ([], [], next_commit_time ()))
+ else
+ (relearns, flops, next_commit)
+ val timed_out = Timer.checkRealTimer timer > learn_timeout
+ in
+ ((relearns, flops), (num_nontrivial, next_commit, timed_out))
+ end
- val num_nontrivial =
- if not run_prover then
- num_nontrivial
- else
- let
- val max_isar = 1000 * max_dependencies
+ val num_nontrivial =
+ if not run_prover then
+ num_nontrivial
+ else
+ let
+ val max_isar = 1000 * max_dependencies
- fun priority_of th =
- Random.random_range 0 max_isar +
- (case try (Graph.get_node access_G) (nickname_of_thm th) of
- SOME (Isar_Proof, _, deps) => ~100 * length deps
- | SOME (Automatic_Proof, _, _) => 2 * max_isar
- | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar
- | NONE => 0)
+ fun priority_of th =
+ Random.random_range 0 max_isar +
+ (case try (Graph.get_node access_G) (nickname_of_thm th) of
+ SOME (Isar_Proof, _, deps) => ~100 * length deps
+ | SOME (Automatic_Proof, _, _) => 2 * max_isar
+ | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar
+ | NONE => 0)
- val old_facts = facts
- |> filter is_in_access_G
- |> map (`(priority_of o snd))
- |> sort (int_ord o apply2 fst)
- |> map snd
- val ((relearns, flops), (num_nontrivial, _, _)) =
- (([], []), (num_nontrivial, next_commit_time (), false))
- |> fold relearn_old_fact old_facts
- in
- commit true [] relearns flops; num_nontrivial
- end
- in
- if verbose orelse auto_level < 2 then
- "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ " and " ^
- string_of_int num_nontrivial ^ " nontrivial " ^
- (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s num_nontrivial ^
- (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "")
- else
- ""
- end
+ val old_facts = facts
+ |> filter is_in_access_G
+ |> map (`(priority_of o snd))
+ |> sort (int_ord o apply2 fst)
+ |> map snd
+ val ((relearns, flops), (num_nontrivial, _, _)) =
+ (([], []), (num_nontrivial, next_commit_time (), false))
+ |> fold relearn_old_fact old_facts
+ in
+ commit true [] relearns flops; num_nontrivial
+ end
+ in
+ if verbose orelse auto_level < 2 then
+ "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^
+ " and " ^ string_of_int num_nontrivial ^ " nontrivial " ^
+ (if run_prover then "automatic and " else "") ^ "Isar proof" ^
+ plural_s num_nontrivial ^
+ (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "")
+ else
+ ""
+ end
+ end)
end
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover =
@@ -1552,21 +1571,23 @@
end
fun mash_can_suggest_facts ctxt =
- not (Graph.is_empty (#access_G (get_state ctxt)))
+ (case get_state ctxt of
+ NONE => false
+ | SOME {access_G, ...} => not (Graph.is_empty access_G))
-fun mash_can_suggest_facts_fast () =
- (case peek_state () of
+fun mash_can_suggest_facts_fast ctxt =
+ (case peek_state ctxt of
NONE => false
- | SOME (_, {access_G, ...}) => not (Graph.is_empty access_G));
+ | SOME (_, {access_G, ...}) => not (Graph.is_empty access_G))
(* Generate more suggestions than requested, because some might be thrown out later for various
reasons (e.g., duplicates). *)
fun generous_max_suggestions max_facts = 3 * max_facts div 2 + 25
-val mepo_weight = 0.5
-val mash_weight = 0.5
+val mepo_weight = 0.5 (* FUDGE *)
+val mash_weight = 0.5 (* FUDGE *)
-val max_facts_to_learn_before_query = 100
+val max_facts_to_learn_before_query = 100 (* FUDGE *)
(* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer. *)
val min_secs_for_learning = 10
@@ -1600,27 +1621,29 @@
()
val mash_enabled = is_mash_enabled ()
- val mash_fast = mash_can_suggest_facts_fast ()
+ val mash_fast = mash_can_suggest_facts_fast ctxt
fun please_learn () =
if mash_fast then
- let
- val {access_G, xtabs = ((num_facts0, _), _), ...} = get_state ctxt
- val is_in_access_G = is_fact_in_graph access_G o snd
- val min_num_facts_to_learn = length facts - num_facts0
- in
- if min_num_facts_to_learn <= max_facts_to_learn_before_query then
- (case length (filter_out is_in_access_G facts) of
- 0 => ()
- | num_facts_to_learn =>
- if num_facts_to_learn <= max_facts_to_learn_before_query then
- mash_learn_facts ctxt params prover 2 false timeout facts
- |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s))
- else
- maybe_launch_thread true num_facts_to_learn)
- else
- maybe_launch_thread false min_num_facts_to_learn
- end
+ (case get_state ctxt of
+ NONE => maybe_launch_thread false (length facts)
+ | SOME {access_G, xtabs = ((num_facts0, _), _), ...} =>
+ let
+ val is_in_access_G = is_fact_in_graph access_G o snd
+ val min_num_facts_to_learn = length facts - num_facts0
+ in
+ if min_num_facts_to_learn <= max_facts_to_learn_before_query then
+ (case length (filter_out is_in_access_G facts) of
+ 0 => ()
+ | num_facts_to_learn =>
+ if num_facts_to_learn <= max_facts_to_learn_before_query then
+ mash_learn_facts ctxt params prover 2 false timeout facts
+ |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s))
+ else
+ maybe_launch_thread true num_facts_to_learn)
+ else
+ maybe_launch_thread false min_num_facts_to_learn
+ end)
else
maybe_launch_thread false (length facts)
--- a/src/HOL/Unix/Unix.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Unix/Unix.thy Sun Nov 27 20:25:38 2016 +0100
@@ -5,9 +5,9 @@
section \<open>Unix file-systems \label{sec:unix-file-system}\<close>
theory Unix
-imports
- Nested_Environment
- "~~/src/HOL/Library/Sublist"
+ imports
+ Nested_Environment
+ "~~/src/HOL/Library/Sublist"
begin
text \<open>
@@ -296,26 +296,26 @@
\<close>
primrec uid_of :: "operation \<Rightarrow> uid"
-where
- "uid_of (Read uid text path) = uid"
-| "uid_of (Write uid text path) = uid"
-| "uid_of (Chmod uid perms path) = uid"
-| "uid_of (Creat uid perms path) = uid"
-| "uid_of (Unlink uid path) = uid"
-| "uid_of (Mkdir uid path perms) = uid"
-| "uid_of (Rmdir uid path) = uid"
-| "uid_of (Readdir uid names path) = uid"
+ where
+ "uid_of (Read uid text path) = uid"
+ | "uid_of (Write uid text path) = uid"
+ | "uid_of (Chmod uid perms path) = uid"
+ | "uid_of (Creat uid perms path) = uid"
+ | "uid_of (Unlink uid path) = uid"
+ | "uid_of (Mkdir uid path perms) = uid"
+ | "uid_of (Rmdir uid path) = uid"
+ | "uid_of (Readdir uid names path) = uid"
primrec path_of :: "operation \<Rightarrow> path"
-where
- "path_of (Read uid text path) = path"
-| "path_of (Write uid text path) = path"
-| "path_of (Chmod uid perms path) = path"
-| "path_of (Creat uid perms path) = path"
-| "path_of (Unlink uid path) = path"
-| "path_of (Mkdir uid perms path) = path"
-| "path_of (Rmdir uid path) = path"
-| "path_of (Readdir uid names path) = path"
+ where
+ "path_of (Read uid text path) = path"
+ | "path_of (Write uid text path) = path"
+ | "path_of (Chmod uid perms path) = path"
+ | "path_of (Creat uid perms path) = path"
+ | "path_of (Unlink uid path) = path"
+ | "path_of (Mkdir uid perms path) = path"
+ | "path_of (Rmdir uid path) = path"
+ | "path_of (Readdir uid names path) = path"
text \<open>
\<^medskip>
@@ -340,45 +340,43 @@
inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
-where
- read:
- "root \<midarrow>(Read uid text path)\<rightarrow> root"
- if "access root path uid {Readable} = Some (Val (att, text))"
-| "write":
- "root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
- if "access root path uid {Writable} = Some (Val (att, text'))"
-| chmod:
- "root \<midarrow>(Chmod uid perms path)\<rightarrow>
- update path (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"
- if "access root path uid {} = Some file" and "uid = 0 \<or> uid = owner (attributes file)"
-| creat:
- "root \<midarrow>(Creat uid perms path)\<rightarrow>
- update path (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
- if "path = parent_path @ [name]"
- and "access root parent_path uid {Writable} = Some (Env att parent)"
- and "access root path uid {} = None"
-| unlink:
- "root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
- if "path = parent_path @ [name]"
- and "access root parent_path uid {Writable} = Some (Env att parent)"
- and "access root path uid {} = Some (Val plain)"
-| mkdir:
- "root \<midarrow>(Mkdir uid perms path)\<rightarrow>
- update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
- if "path = parent_path @ [name]"
- and "access root parent_path uid {Writable} = Some (Env att parent)"
- and "access root path uid {} = None"
-|
- rmdir:
- "root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
- if "path = parent_path @ [name]"
- and "access root parent_path uid {Writable} = Some (Env att parent)"
- and "access root path uid {} = Some (Env att' empty)"
-|
- readdir:
- "root \<midarrow>(Readdir uid names path)\<rightarrow> root"
- if "access root path uid {Readable} = Some (Env att dir)"
- and "names = dom dir"
+ where
+ read:
+ "root \<midarrow>(Read uid text path)\<rightarrow> root"
+ if "access root path uid {Readable} = Some (Val (att, text))"
+ | "write":
+ "root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
+ if "access root path uid {Writable} = Some (Val (att, text'))"
+ | chmod:
+ "root \<midarrow>(Chmod uid perms path)\<rightarrow>
+ update path (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"
+ if "access root path uid {} = Some file" and "uid = 0 \<or> uid = owner (attributes file)"
+ | creat:
+ "root \<midarrow>(Creat uid perms path)\<rightarrow>
+ update path (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
+ if "path = parent_path @ [name]"
+ and "access root parent_path uid {Writable} = Some (Env att parent)"
+ and "access root path uid {} = None"
+ | unlink:
+ "root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
+ if "path = parent_path @ [name]"
+ and "access root parent_path uid {Writable} = Some (Env att parent)"
+ and "access root path uid {} = Some (Val plain)"
+ | mkdir:
+ "root \<midarrow>(Mkdir uid perms path)\<rightarrow>
+ update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
+ if "path = parent_path @ [name]"
+ and "access root parent_path uid {Writable} = Some (Env att parent)"
+ and "access root path uid {} = None"
+ | rmdir:
+ "root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
+ if "path = parent_path @ [name]"
+ and "access root parent_path uid {Writable} = Some (Env att parent)"
+ and "access root path uid {} = Some (Env att' empty)"
+ | readdir:
+ "root \<midarrow>(Readdir uid names path)\<rightarrow> root"
+ if "access root path uid {Readable} = Some (Env att dir)"
+ and "names = dom dir"
text \<open>
\<^medskip>
@@ -480,11 +478,10 @@
running processes over a finite amount of time.
\<close>
-inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
- ("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
-where
- nil: "root \<Midarrow>[]\<Rightarrow> root"
-| cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"
+inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" ("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
+ where
+ nil: "root \<Midarrow>[]\<Rightarrow> root"
+ | cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"
text \<open>
\<^medskip>
@@ -750,8 +747,7 @@
fix xs
assume Ps: "\<forall>x \<in> set xs. P x"
assume can_exec: "can_exec root (xs @ [y])"
- then obtain root' root'' where
- xs: "root \<Midarrow>xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''"
+ then obtain root' root'' where xs: "root \<Midarrow>xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''"
by (blast dest: can_exec_snocD)
from init_result have "Q root" by (rule init_inv)
from preserve_inv xs this Ps have "Q root'"
@@ -864,8 +860,7 @@
from inv obtain "file" where "access root bogus_path user\<^sub>1 {} = Some file"
unfolding invariant_def by blast
moreover
- from rmdir obtain att where
- "access root [user\<^sub>1, name\<^sub>1] user\<^sub>1 {} = Some (Env att empty)"
+ from rmdir obtain att where "access root [user\<^sub>1, name\<^sub>1] user\<^sub>1 {} = Some (Env att empty)"
by cases auto
then have "access root ([user\<^sub>1, name\<^sub>1] @ [name\<^sub>2]) user\<^sub>1 {} = empty name\<^sub>2"
by (simp only: access_empty_lookup lookup_append_some) simp
--- a/src/HOL/Word/Bool_List_Representation.thy Thu Nov 24 15:04:05 2016 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Sun Nov 27 20:25:38 2016 +0100
@@ -9,7 +9,7 @@
section "Bool lists and integers"
theory Bool_List_Representation
-imports Complex_Main Bits_Int
+imports Main Bits_Int
begin
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
@@ -1106,7 +1106,7 @@
apply (case_tac m)
apply simp
apply (case_tac "m <= n")
- apply auto
+ apply (auto simp add: div_add_self2)
done
lemma bin_rsplit_len:
--- a/src/Pure/Admin/build_history.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/Admin/build_history.scala Sun Nov 27 20:25:38 2016 +0100
@@ -11,8 +11,6 @@
import java.time.format.DateTimeFormatter
import java.util.Locale
-import scala.collection.mutable
-
object Build_History
{
@@ -105,7 +103,6 @@
def build_history(
hg: Mercurial.Repository,
progress: Progress = Ignore_Progress,
- progress_result: (Process_Result, Path) => Unit = (result: Process_Result, path: Path) => (),
rev: String = default_rev,
isabelle_identifier: String = default_isabelle_identifier,
components_base: String = "",
@@ -259,9 +256,7 @@
first_build = false
- val res = (build_result, log_path.ext("xz"))
- progress_result(res._1, res._2)
- res
+ (build_result, log_path.ext("xz"))
}
}
@@ -353,13 +348,14 @@
val results =
build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier,
- progress_result = (_, log_path) => Output.writeln(log_path.implode, stdout = true),
components_base = components_base, fresh = fresh, nonfree = nonfree,
multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
max_heap = max_heap, more_settings = more_settings, verbose = verbose,
build_tags = build_tags, build_args = build_args)
+ for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true)
+
val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
if (rc != 0) sys.exit(rc)
}
@@ -377,7 +373,6 @@
self_update: Boolean = false,
push_isabelle_home: Boolean = false,
progress: Progress = Ignore_Progress,
- progress_result: (String, Bytes) => Unit = (log_name: String, bytes: Bytes) => (),
options: String = "",
args: String = ""): (List[(String, Bytes)], Process_Result) =
{
@@ -403,6 +398,9 @@
isabelle_hg.id()
}
isabelle_hg.update(rev = rev, clean = true)
+ ssh.execute(
+ ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle"))
+ + " components -a").check
ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
rev
}
@@ -417,24 +415,23 @@
/* Admin/build_history */
- val result = new mutable.ListBuffer[(String, Bytes)]
-
- def progress_stdout(line: String)
- {
- val log = Path.explode(line)
- val res = (log.base.implode, ssh.read_bytes(log))
- ssh.rm(log)
- progress_result(res._1, res._2)
- result += res
- }
-
val process_result =
ssh.execute(
ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
ssh.bash_path(isabelle_repos_other) + " " + args,
- progress_stdout = progress_stdout _,
- progress_stderr = progress.echo(_))
+ progress_stdout = progress.echo(_),
+ progress_stderr = progress.echo(_),
+ strict = false)
- (result.toList, process_result)
+ val result =
+ for (line <- process_result.out_lines)
+ yield {
+ val log = Path.explode(line)
+ val bytes = ssh.read_bytes(log)
+ ssh.rm(log)
+ (log.base.implode, bytes)
+ }
+
+ (result, process_result)
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_polyml.scala Sun Nov 27 20:25:38 2016 +0100
@@ -0,0 +1,224 @@
+/* Title: Pure/Admin/build_polyml.scala
+ Author: Makarius
+
+Build Poly/ML from sources.
+*/
+
+package isabelle
+
+
+object Build_PolyML
+{
+ /** build_polyml **/
+
+ sealed case class Platform_Info(
+ options: List[String] = Nil,
+ options_multilib: List[String] = Nil,
+ setup: String = "",
+ copy_files: List[String] = Nil)
+
+ private val platform_info = Map(
+ "x86-linux" ->
+ Platform_Info(
+ options_multilib =
+ List("--build=i386", "CFLAGS=-m32 -O3", "CXXFLAGS=-m32 -O3", "CCASFLAGS=-m32")),
+ "x86_64-linux" -> Platform_Info(),
+ "x86-darwin" ->
+ Platform_Info(
+ options =
+ List("--build=i686-darwin", "CFLAGS=-arch i686 -O3 -I../libffi/include",
+ "CXXFLAGS=-arch i686 -O3 -I../libffi/include", "CCASFLAGS=-arch i686 -O3",
+ "LDFLAGS=-segprot POLY rwx rwx"),
+ setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin"),
+ "x86_64-darwin" ->
+ Platform_Info(
+ options =
+ List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include",
+ "CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64",
+ "LDFLAGS=-segprot POLY rwx rwx"),
+ setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin"),
+ "x86-windows" ->
+ Platform_Info(
+ options =
+ List("--host=i686-w32-mingw32", "CPPFLAGS=-I/mingw32/include", "--disable-windows-gui"),
+ setup =
+ """PATH=/usr/bin:/bin:/mingw32/bin
+ export CONFIG_SITE=/etc/config.site""",
+ copy_files =
+ List("$MSYS/mingw32/bin/libgcc_s_dw2-1.dll",
+ "$MSYS/mingw32/bin/libgmp-10.dll",
+ "$MSYS/mingw32/bin/libstdc++-6.dll")),
+ "x86_64-windows" ->
+ Platform_Info(
+ options =
+ List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
+ setup =
+ """PATH=/usr/bin:/bin:/mingw64/bin
+ export CONFIG_SITE=/etc/config.site""",
+ copy_files =
+ List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll",
+ "$MSYS/mingw64/bin/libgmp-10.dll",
+ "$MSYS/mingw64/bin/libstdc++-6.dll")))
+
+ def build_polyml(
+ root: Path,
+ sha1_root: Option[Path] = None,
+ progress: Progress = Ignore_Progress,
+ arch_64: Boolean = false,
+ options: List[String] = Nil,
+ msys_root: Option[Path] = None,
+ component_root: Option[Path] = None)
+ {
+ if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
+ error("Bad Poly/ML root directory: " + root)
+
+ val platform =
+ (if (arch_64) "x86_64" else "x86") +
+ (if (Platform.is_windows) "-windows" else if (Platform.is_macos) "-darwin" else "-linux")
+
+ val info =
+ platform_info.get(platform) getOrElse
+ error("Bad platform identifier: " + quote(platform))
+
+ val settings =
+ msys_root match {
+ case None if Platform.is_windows =>
+ error("Windows requires specification of msys root directory")
+ case None => Isabelle_System.settings()
+ case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode)
+ }
+
+
+ /* bash */
+
+ def bash(
+ cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
+ {
+ val script1 =
+ msys_root match {
+ case None => script
+ case Some(msys) =>
+ File.bash_path(msys + Path.explode("usr/bin/bash")) + " -c " + Bash.string(script)
+ }
+ progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo)
+ }
+
+
+ /* component setup */
+
+ component_root match {
+ case None =>
+ case Some(component) =>
+ val etc = component + Path.explode("etc")
+ Isabelle_System.mkdirs(etc)
+ File.copy(Path.explode("~~/Admin/polyml/settings"), etc)
+ File.copy(Path.explode("~~/Admin/polyml/README"), component)
+ }
+
+
+ /* configure and make */
+
+ val configure_options =
+ (if (!arch_64 && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux")
+ info.options_multilib
+ else info.options) ::: List("--enable-intinf-as-int") ::: options
+
+ bash(root,
+ info.setup + "\n" +
+ """
+ [ -f Makefile ] && make distclean
+ {
+ ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
+ rm -rf target
+ make compiler && make compiler && make install
+ } || { echo "Build failed" >&2; exit 2; }
+ """, redirect = true, echo = true).check
+
+ val ldd_files =
+ if (Platform.is_linux) {
+ val libs = bash(root, "ldd target/bin/poly").check.out_lines
+ val Pattern = """\s*libgmp.*=>\s*(\S+).*""".r
+ for (Pattern(lib) <- libs) yield lib
+ }
+ else Nil
+
+
+ /* sha1 library */
+
+ val sha1_files =
+ if (sha1_root.isDefined) {
+ val dir1 = sha1_root.get
+ bash(dir1, "./build " + platform, redirect = true, echo = true).check
+
+ if (component_root.isDefined)
+ Mercurial.repository(dir1).
+ archive(File.standard_path(component_root.get + Path.explode("sha1")))
+
+ val dir2 = dir1 + Path.explode(platform)
+ File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
+ }
+ else Nil
+
+
+ /* target */
+
+ val target = component_root.getOrElse(Path.current) + Path.explode(platform)
+ Isabelle_System.rm_tree(target)
+ Isabelle_System.mkdirs(target)
+
+ for {
+ d <- List("target/bin", "target/lib")
+ dir = root + Path.explode(d)
+ entry <- File.read_dir(dir)
+ } File.move(dir + Path.explode(entry), target)
+
+ for (file <- "~~/Admin/polyml/polyi" :: info.copy_files ::: ldd_files ::: sha1_files)
+ File.copy(Path.explode(file).expand_env(settings), target)
+ }
+
+
+
+ /** Isabelle tool wrapper **/
+
+ val isabelle_tool = Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
+ {
+ Command_Line.tool0 {
+ var component_root: Option[Path] = None
+ var msys_root: Option[Path] = None
+ var arch_64 = false
+ var sha1_root: Option[Path] = None
+
+ val getopts = Getopts("""
+Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
+
+ Options are:
+ -C DIR Isabelle component root directory (for etc/settings ...)
+ -M DIR msys root directory (for Windows)
+ -m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
+ -s DIR sha1 sources, see https://bitbucket.org/isabelle_project/sha1
+
+ Build Poly/ML in the ROOT directory of its sources, with additional
+ CONFIGURE_OPTIONS (e.g. --with-gmp).
+""",
+ "C:" -> (arg => component_root = Some(Path.explode(arg))),
+ "M:" -> (arg => msys_root = Some(Path.explode(arg))),
+ "m:" ->
+ {
+ case "32" | "x86" => arch_64 = false
+ case "64" | "x86_64" => arch_64 = true
+ case bad => error("Bad processor architecture: " + quote(bad))
+ },
+ "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
+
+ val more_args = getopts(args)
+ val (root, options) =
+ more_args match {
+ case root :: options => (Path.explode(root), options)
+ case Nil => getopts.usage()
+ }
+ build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
+ arch_64 = arch_64, options = options, component_root = component_root,
+ msys_root = msys_root)
+ }
+ }, admin = true)
+}
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Nov 27 20:25:38 2016 +0100
@@ -59,8 +59,8 @@
Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
parallel_jobs = 4, remote_mac = "macbroy31", website = Some(new_snapshot))
- if (release_snapshot.is_dir) File.mv(release_snapshot, old_snapshot)
- File.mv(new_snapshot, release_snapshot)
+ if (release_snapshot.is_dir) File.move(release_snapshot, old_snapshot)
+ File.move(new_snapshot, release_snapshot)
Isabelle_System.rm_tree(old_snapshot)
}))
@@ -79,7 +79,7 @@
hg, rev = "build_history_base", fresh = true, build_args = List("HOL"))
} {
result.check
- File.copy(log_path, logger.log_dir + log_path.base)
+ File.move(log_path, logger.log_dir + log_path.base)
}
})
@@ -96,7 +96,11 @@
private val remote_builds =
List(
- List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6 -N", args = "-g timing")),
+ List(Remote_Build("lxbroy8",
+ options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-7a7b742897e9'",
+ args = "-N -g timing")),
+ List(Remote_Build("lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")),
+ List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
List(
Remote_Build("macbroy2", options = "-m32 -M8", args = "-a"),
Remote_Build("macbroy2", options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty"),
@@ -118,19 +122,21 @@
val self_update = !r.shared_home
val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
- def progress_result(log_name: String, bytes: Bytes): Unit =
- Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
+ val (results, _) =
+ Build_History.remote_build_history(ssh,
+ isabelle_repos,
+ isabelle_repos.ext(r.host),
+ isabelle_repos_source = isabelle_release_source,
+ self_update = self_update,
+ push_isabelle_home = push_isabelle_home,
+ options =
+ "-r " + Bash.string(rev) + " -N " + Bash.string(task_name) + " -f " + r.options,
+ args = "-o timeout=10800 " + r.args)
- Build_History.remote_build_history(ssh,
- isabelle_repos,
- isabelle_repos.ext(r.host),
- isabelle_repos_source = isabelle_dev_source,
- self_update = self_update,
- push_isabelle_home = push_isabelle_home,
- progress_result = progress_result _,
- options =
- r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
- args = "-o timeout=10800 " + r.args)
+ for ((log_name, bytes) <- results) {
+ logger.log(Date.now(), log_name)
+ Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
+ }
})
})
}
--- a/src/Pure/General/file.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/General/file.scala Sun Nov 27 20:25:38 2016 +0100
@@ -220,13 +220,13 @@
def write_backup(path: Path, text: CharSequence)
{
- if (path.is_file) mv(path, path.backup)
+ if (path.is_file) move(path, path.backup)
write(path, text)
}
def write_backup2(path: Path, text: CharSequence)
{
- if (path.is_file) mv(path, path.backup2)
+ if (path.is_file) move(path, path.backup2)
write(path, text)
}
@@ -265,8 +265,12 @@
/* move */
- def mv(file1: JFile, file2: JFile): Unit =
- Files.move(file1.toPath, file2.toPath, StandardCopyOption.REPLACE_EXISTING)
+ def move(src: JFile, dst: JFile)
+ {
+ val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
+ if (!eq(src, target))
+ Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
+ }
- def mv(path1: Path, path2: Path): Unit = mv(path1.file, path2.file)
+ def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file)
}
--- a/src/Pure/General/mercurial.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/General/mercurial.scala Sun Nov 27 20:25:38 2016 +0100
@@ -54,7 +54,7 @@
case None => root.is_dir
case Some(ssh) => ssh.is_dir(root)
}
- if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg }
+ if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
else clone_repository(source, root, options = "--noupdate", ssh = ssh)
}
@@ -92,6 +92,9 @@
}
}
+ def archive(target: String, rev: String = "", options: String = ""): Unit =
+ hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
+
def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
hg.command("heads", opt_template(template), options).check.out_lines
--- a/src/Pure/General/symbol.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/General/symbol.scala Sun Nov 27 20:25:38 2016 +0100
@@ -197,7 +197,7 @@
}
- /* text chunks */
+ /* symbolic text chunks -- without actual text */
object Text_Chunk
{
--- a/src/Pure/Isar/parse.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/Isar/parse.scala Sun Nov 27 20:25:38 2016 +0100
@@ -64,12 +64,13 @@
def string: Parser[String] = atom("string", _.is_string)
def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
def name: Parser[String] = atom("name", _.is_name)
+ def embedded: Parser[String] = atom("embedded content", _.is_embedded)
def text: Parser[String] = atom("text", _.is_text)
def ML_source: Parser[String] = atom("ML source", _.is_text)
def document_source: Parser[String] = atom("document source", _.is_text)
def path: Parser[String] =
- atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
+ atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
def theory_name: Parser[String] =
atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
--- a/src/Pure/Isar/token.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/Isar/token.scala Sun Nov 27 20:25:38 2016 +0100
@@ -242,6 +242,11 @@
kind == Token.Kind.SYM_IDENT ||
kind == Token.Kind.STRING ||
kind == Token.Kind.NAT
+ def is_embedded: Boolean = is_name ||
+ kind == Token.Kind.CARTOUCHE ||
+ kind == Token.Kind.VAR ||
+ kind == Token.Kind.TYPE_IDENT ||
+ kind == Token.Kind.TYPE_VAR
def is_text: Boolean = is_name || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
def is_space: Boolean = kind == Token.Kind.SPACE
def is_comment: Boolean = kind == Token.Kind.COMMENT
--- a/src/Pure/PIDE/command.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/PIDE/command.scala Sun Nov 27 20:25:38 2016 +0100
@@ -322,7 +322,7 @@
private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
if (tokens.exists({ case (t, _) => t.is_command })) {
tokens.dropWhile({ case (t, _) => !t.is_command }).
- collectFirst({ case (t, i) if t.is_name => (t.content, i) })
+ collectFirst({ case (t, i) if t.is_embedded => (t.content, i) })
}
else None
--- a/src/Pure/PIDE/editor.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/PIDE/editor.scala Sun Nov 27 20:25:38 2016 +0100
@@ -12,6 +12,7 @@
def session: Session
def flush(hidden: Boolean = true): Unit
def invoke(): Unit
+ def invoke_generated(): Unit
def current_context: Context
def current_node(context: Context): Option[Document.Node.Name]
def current_node_snapshot(context: Context): Option[Document.Snapshot]
--- a/src/Pure/System/isabelle_system.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Sun Nov 27 20:25:38 2016 +0100
@@ -107,12 +107,14 @@
dump.deleteOnExit
try {
val cmd1 =
- if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l") else Nil
- val cmd2 =
- List(isabelle_root1 + JFile.separator + "bin" + JFile.separator + "isabelle",
- "getenv", "-d", dump.toString)
+ if (Platform.is_windows)
+ List(cygwin_root1 + "\\bin\\bash", "-l",
+ File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
+ else
+ List(isabelle_root1 + "/bin/isabelle")
+ val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
- val (output, rc) = process_output(process(cmd1 ::: cmd2, env = env, redirect = true))
+ val (output, rc) = process_output(process(cmd, env = env, redirect = true))
if (rc != 0) error(output)
val entries =
--- a/src/Pure/System/isabelle_tool.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/System/isabelle_tool.scala Sun Nov 27 20:25:38 2016 +0100
@@ -101,6 +101,7 @@
List(
Build.isabelle_tool,
Build_Doc.isabelle_tool,
+ Build_PolyML.isabelle_tool,
Build_Stats.isabelle_tool,
Check_Sources.isabelle_tool,
Doc.isabelle_tool,
--- a/src/Pure/System/numa.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/System/numa.scala Sun Nov 27 20:25:38 2016 +0100
@@ -26,7 +26,7 @@
}
if (numa_nodes_linux.is_file) {
- Library.space_explode(',', Library.trim_line(File.read(numa_nodes_linux))).flatMap(read(_))
+ Library.space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
}
else Nil
}
--- a/src/Pure/System/platform.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/System/platform.scala Sun Nov 27 20:25:38 2016 +0100
@@ -14,6 +14,7 @@
{
/* main OS variants */
+ val is_linux = System.getProperty("os.name", "") == "Linux"
val is_macos = System.getProperty("os.name", "") == "Mac OS X"
val is_windows = System.getProperty("os.name", "").startsWith("Windows")
--- a/src/Pure/Thy/latex.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/Thy/latex.ML Sun Nov 27 20:25:38 2016 +0100
@@ -106,21 +106,30 @@
| Symbol.Malformed s => error (Symbol.malformed_msg s)
| Symbol.EOF => error "Bad EOF symbol");
+val scan_latex_length =
+ Scan.many1 (fn (s, _) => Symbol.not_eof s andalso not (is_latex_control s))
+ >> (Symbol.length o map Symbol_Pos.symbol) ||
+ Scan.one (is_latex_control o Symbol_Pos.symbol) --
+ Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
+
fun scan_latex known =
Scan.one (is_latex_control o Symbol_Pos.symbol) |--
Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
-fun read_latex known syms =
- (case Scan.read Symbol_Pos.stopper (Scan.repeat (scan_latex known))
- (map (rpair Position.none) syms) of
- SOME ss => implode ss
- | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)));
+fun read scan syms =
+ Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
in
+fun length_symbols syms =
+ fold Integer.add (these (read scan_latex_length syms)) 0;
+
fun output_known_symbols known syms =
- if exists is_latex_control syms then read_latex known syms
+ if exists is_latex_control syms then
+ (case read (scan_latex known) syms of
+ SOME ss => implode ss
+ | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
else implode (map (output_known_sym known) syms);
val output_symbols = output_known_symbols (K true, K true);
@@ -201,7 +210,7 @@
fun latex_output str =
let val syms = Symbol.explode str
- in (output_symbols syms, Symbol.length syms) end;
+ in (output_symbols syms, length_symbols syms) end;
fun latex_markup (s, _) =
if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
--- a/src/Pure/Tools/build.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/Tools/build.scala Sun Nov 27 20:25:38 2016 +0100
@@ -751,7 +751,7 @@
Build and manage Isabelle sessions, depending on implicit settings:
-""" + Library.prefix_lines(" ", Build_Log.Settings.show()),
+""" + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n",
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"N" -> (_ => numa_shuffling = true),
"R" -> (_ => requirements = true),
--- a/src/Pure/build-jars Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/build-jars Sun Nov 27 20:25:38 2016 +0100
@@ -12,6 +12,7 @@
Admin/build_doc.scala
Admin/build_history.scala
Admin/build_log.scala
+ Admin/build_polyml.scala
Admin/build_release.scala
Admin/build_stats.scala
Admin/check_sources.scala
--- a/src/Pure/theory.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Pure/theory.ML Sun Nov 27 20:25:38 2016 +0100
@@ -220,9 +220,6 @@
fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
let
- val thy = Proof_Context.theory_of ctxt;
- val consts = Sign.consts_of thy;
-
fun prep (item, args) =
(case fold Term.add_tvarsT args [] of
[] => (item, map Logic.varifyT_global args)
--- a/src/Tools/Code/code_scala.ML Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Tools/Code/code_scala.ML Sun Nov 27 20:25:38 2016 +0100
@@ -443,7 +443,7 @@
else if c = "\\" then "\\\\"
else let val k = ord c
in if k < 32 orelse k > 126
- then "\\u" ^ align_right "0" 4 (radixstring (8, "0", k)) else c end
+ then "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX k) else c end
fun numeral_scala k =
if ~2147483647 < k andalso k <= 2147483647
then signed_string_of_int k
--- a/src/Tools/jEdit/src/document_view.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sun Nov 27 20:25:38 2016 +0100
@@ -111,7 +111,7 @@
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
// no robust_body
- PIDE.editor.invoke()
+ PIDE.editor.invoke_generated()
}
}
--- a/src/Tools/jEdit/src/isabelle.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sun Nov 27 20:25:38 2016 +0100
@@ -338,9 +338,9 @@
JEdit_Lib.buffer_edit(buffer) {
if (padding) {
text_area.moveCaretPosition(start + range.length)
+ val start_line = text_area.getCaretLine + 1
text_area.setSelectedText("\n" + text)
val end_line = text_area.getCaretLine
- val start_line = end_line - split_lines(text).length
buffer.indentLines(start_line, end_line)
}
else {
--- a/src/Tools/jEdit/src/jedit_editor.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Nov 27 20:25:38 2016 +0100
@@ -44,10 +44,14 @@
session.update(doc_blobs, edits)
}
- private val delay_flush =
+ private val delay1_flush =
GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
- def invoke(): Unit = delay_flush.invoke()
+ private val delay2_flush =
+ GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
+
+ def invoke(): Unit = delay1_flush.invoke()
+ def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
def stable_tip_version(): Option[Document.Version] =
GUI_Thread.require {
--- a/src/Tools/jEdit/src/plugin.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Nov 27 20:25:38 2016 +0100
@@ -125,7 +125,7 @@
else if (plugin != null) plugin.delay_init.invoke()
}
- PIDE.editor.invoke()
+ PIDE.editor.invoke_generated()
}
}
@@ -223,7 +223,7 @@
if (PIDE.options.bool("jedit_auto_resolve")) {
PIDE.editor.stable_tip_version() match {
case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node)
- case None => Nil
+ case None => delay_load.invoke(); Nil
}
}
else Nil
@@ -263,7 +263,7 @@
}
}
- lazy val delay_load =
+ private lazy val delay_load =
GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() }
--- a/src/Tools/jEdit/src/text_structure.scala Thu Nov 24 15:04:05 2016 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala Sun Nov 27 20:25:38 2016 +0100
@@ -44,7 +44,7 @@
private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open
private val keyword_close = Keyword.proof_close
- def apply(buffer: JEditBuffer, current_line: Int, prev_line: Int, prev_prev_line: Int,
+ def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
actions: java.util.List[IndentAction])
{
Isabelle.buffer_syntax(buffer) match {
@@ -68,6 +68,11 @@
case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
}
+ val prev_line: Int =
+ Range.inclusive(current_line - 1, 0, -1).find(line =>
+ Token_Markup.Line_Context.prev(buffer, line).get_context == Scan.Finished &&
+ !Token_Markup.Line_Context.next(buffer, line).structure.improper) getOrElse -1
+
def prev_line_command: Option[Token] =
nav.reverse_iterator(prev_line, 1).
collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok })
@@ -135,33 +140,36 @@
else 0
val indent =
- line_head(current_line) match {
- case None => indent_structure + indent_brackets + indent_extra
- case Some(info @ Text.Info(range, tok)) =>
- if (tok.is_begin ||
- keywords.is_before_command(tok) ||
- keywords.is_command(tok, Keyword.theory)) 0
- else if (keywords.is_command(tok, Keyword.proof_enclose))
- indent_structure + script_indent(info) - indent_offset(tok)
- else if (keywords.is_command(tok, Keyword.proof))
- (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
- else if (tok.is_command) indent_structure - indent_offset(tok)
- else {
- prev_line_command match {
- case None =>
- val extra =
- (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
- case (true, true) | (false, false) => 0
- case (true, false) => - indent_extra
- case (false, true) => indent_extra
- }
- line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
- case Some(prev_tok) =>
- indent_structure + indent_brackets + indent_size - indent_offset(tok) -
- indent_offset(prev_tok) - indent_indent(prev_tok)
- }
- }
+ if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
+ line_head(current_line) match {
+ case None => indent_structure + indent_brackets + indent_extra
+ case Some(info @ Text.Info(range, tok)) =>
+ if (tok.is_begin ||
+ keywords.is_before_command(tok) ||
+ keywords.is_command(tok, Keyword.theory)) 0
+ else if (keywords.is_command(tok, Keyword.proof_enclose))
+ indent_structure + script_indent(info) - indent_offset(tok)
+ else if (keywords.is_command(tok, Keyword.proof))
+ (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
+ else if (tok.is_command) indent_structure - indent_offset(tok)
+ else {
+ prev_line_command match {
+ case None =>
+ val extra =
+ (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
+ case (true, true) | (false, false) => 0
+ case (true, false) => - indent_extra
+ case (false, true) => indent_extra
+ }
+ line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
+ case Some(prev_tok) =>
+ indent_structure + indent_brackets + indent_size - indent_offset(tok) -
+ indent_offset(prev_tok) - indent_indent(prev_tok)
+ }
+ }
+ }
}
+ else line_indent(current_line)
actions.clear()
actions.add(new IndentAction.AlignOffset(indent max 0))