merged
authorwenzelm
Sun Nov 27 20:25:38 2016 +0100 (2016-11-27)
changeset 645291c0b93961cb1
parent 64449 8c44dfb4ca8a
parent 64528 a67edee6b1fa
child 64530 a720c3911308
merged
NEWS
     1.1 --- a/.hgtags	Thu Nov 24 15:04:05 2016 +0100
     1.2 +++ b/.hgtags	Sun Nov 27 20:25:38 2016 +0100
     1.3 @@ -34,3 +34,6 @@
     1.4  d3996d5873ddcf1115ec8d3d511a0bb5dbd1cfc4 Isabelle2016
     1.5  666c7475f4f7e9ba46c59170026230787c504ca7 Isabelle2016-1-RC0
     1.6  9ee2480d10b7404683aa7f4c3a30d44cbb6a21b9 Isabelle2016-1-RC1
     1.7 +2bf4fdcebd495516947e5e85f3b3db01d5fbe1a4 Isabelle2016-1-RC2
     1.8 +51be997d0698583bf2d3f5a99f37381a146d3a6c Isabelle2016-1-RC3
     1.9 +49708cffb98dc6ced89f66b10662e6af2808bebd Isabelle2016-1-RC4
     2.1 --- a/Admin/Release/CHECKLIST	Thu Nov 24 15:04:05 2016 +0100
     2.2 +++ b/Admin/Release/CHECKLIST	Sun Nov 27 20:25:38 2016 +0100
     2.3 @@ -88,6 +88,9 @@
     2.4  - Admin/cronjob/self_update:
     2.5    http://bitbucket.org/isabelle_project/isabelle-release
     2.6  
     2.7 +- src/Pure/Admin/isabelle_cronjon.scala:
     2.8 +  isabelle_repos_source = isabelle_release_source
     2.9 +
    2.10  
    2.11  Post-release
    2.12  ============
     3.1 --- a/Admin/components/components.sha1	Thu Nov 24 15:04:05 2016 +0100
     3.2 +++ b/Admin/components/components.sha1	Sun Nov 27 20:25:38 2016 +0100
     3.3 @@ -115,6 +115,7 @@
     3.4  377e36efb8608e6c828c7718d890e97fde2006a4  linux_app-20131007.tar.gz
     3.5  0aab4f73ff7f5e36f33276547e10897e1e56fb1d  macos_app-20130716.tar.gz
     3.6  ad5d0e640ce3609a885cecab645389a2204e03bb  macos_app-20150916.tar.gz
     3.7 +26df569cee9c2fd91b9ac06714afd43f3b37a1dd  nunchaku-0.3.tar.gz
     3.8  1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb  polyml-5.4.1.tar.gz
     3.9  a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56  polyml-5.5.0-1.tar.gz
    3.10  7d604a99355efbfc1459d80db3279ffa7ade3e39  polyml-5.5.0-2.tar.gz
    3.11 @@ -136,6 +137,7 @@
    3.12  bd6a448f0e0d5787747f4f30ca661f9c1868e4a7  polyml-5.6-20151223.tar.gz
    3.13  5b70c12c95a90d858f90c1945011289944ea8e17  polyml-5.6-20160118.tar.gz
    3.14  5b19dc93082803b82aa553a5cfb3e914606c0ffd  polyml-5.6.tar.gz
    3.15 +853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e  polyml-test-7a7b742897e9.tar.gz
    3.16  8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
    3.17  847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
    3.18  8e0b2b432755ef11d964e20637d1bc567d1c0477  ProofGeneral-4.2-1.tar.gz
     4.1 --- a/Admin/components/main	Thu Nov 24 15:04:05 2016 +0100
     4.2 +++ b/Admin/components/main	Sun Nov 27 20:25:38 2016 +0100
     4.3 @@ -9,6 +9,7 @@
     4.4  jfreechart-1.0.14-1
     4.5  jortho-1.0-2
     4.6  kodkodi-1.5.2
     4.7 +nunchaku-0.3
     4.8  polyml-5.6-1
     4.9  scala-2.11.8
    4.10  ssh-java-20161009
     5.1 --- a/Admin/cronjob/main	Thu Nov 24 15:04:05 2016 +0100
     5.2 +++ b/Admin/cronjob/main	Sun Nov 27 20:25:38 2016 +0100
     5.3 @@ -9,4 +9,4 @@
     5.4  export ISABELLE_IDENTIFIER="cronjob"
     5.5  "$THIS/../build" jars_fresh || exit $?
     5.6  
     5.7 -exec "$THIS/../../bin/isabelle_java" "-Duser.timezone=Europe/Berlin" isabelle.Isabelle_Cronjob "$@"
     5.8 +exec "$THIS/../../bin/isabelle_java" isabelle.Isabelle_Cronjob "$@"
     6.1 --- a/Admin/cronjob/self_update	Thu Nov 24 15:04:05 2016 +0100
     6.2 +++ b/Admin/cronjob/self_update	Sun Nov 27 20:25:38 2016 +0100
     6.3 @@ -10,5 +10,5 @@
     6.4  cd "$HOME/cronjob"
     6.5  mkdir -p run log
     6.6  
     6.7 -hg -R isabelle pull "http://isabelle.in.tum.de/repos/isabelle" -q || echo "self_update pull failed"
     6.8 +hg -R isabelle pull "http://bitbucket.org/isabelle_project/isabelle-release" -q || echo "self_update pull failed"
     6.9  hg -R isabelle update -C -q || echo "self_update update failed"
     7.1 --- a/NEWS	Thu Nov 24 15:04:05 2016 +0100
     7.2 +++ b/NEWS	Sun Nov 27 20:25:38 2016 +0100
     7.3 @@ -70,6 +70,11 @@
     7.4  
     7.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     7.6  
     7.7 +* More aggressive flushing of machine-generated input, according to
     7.8 +system option editor_generated_input_delay (in addition to existing
     7.9 +editor_input_delay for regular user edits). This may affect overall PIDE
    7.10 +reactivity and CPU usage.
    7.11 +
    7.12  * Syntactic indentation according to Isabelle outer syntax. Action
    7.13  "indent-lines" (shortcut C+i) indents the current line according to
    7.14  command keywords and some command substructure. Action
    7.15 @@ -99,7 +104,7 @@
    7.16  * Highlighting of entity def/ref positions wrt. cursor.
    7.17  
    7.18  * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
    7.19 -occurences of the formal entity at the caret position. This facilitates
    7.20 +occurrences of the formal entity at the caret position. This facilitates
    7.21  systematic renaming.
    7.22  
    7.23  * PIDE document markup works across multiple Isar commands, e.g. the
    7.24 @@ -910,11 +915,12 @@
    7.25  support for monotonicity and continuity in chain-complete partial orders
    7.26  and about admissibility conditions for fixpoint inductions.
    7.27  
    7.28 -* Session HOL-Library: theory Polynomial contains also derivation of
    7.29 -polynomials but not gcd/lcm on polynomials over fields. This has been
    7.30 -moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave
    7.31 -way for a possible future different type class instantiation for
    7.32 -polynomials over factorial rings. INCOMPATIBILITY.
    7.33 +* Session HOL-Library: theory Library/Polynomial contains also
    7.34 +derivation of polynomials (formerly in Library/Poly_Deriv) but not
    7.35 +gcd/lcm on polynomials over fields. This has been moved to a separate
    7.36 +theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible
    7.37 +future different type class instantiation for polynomials over factorial
    7.38 +rings. INCOMPATIBILITY.
    7.39  
    7.40  * Session HOL-Library: theory Sublist provides function "prefixes" with
    7.41  the following renaming
     8.1 --- a/etc/options	Thu Nov 24 15:04:05 2016 +0100
     8.2 +++ b/etc/options	Sun Nov 27 20:25:38 2016 +0100
     8.3 @@ -144,6 +144,9 @@
     8.4  public option editor_input_delay : real = 0.3
     8.5    -- "delay for user input (text edits, cursor movement etc.)"
     8.6  
     8.7 +public option editor_generated_input_delay : real = 1.0
     8.8 +  -- "delay for machine-generated input that may outperform user edits"
     8.9 +
    8.10  public option editor_output_delay : real = 0.1
    8.11    -- "delay for prover output (markup, common messages etc.)"
    8.12  
     9.1 --- a/lib/texinputs/isabelle.sty	Thu Nov 24 15:04:05 2016 +0100
     9.2 +++ b/lib/texinputs/isabelle.sty	Sun Nov 27 20:25:38 2016 +0100
     9.3 @@ -73,7 +73,7 @@
     9.4  \newcommand{\isadigit}[1]{#1}
     9.5  
     9.6  \newcommand{\isachardefaults}{%
     9.7 -\def\isacharbell{\isamath{\bigbox}}  %requires stmaryrd
     9.8 +\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
     9.9  \chardef\isacharbang=`\!%
    9.10  \chardef\isachardoublequote=`\"%
    9.11  \chardef\isachardoublequoteopen=`\"%
    10.1 --- a/src/Doc/Implementation/ML.thy	Thu Nov 24 15:04:05 2016 +0100
    10.2 +++ b/src/Doc/Implementation/ML.thy	Sun Nov 27 20:25:38 2016 +0100
    10.3 @@ -138,7 +138,7 @@
    10.4    @{ML_text foo1}, @{ML_text foo42}.
    10.5  \<close>
    10.6  
    10.7 -paragraph\<open>Scopes.\<close>
    10.8 +paragraph \<open>Scopes.\<close>
    10.9  text \<open>
   10.10    Apart from very basic library modules, ML structures are not ``opened'', but
   10.11    names are referenced with explicit qualification, as in @{ML
   10.12 @@ -1192,11 +1192,43 @@
   10.13  text %mlantiq \<open>
   10.14    \begin{matharray}{rcl}
   10.15    @{ML_antiquotation_def "assert"} & : & \<open>ML_antiquotation\<close> \\
   10.16 +  @{ML_antiquotation_def "undefined"} & : & \<open>ML_antiquotation\<close> \\
   10.17    \end{matharray}
   10.18  
   10.19    \<^descr> \<open>@{assert}\<close> inlines a function @{ML_type "bool -> unit"} that raises @{ML
   10.20    Fail} if the argument is @{ML false}. Due to inlining the source position of
   10.21    failed assertions is included in the error output.
   10.22 +
   10.23 +  \<^descr> \<open>@{undefined}\<close> inlines @{verbatim raise}~@{ML Match}, i.e.\ the ML program
   10.24 +  behaves as in some function application of an undefined case.
   10.25 +\<close>
   10.26 +
   10.27 +text %mlex \<open>
   10.28 +  The ML function @{ML undefined} is defined in \<^file>\<open>~~/src/Pure/library.ML\<close>
   10.29 +  as follows:
   10.30 +\<close>
   10.31 +
   10.32 +ML \<open>fun undefined _ = raise Match\<close>
   10.33 +
   10.34 +text \<open>
   10.35 +  \<^medskip>
   10.36 +  The following variant uses the antiquotation @{ML_antiquotation undefined}
   10.37 +  instead:
   10.38 +\<close>
   10.39 +
   10.40 +ML \<open>fun undefined _ = @{undefined}\<close>
   10.41 +
   10.42 +text \<open>
   10.43 +  \<^medskip>
   10.44 +  Here is the same, using control-symbol notation for the antiquotation, with
   10.45 +  special rendering of \<^verbatim>\<open>\<^undefined>\<close>:
   10.46 +\<close>
   10.47 +
   10.48 +ML \<open>fun undefined _ = \<^undefined>\<close>
   10.49 +
   10.50 +text \<open>
   10.51 +  \medskip Semantically, all forms are equivalent to a function definition
   10.52 +  without any clauses, but that is syntactically not allowed in ML.
   10.53  \<close>
   10.54  
   10.55  
    11.1 --- a/src/Doc/Isar_Ref/Framework.thy	Thu Nov 24 15:04:05 2016 +0100
    11.2 +++ b/src/Doc/Isar_Ref/Framework.thy	Sun Nov 27 20:25:38 2016 +0100
    11.3 @@ -485,11 +485,58 @@
    11.4    entities of Pure (propositions, facts, and goals). The Isar proof language
    11.5    allows to organize reasoning within the underlying rule calculus of Pure,
    11.6    but Isar is not another logical calculus. Isar merely imposes certain
    11.7 -  structure and policies on Pure inferences.
    11.8 +  structure and policies on Pure inferences. The main grammar of the Isar
    11.9 +  proof language is given in \figref{fig:isar-syntax}.
   11.10  
   11.11 -  Isar is intended as an exercise in minimalism. Approximately half of the
   11.12 -  language is introduced as primitive, the rest defined as derived concepts.
   11.13 -  The grammar in \appref{ap:main-grammar} describes the core language
   11.14 +  \begin{figure}[htb]
   11.15 +  \begin{center}
   11.16 +  \begin{tabular}{rcl}
   11.17 +    \<open>main\<close> & \<open>=\<close> & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
   11.18 +    & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if name: props for vars\<close> \\
   11.19 +    & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
   11.20 +    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
   11.21 +    & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
   11.22 +    & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
   11.23 +    & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
   11.24 +    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
   11.25 +    & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
   11.26 +    & & \quad\<^theory_text>\<open>obtains (name) clause "\<^bold>|" \<dots> "proof"\<close> \\
   11.27 +    \<open>proof\<close> & \<open>=\<close> & \<^theory_text>\<open>"refinement\<^sup>* proper_proof"\<close> \\
   11.28 +    \<open>refinement\<close> & \<open>=\<close> &  \<^theory_text>\<open>apply method\<close> \\
   11.29 +    & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
   11.30 +    & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
   11.31 +    & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
   11.32 +    & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
   11.33 +    \<open>proper_proof\<close> & \<open>=\<close> & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
   11.34 +    & \<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> \\
   11.35 +    \<open>statement\<close> & \<open>=\<close> & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>next\<close> \\
   11.36 +    & \<open>|\<close> & \<^theory_text>\<open>note name = thms\<close> \\
   11.37 +    & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
   11.38 +    & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
   11.39 +    & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\
   11.40 +    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\
   11.41 +    & \<open>|\<close> & \<^theory_text>\<open>presume name: props if props for vars\<close> \\
   11.42 +    & \<open>|\<close> & \<^theory_text>\<open>define clause\<close> \\
   11.43 +    & \<open>|\<close> & \<^theory_text>\<open>case name: "case"\<close> \\
   11.44 +    & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
   11.45 +    & \<open>|\<close> & \<^theory_text>\<open>from thms goal\<close> \\
   11.46 +    & \<open>|\<close> & \<^theory_text>\<open>with thms goal\<close> \\
   11.47 +    & \<open>|\<close> & \<^theory_text>\<open>also\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>finally goal\<close> \\
   11.48 +    & \<open>|\<close> & \<^theory_text>\<open>moreover\<close>~~~\<open>|\<close>~~~\<^theory_text>\<open>ultimately goal\<close> \\
   11.49 +    \<open>goal\<close> & \<open>=\<close> & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\
   11.50 +    & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\
   11.51 +    & \<open>|\<close> & \<^theory_text>\<open>show name: props when name: props for vars "proof"\<close> \\
   11.52 +    & \<open>|\<close> & \<^theory_text>\<open>consider (name) clause "\<^bold>|" \<dots> "proof"\<close> \\
   11.53 +    & \<open>|\<close> & \<^theory_text>\<open>obtain (name) clause "proof"\<close> \\
   11.54 +    \<open>clause\<close> & \<open>=\<close> & \<^theory_text>\<open>vars where name: props if props for vars\<close> \\
   11.55 +  \end{tabular}
   11.56 +  \end{center}
   11.57 +  \caption{Main grammar of the Isar proof language}\label{fig:isar-syntax}
   11.58 +  \end{figure}
   11.59 +
   11.60 +  The construction of the Isar proof language proceeds in a bottom-up fashion,
   11.61 +  as an exercise in purity and minimalism. The grammar in
   11.62 +  \appref{ap:main-grammar} describes the primitive parts of the core language
   11.63    (category \<open>proof\<close>), which is embedded into the main outer theory syntax via
   11.64    elements that require a proof (e.g.\ \<^theory_text>\<open>theorem\<close>, \<^theory_text>\<open>lemma\<close>, \<^theory_text>\<open>function\<close>,
   11.65    \<^theory_text>\<open>termination\<close>).
    12.1 --- a/src/Doc/Isar_Ref/document/root.tex	Thu Nov 24 15:04:05 2016 +0100
    12.2 +++ b/src/Doc/Isar_Ref/document/root.tex	Sun Nov 27 20:25:38 2016 +0100
    12.3 @@ -64,6 +64,7 @@
    12.4  \chapter*{Preface}
    12.5  \input{Preface.tex}
    12.6  \tableofcontents
    12.7 +\listoffigures
    12.8  \clearfirst
    12.9  
   12.10  \part{Basic Concepts}
    13.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Nov 24 15:04:05 2016 +0100
    13.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 27 20:25:38 2016 +0100
    13.3 @@ -141,8 +141,7 @@
    13.4    done with the usual care for such an open bazaar of contributions. Arbitrary
    13.5    combinations of add-on features are apt to cause problems. It is advisable
    13.6    to start with the default configuration of Isabelle/jEdit and develop some
    13.7 -  understanding how it is supposed to work, before loading too many other
    13.8 -  plugins.
    13.9 +  sense how it is meant to work, before loading too many other plugins.
   13.10  
   13.11    \<^medskip>
   13.12    The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs
   13.13 @@ -207,12 +206,15 @@
   13.14    first start of the editor; afterwards the keymap file takes precedence and
   13.15    is no longer affected by change of default properties.
   13.16  
   13.17 -  This subtle difference of jEdit keymaps versus properties is relevant for
   13.18 -  Isabelle/jEdit due to various fine-tuning of global defaults, with
   13.19 -  additional keyboard shortcuts for Isabelle-specific functionality. Users may
   13.20 -  change their keymap later, but need to copy some keyboard shortcuts manually
   13.21 -  (see also @{path "$JEDIT_SETTINGS/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in
   13.22 -  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>).
   13.23 +  Users may change their keymap later, but need to keep its content @{path
   13.24 +  "$JEDIT_SETTINGS/keymaps"} in sync with \<^verbatim>\<open>shortcut\<close> properties in
   13.25 +  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
   13.26 +
   13.27 +  \<^medskip>
   13.28 +  The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
   13.29 +  Isabelle keymap changes that are in conflict with the current jEdit keymap;
   13.30 +  non-conflicting changes are always applied implicitly. This action is
   13.31 +  automatically invoked on Isabelle/jEdit startup.
   13.32  \<close>
   13.33  
   13.34  
   13.35 @@ -292,7 +294,7 @@
   13.36  
   13.37    The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
   13.38    different server name. The default server name is the official distribution
   13.39 -  name (e.g.\ \<^verbatim>\<open>Isabelle2016\<close>). Thus @{tool jedit_client} can connect to the
   13.40 +  name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<close>). Thus @{tool jedit_client} can connect to the
   13.41    Isabelle desktop application without further options.
   13.42  
   13.43    The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
   13.44 @@ -694,14 +696,44 @@
   13.45  \<close>
   13.46  
   13.47  
   13.48 +section \<open>Indentation\<close>
   13.49 +
   13.50 +text \<open>
   13.51 +  Isabelle/jEdit augments the existing indentation facilities of jEdit to take
   13.52 +  the structure of theory and proof texts into account. There is also special
   13.53 +  support for unstructured proof scripts.
   13.54 +
   13.55 +    \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar.
   13.56 +
   13.57 +    Action @{action "indent-lines"} (shortcut \<^verbatim>\<open>C+i\<close>) indents the current line
   13.58 +    according to command keywords and some command substructure: this
   13.59 +    approximation may need further manual tuning.
   13.60 +
   13.61 +    Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the old
   13.62 +    and the new line according to command keywords only: this leads to precise
   13.63 +    alignment of the main Isar language elements. This depends on option
   13.64 +    @{system_option_def "jedit_indent_newline"} (enabled by default).
   13.65 +
   13.66 +    \<^descr>[Semantic indentation] adds additional white space to unstructured proof
   13.67 +    scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
   13.68 +    of ongoing document processing and may thus lag behind, when the user is
   13.69 +    editing too quickly; see also option @{system_option_def
   13.70 +    "jedit_script_indent"} and @{system_option_def
   13.71 +    "jedit_script_indent_limit"}.
   13.72 +
   13.73 +  The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
   13.74 +  Isabelle / General\<close>.
   13.75 +\<close>
   13.76 +
   13.77 +
   13.78  section \<open>SideKick parsers \label{sec:sidekick}\<close>
   13.79  
   13.80  text \<open>
   13.81    The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer
   13.82    structure in a tree view. Isabelle/jEdit provides SideKick parsers for its
   13.83 -  main mode for theory files, as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file
   13.84 -  (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system \<^verbatim>\<open>options\<close>, and
   13.85 -  Bib{\TeX} files (\secref{sec:bibtex}).
   13.86 +  main mode for theory files, ML files, as well as some minor modes for the
   13.87 +  \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system
   13.88 +  \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}).
   13.89  
   13.90    \begin{figure}[!htb]
   13.91    \begin{center}
   13.92 @@ -711,6 +743,19 @@
   13.93    \label{fig:sidekick}
   13.94    \end{figure}
   13.95  
   13.96 +  The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides a
   13.97 +  tree-view on the formal document structure, with section headings at the top
   13.98 +  and formal specification elements at the bottom. The alternative parser
   13.99 +  \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>
  13.100 +  end\<close> structure.
  13.101 +
  13.102 +  \<^medskip>
  13.103 +  Isabelle/ML files are structured according to semi-formal comments that are
  13.104 +  explained in @{cite "isabelle-implementation"}. This outline is turned into
  13.105 +  a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a
  13.106 +  folding mode of the same name, for hierarchic text folds within ML files.
  13.107 +
  13.108 +  \<^medskip>
  13.109    The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpreted
  13.110    markup tree of the PIDE document model of the current buffer. This is
  13.111    occasionally useful for informative purposes, but the amount of displayed
  13.112 @@ -1155,6 +1200,40 @@
  13.113  \<close>
  13.114  
  13.115  
  13.116 +section \<open>Formal scopes and semantic selection\<close>
  13.117 +
  13.118 +text \<open>
  13.119 +  Formal entities are semantically annotated in the source text as explained
  13.120 +  in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the
  13.121 +  defining position with all its referencing positions. This correspondence is
  13.122 +  highlighted in the text according to the cursor position, see also
  13.123 +  \figref{fig:scope1}. Here the referencing positions are rendered with an
  13.124 +  additional border, in reminiscence to a hyperlink: clicking there moves the
  13.125 +  cursor to the original defining position.
  13.126 +
  13.127 +  \begin{figure}[!htb]
  13.128 +  \begin{center}
  13.129 +  \includegraphics[scale=0.5]{scope1}
  13.130 +  \end{center}
  13.131 +  \caption{Scope of formal entity: defining vs.\ referencing positions}
  13.132 +  \label{fig:scope1}
  13.133 +  \end{figure}
  13.134 +
  13.135 +  The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
  13.136 +  supports semantic selection of all occurrences of the formal entity at the
  13.137 +  caret position. This facilitates systematic renaming, using regular jEdit
  13.138 +  editing of a multi-selection, see also \figref{fig:scope2}.
  13.139 +
  13.140 +  \begin{figure}[!htb]
  13.141 +  \begin{center}
  13.142 +  \includegraphics[scale=0.5]{scope2}
  13.143 +  \end{center}
  13.144 +  \caption{The result of semantic selection and systematic renaming}
  13.145 +  \label{fig:scope2}
  13.146 +  \end{figure}
  13.147 +\<close>
  13.148 +
  13.149 +
  13.150  section \<open>Completion \label{sec:completion}\<close>
  13.151  
  13.152  text \<open>
  13.153 @@ -1199,12 +1278,12 @@
  13.154    kinds and purposes. The completion mechanism supports this by the following
  13.155    built-in templates:
  13.156  
  13.157 -    \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) supports \<^emph>\<open>quotations\<close> via text
  13.158 -    cartouches. There are three selections, which are always presented in the
  13.159 -    same order and do not depend on any context information. The default
  13.160 -    choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the box indicates the cursor
  13.161 -    position after insertion; the other choices help to repair the block
  13.162 -    structure of unbalanced text cartouches.
  13.163 +    \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) or \<^verbatim>\<open>"\<close> (double ASCII quote) support
  13.164 +    \<^emph>\<open>quotations\<close> via text cartouches. There are three selections, which are
  13.165 +    always presented in the same order and do not depend on any context
  13.166 +    information. The default choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the
  13.167 +    box indicates the cursor position after insertion; the other choices help
  13.168 +    to repair the block structure of unbalanced text cartouches.
  13.169  
  13.170      \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'', where the box indicates
  13.171      the cursor position after insertion. Here it is convenient to use the
  13.172 @@ -1213,8 +1292,8 @@
  13.173  
  13.174    With some practice, input of quoted sub-languages and antiquotations of
  13.175    embedded languages should work fluently. Note that national keyboard layouts
  13.176 -  might cause problems with back-quote as dead key: if possible, dead keys
  13.177 -  should be disabled.
  13.178 +  might cause problems with back-quote as dead key, but double quote can be
  13.179 +  used instead.
  13.180  \<close>
  13.181  
  13.182  
  13.183 @@ -1274,6 +1353,20 @@
  13.184  \<close>
  13.185  
  13.186  
  13.187 +subsubsection \<open>User-defined abbreviations\<close>
  13.188 +
  13.189 +text \<open>
  13.190 +  The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword
  13.191 +  @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in
  13.192 +  templates and abbreviations for Isabelle symbols, as explained above.
  13.193 +  Examples may be found in the Isabelle sources, by searching for
  13.194 +  ``\<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.
  13.195 +
  13.196 +  The \<^emph>\<open>Symbols\<close> panel shows the abbreviations that are available in the
  13.197 +  current theory buffer (according to its \<^theory_text>\<open>imports\<close>) in the \<^verbatim>\<open>Abbrevs\<close> tab.
  13.198 +\<close>
  13.199 +
  13.200 +
  13.201  subsubsection \<open>Name-space entries\<close>
  13.202  
  13.203  text \<open>
  13.204 @@ -2020,6 +2113,27 @@
  13.205  
  13.206    \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window manager (notably
  13.207    on Mac OS X).
  13.208 +
  13.209 +  \<^item> \<^bold>\<open>Problem:\<close> Heap space of the JVM may fill up and render the Prover IDE
  13.210 +  unresponsive, e.g.\ when editing big Isabelle sessions with many theories.
  13.211 +
  13.212 +  \<^bold>\<open>Workaround:\<close> On a 64bit platform, ensure that the JVM runs in 64bit mode,
  13.213 +  but the Isabelle/ML process remains in 32bit mode! Do not switch Isabelle/ML
  13.214 +  into 64bit mode in the expectation to be ``more efficient'' --- this
  13.215 +  requires approx.\ 32\,GB to make sense.
  13.216 +
  13.217 +  For the JVM, always use the 64bit version. That is the default on all
  13.218 +  platforms, except for Windows: the standard download is for win32, but there
  13.219 +  is a separate download for win64. This implicitly provides a larger default
  13.220 +  heap for the JVM.
  13.221 +
  13.222 +  Moreover, it is possible to increase JVM heap parameters explicitly, by
  13.223 +  editing platform-specific files (for ``properties'' or ``options'') that are
  13.224 +  associated with the main app bundle.
  13.225 +
  13.226 +  Also note that jEdit provides a heap space monitor in the status line
  13.227 +  (bottom-right). Double-clicking on that causes full garbage-collection,
  13.228 +  which sometimes helps in low-memory situations.
  13.229  \<close>
  13.230  
  13.231  end
  13.232 \ No newline at end of file
    14.1 Binary file src/Doc/JEdit/document/scope1.png has changed
    15.1 Binary file src/Doc/JEdit/document/scope2.png has changed
    16.1 --- a/src/Doc/ROOT	Thu Nov 24 15:04:05 2016 +0100
    16.2 +++ b/src/Doc/ROOT	Sun Nov 27 20:25:38 2016 +0100
    16.3 @@ -234,6 +234,8 @@
    16.4      "popup2.png"
    16.5      "query.png"
    16.6      "root.tex"
    16.7 +    "scope1.png"
    16.8 +    "scope2.png"
    16.9      "sidekick-document.png"
   16.10      "sidekick.png"
   16.11      "sledgehammer.png"
    17.1 --- a/src/Doc/System/Environment.thy	Thu Nov 24 15:04:05 2016 +0100
    17.2 +++ b/src/Doc/System/Environment.thy	Sun Nov 27 20:25:38 2016 +0100
    17.3 @@ -214,8 +214,8 @@
    17.4  
    17.5      \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
    17.6      bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
    17.7 -    usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
    17.8 -    component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
    17.9 +    usual, the content is interpreted as a GNU bash script. It may refer to
   17.10 +    the component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
   17.11  
   17.12      For example, the following setting allows to refer to files within the
   17.13      component later on, without having to hardwire absolute paths:
   17.14 @@ -260,9 +260,12 @@
   17.15  
   17.16  text \<open>
   17.17    The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
   17.18 -  Isabelle related utilities, user interfaces etc. Such tools automatically
   17.19 -  benefit from the settings mechanism. All Isabelle command-line tools are
   17.20 -  invoked via a common wrapper --- @{executable_ref isabelle}:
   17.21 +  Isabelle-related utilities, user interfaces, add-on applications etc. Such
   17.22 +  tools automatically benefit from the settings mechanism
   17.23 +  (\secref{sec:settings}). Moreover, this is the standard way to invoke
   17.24 +  Isabelle/Scala functionality as a separate operating-system process.
   17.25 +  Isabelle command-line tools are run uniformly via a common wrapper ---
   17.26 +  @{executable_ref isabelle}:
   17.27    @{verbatim [display]
   17.28  \<open>Usage: isabelle TOOL [ARGS ...]
   17.29  
   17.30 @@ -271,12 +274,32 @@
   17.31  Available tools:
   17.32    ...\<close>}
   17.33  
   17.34 -  In principle, Isabelle tools are ordinary executable scripts that are run
   17.35 -  within the Isabelle settings environment, see \secref{sec:settings}. The set
   17.36 -  of available tools is collected by @{executable isabelle} from the
   17.37 -  directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
   17.38 -  call the scripts directly from the shell. Neither should you add the tool
   17.39 -  directories to your shell's search path!
   17.40 +  Tools may be implemented in Isabelle/Scala or as stand-alone executables
   17.41 +  (usually as GNU bash scripts). In the invocation of ``@{executable
   17.42 +  isabelle}~\<open>tool\<close>'', the named \<open>tool\<close> is resolved as follows (and in the
   17.43 +  given order).
   17.44 +
   17.45 +    \<^enum> An external tool found on the directories listed in the @{setting
   17.46 +    ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX
   17.47 +    notation).
   17.48 +
   17.49 +      \<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define
   17.50 +      some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala
   17.51 +      compiler is invoked on the spot (which may take some time), and the body
   17.52 +      function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>.
   17.53 +
   17.54 +      \<^enum> If an executable file ``\<open>tool\<close>'' is found, it is invoked as
   17.55 +      stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close>
   17.56 +      array.
   17.57 +
   17.58 +    \<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close>
   17.59 +    within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred
   17.60 +    entry-point for high-end tools implemented in Isabelle/Scala --- compiled
   17.61 +    once when the Isabelle distribution is built. These tools are provided by
   17.62 +    Isabelle/Pure and cannot be augmented in user-space.
   17.63 +
   17.64 +  There are also some administrative tools that are available from a bare
   17.65 +  repository clone of Isabelle, but not in regular distributions.
   17.66  \<close>
   17.67  
   17.68  
   17.69 @@ -346,7 +369,7 @@
   17.70    loader within ML:
   17.71    @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
   17.72  
   17.73 -  Observe the delicate quoting rules for the Bash shell vs.\ ML. The
   17.74 +  Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
   17.75    Isabelle/ML and Scala libraries provide functions for that, but here we need
   17.76    to do it manually.
   17.77  \<close>
    18.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Nov 24 15:04:05 2016 +0100
    18.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sun Nov 27 20:25:38 2016 +0100
    18.3 @@ -3265,8 +3265,8 @@
    18.4  
    18.5  lemma homotopic_circlemaps_imp_homotopic_loops:
    18.6    assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
    18.7 -   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))
    18.8 -                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * ii))"
    18.9 +   shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))
   18.10 +                            (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
   18.11  proof -
   18.12    have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
   18.13      using assms by (auto simp: sphere_def)
   18.14 @@ -3347,7 +3347,7 @@
   18.15        and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
   18.16      shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
   18.17  proof -
   18.18 -  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))"
   18.19 +  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>))"
   18.20      apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
   18.21      apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
   18.22      done
    19.1 --- a/src/HOL/Analysis/Further_Topology.thy	Thu Nov 24 15:04:05 2016 +0100
    19.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Sun Nov 27 20:25:38 2016 +0100
    19.3 @@ -3240,7 +3240,7 @@
    19.4      have inj_exp: "inj_on exp (ball (Ln z) 1)"
    19.5        apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
    19.6        using pi_ge_two by (simp add: ball_subset_ball_iff)
    19.7 -    define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1))"
    19.8 +    define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * \<i>) ` (ball(Ln z) 1))"
    19.9      show ?thesis
   19.10      proof (intro exI conjI)
   19.11        show "z \<in> exp ` (ball(Ln z) 1)"
   19.12 @@ -3286,7 +3286,7 @@
   19.13        proof
   19.14          fix u
   19.15          assume "u \<in> \<V>"
   19.16 -        then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1)"
   19.17 +        then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * \<i>) ` (ball(Ln z) 1)"
   19.18            by (auto simp: \<V>_def)
   19.19          have "compact (cball (Ln z) 1)"
   19.20            by simp
   19.21 @@ -3325,7 +3325,7 @@
   19.22            apply (force simp:)
   19.23            done
   19.24          show "\<exists>q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
   19.25 -          apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * ii) \<circ> \<gamma>" in exI)
   19.26 +          apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * \<i>) \<circ> \<gamma>" in exI)
   19.27            unfolding homeomorphism_def
   19.28            apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id])
   19.29               apply (auto simp: \<gamma>exp exp2n cont n)
    20.1 --- a/src/HOL/Decision_Procs/approximation_generator.ML	Thu Nov 24 15:04:05 2016 +0100
    20.2 +++ b/src/HOL/Decision_Procs/approximation_generator.ML	Sun Nov 27 20:25:38 2016 +0100
    20.3 @@ -52,6 +52,8 @@
    20.4    | mapprox_floatarith @{term Pi} _ = Math.pi
    20.5    | mapprox_floatarith (@{term Sqrt} $ a) xs = Math.sqrt (mapprox_floatarith a xs)
    20.6    | mapprox_floatarith (@{term Exp} $ a) xs = Math.exp (mapprox_floatarith a xs)
    20.7 +  | mapprox_floatarith (@{term Powr} $ a $ b) xs =
    20.8 +      Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)
    20.9    | mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs)
   20.10    | mapprox_floatarith (@{term Power} $ a $ n) xs =
   20.11        Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
    21.1 --- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Thu Nov 24 15:04:05 2016 +0100
    21.2 +++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sun Nov 27 20:25:38 2016 +0100
    21.3 @@ -300,7 +300,7 @@
    21.4  
    21.5  theorem (in classical) Peirce's_Law: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
    21.6  proof
    21.7 -  assume a: "(A \<longrightarrow> B) \<longrightarrow> A"
    21.8 +  assume *: "(A \<longrightarrow> B) \<longrightarrow> A"
    21.9    show A
   21.10    proof (rule classical)
   21.11      assume "\<not> A"
   21.12 @@ -309,7 +309,7 @@
   21.13        assume A
   21.14        with \<open>\<not> A\<close> show B by (rule contradiction)
   21.15      qed
   21.16 -    with a show A ..
   21.17 +    with * show A ..
   21.18    qed
   21.19  qed
   21.20  
    22.1 --- a/src/HOL/Nunchaku/Nunchaku.thy	Thu Nov 24 15:04:05 2016 +0100
    22.2 +++ b/src/HOL/Nunchaku/Nunchaku.thy	Sun Nov 27 20:25:38 2016 +0100
    22.3 @@ -9,9 +9,9 @@
    22.4  
    22.5      https://github.com/nunchaku-inria
    22.6  
    22.7 -The "$NUNCHAKU" environment variable must be set to the absolute file name of
    22.8 -the "nunchaku" executable. The Isabelle components for CVC4 and Kodkodi are
    22.9 -necessary to use these backends.
   22.10 +The "$NUNCHAKU_HOME" environment variable must be set to the absolute path to
   22.11 +the directory containing the "nunchaku" executable. The Isabelle components
   22.12 +for CVC4 and Kodkodi are necessary to use these backends.
   22.13  *)
   22.14  
   22.15  theory Nunchaku
    23.1 --- a/src/HOL/Nunchaku/Tools/nunchaku.ML	Thu Nov 24 15:04:05 2016 +0100
    23.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku.ML	Sun Nov 27 20:25:38 2016 +0100
    23.3 @@ -256,7 +256,7 @@
    23.4              | Unknown (SOME (output, _)) => sat_or_maybe_sat false output
    23.5              | Timeout => (print_n "Time out"; (unknownN, NONE))
    23.6              | Nunchaku_Var_Not_Set =>
    23.7 -              (print_n ("Variable $" ^ nunchaku_env_var ^ " not set"); (unknownN, NONE))
    23.8 +              (print_n ("Variable $" ^ nunchaku_home_env_var ^ " not set"); (unknownN, NONE))
    23.9              | Nunchaku_Cannot_Execute =>
   23.10                (print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
   23.11              | Nunchaku_Not_Found =>
    24.1 --- a/src/HOL/Nunchaku/Tools/nunchaku_tool.ML	Thu Nov 24 15:04:05 2016 +0100
    24.2 +++ b/src/HOL/Nunchaku/Tools/nunchaku_tool.ML	Sun Nov 27 20:25:38 2016 +0100
    24.3 @@ -33,7 +33,7 @@
    24.4    | CVC4_Not_Found
    24.5    | Unknown_Error of int * string
    24.6  
    24.7 -  val nunchaku_env_var: string
    24.8 +  val nunchaku_home_env_var: string
    24.9  
   24.10    val solve_nun_problem: tool_params -> nun_problem -> nun_outcome
   24.11  end;
   24.12 @@ -71,7 +71,7 @@
   24.13      ((out, err), rc)
   24.14    end;
   24.15  
   24.16 -val nunchaku_env_var = "NUNCHAKU";
   24.17 +val nunchaku_home_env_var = "NUNCHAKU_HOME";
   24.18  
   24.19  val cached_outcome =
   24.20    Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : (nun_problem * nun_outcome) option);
   24.21 @@ -79,13 +79,13 @@
   24.22  fun uncached_solve_nun_problem ({overlord, specialize, timeout, ...} : tool_params)
   24.23      (problem as {sound, complete, ...}) =
   24.24    with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
   24.25 -    if getenv nunchaku_env_var = "" then
   24.26 +    if getenv nunchaku_home_env_var = "" then
   24.27        Nunchaku_Var_Not_Set
   24.28      else
   24.29        let
   24.30          val bash_cmd =
   24.31 -          "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^ nunchaku_env_var ^ "\" \
   24.32 -          \--skolems-in-model --no-color " ^
   24.33 +          "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
   24.34 +          nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
   24.35            (if specialize then "" else "--no-specialize ") ^
   24.36            "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
   24.37            File.bash_path prob_path;
   24.38 @@ -99,10 +99,12 @@
   24.39            (if sound then Sat else Unknown o SOME) (output, {tys = [], tms = []})
   24.40          else if String.isPrefix "UNSAT" output then
   24.41            if complete then Unsat else Unknown NONE
   24.42 +        else if String.isSubstring "TIMEOUT" output
   24.43 +            (* FIXME: temporary *)
   24.44 +            orelse String.isSubstring "kodkod failed (errcode 152)" error then
   24.45 +          Timeout
   24.46          else if String.isPrefix "UNKNOWN" output then
   24.47            Unknown NONE
   24.48 -        else if String.isPrefix "TIMEOUT" output then
   24.49 -          Timeout
   24.50          else if code = 126 then
   24.51            Nunchaku_Cannot_Execute
   24.52          else if code = 127 then
    25.1 --- a/src/HOL/Probability/Fin_Map.thy	Thu Nov 24 15:04:05 2016 +0100
    25.2 +++ b/src/HOL/Probability/Fin_Map.thy	Sun Nov 27 20:25:38 2016 +0100
    25.3 @@ -5,7 +5,7 @@
    25.4  section \<open>Finite Maps\<close>
    25.5  
    25.6  theory Fin_Map
    25.7 -  imports Finite_Product_Measure "~~/src/HOL/Library/Finite_Map"
    25.8 +  imports "~~/src/HOL/Analysis/Finite_Product_Measure" "~~/src/HOL/Library/Finite_Map"
    25.9  begin
   25.10  
   25.11  text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of
    26.1 --- a/src/HOL/Proofs/ex/Hilbert_Classical.thy	Thu Nov 24 15:04:05 2016 +0100
    26.2 +++ b/src/HOL/Proofs/ex/Hilbert_Classical.thy	Sun Nov 27 20:25:38 2016 +0100
    26.3 @@ -1,11 +1,12 @@
    26.4  (*  Title:      HOL/Proofs/ex/Hilbert_Classical.thy
    26.5 -    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    26.6 +    Author:     Stefan Berghofer
    26.7 +    Author:     Makarius Wenzel
    26.8  *)
    26.9  
   26.10  section \<open>Hilbert's choice and classical logic\<close>
   26.11  
   26.12  theory Hilbert_Classical
   26.13 -imports Main
   26.14 +  imports Main
   26.15  begin
   26.16  
   26.17  text \<open>
   26.18 @@ -16,145 +17,220 @@
   26.19  
   26.20  subsection \<open>Proof text\<close>
   26.21  
   26.22 -theorem tnd: "A \<or> \<not> A"
   26.23 +theorem tertium_non_datur: "A \<or> \<not> A"
   26.24  proof -
   26.25 -  let ?P = "\<lambda>X. X = False \<or> X = True \<and> A"
   26.26 -  let ?Q = "\<lambda>X. X = False \<and> A \<or> X = True"
   26.27 +  let ?P = "\<lambda>x. (A \<and> x) \<or> \<not> x"
   26.28 +  let ?Q = "\<lambda>x. (A \<and> \<not> x) \<or> x"
   26.29  
   26.30    have a: "?P (Eps ?P)"
   26.31    proof (rule someI)
   26.32 -    have "False = False" ..
   26.33 -    thus "?P False" ..
   26.34 +    have "\<not> False" ..
   26.35 +    then show "?P False" ..
   26.36    qed
   26.37    have b: "?Q (Eps ?Q)"
   26.38    proof (rule someI)
   26.39 -    have "True = True" ..
   26.40 -    thus "?Q True" ..
   26.41 +    have True ..
   26.42 +    then show "?Q True" ..
   26.43    qed
   26.44  
   26.45    from a show ?thesis
   26.46    proof
   26.47 -    assume "Eps ?P = True \<and> A"
   26.48 -    hence A ..
   26.49 -    thus ?thesis ..
   26.50 +    assume "A \<and> Eps ?P"
   26.51 +    then have A ..
   26.52 +    then show ?thesis ..
   26.53    next
   26.54 -    assume P: "Eps ?P = False"
   26.55 +    assume "\<not> Eps ?P"
   26.56      from b show ?thesis
   26.57      proof
   26.58 -      assume "Eps ?Q = False \<and> A"
   26.59 -      hence A ..
   26.60 -      thus ?thesis ..
   26.61 +      assume "A \<and> \<not> Eps ?Q"
   26.62 +      then have A ..
   26.63 +      then show ?thesis ..
   26.64      next
   26.65 -      assume Q: "Eps ?Q = True"
   26.66 +      assume "Eps ?Q"
   26.67        have neq: "?P \<noteq> ?Q"
   26.68        proof
   26.69          assume "?P = ?Q"
   26.70 -        hence "Eps ?P = Eps ?Q" by (rule arg_cong)
   26.71 +        then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
   26.72 +        also note \<open>Eps ?Q\<close>
   26.73 +        finally have "Eps ?P" .
   26.74 +        with \<open>\<not> Eps ?P\<close> show False by contradiction
   26.75 +      qed
   26.76 +      have "\<not> A"
   26.77 +      proof
   26.78 +        assume A
   26.79 +        have "?P = ?Q"
   26.80 +        proof (rule ext)
   26.81 +          show "?P x \<longleftrightarrow> ?Q x" for x
   26.82 +          proof
   26.83 +            assume "?P x"
   26.84 +            then show "?Q x"
   26.85 +            proof
   26.86 +              assume "\<not> x"
   26.87 +              with \<open>A\<close> have "A \<and> \<not> x" ..
   26.88 +              then show ?thesis ..
   26.89 +            next
   26.90 +              assume "A \<and> x"
   26.91 +              then have x ..
   26.92 +              then show ?thesis ..
   26.93 +            qed
   26.94 +          next
   26.95 +            assume "?Q x"
   26.96 +            then show "?P x"
   26.97 +            proof
   26.98 +              assume "A \<and> \<not> x"
   26.99 +              then have "\<not> x" ..
  26.100 +              then show ?thesis ..
  26.101 +            next
  26.102 +              assume x
  26.103 +              with \<open>A\<close> have "A \<and> x" ..
  26.104 +              then show ?thesis ..
  26.105 +            qed
  26.106 +          qed
  26.107 +        qed
  26.108 +        with neq show False by contradiction
  26.109 +      qed
  26.110 +      then show ?thesis ..
  26.111 +    qed
  26.112 +  qed
  26.113 +qed
  26.114 +
  26.115 +
  26.116 +subsection \<open>Old proof text\<close>
  26.117 +
  26.118 +theorem tertium_non_datur1: "A \<or> \<not> A"
  26.119 +proof -
  26.120 +  let ?P = "\<lambda>x. (x \<longleftrightarrow> False) \<or> (x \<longleftrightarrow> True) \<and> A"
  26.121 +  let ?Q = "\<lambda>x. (x \<longleftrightarrow> False) \<and> A \<or> (x \<longleftrightarrow> True)"
  26.122 +
  26.123 +  have a: "?P (Eps ?P)"
  26.124 +  proof (rule someI)
  26.125 +    show "?P False" using refl ..
  26.126 +  qed
  26.127 +  have b: "?Q (Eps ?Q)"
  26.128 +  proof (rule someI)
  26.129 +    show "?Q True" using refl ..
  26.130 +  qed
  26.131 +
  26.132 +  from a show ?thesis
  26.133 +  proof
  26.134 +    assume "(Eps ?P \<longleftrightarrow> True) \<and> A"
  26.135 +    then have A ..
  26.136 +    then show ?thesis ..
  26.137 +  next
  26.138 +    assume P: "Eps ?P \<longleftrightarrow> False"
  26.139 +    from b show ?thesis
  26.140 +    proof
  26.141 +      assume "(Eps ?Q \<longleftrightarrow> False) \<and> A"
  26.142 +      then have A ..
  26.143 +      then show ?thesis ..
  26.144 +    next
  26.145 +      assume Q: "Eps ?Q \<longleftrightarrow> True"
  26.146 +      have neq: "?P \<noteq> ?Q"
  26.147 +      proof
  26.148 +        assume "?P = ?Q"
  26.149 +        then have "Eps ?P \<longleftrightarrow> Eps ?Q" by (rule arg_cong)
  26.150          also note P
  26.151          also note Q
  26.152          finally show False by (rule False_neq_True)
  26.153        qed
  26.154        have "\<not> A"
  26.155        proof
  26.156 -        assume a: A
  26.157 +        assume A
  26.158          have "?P = ?Q"
  26.159          proof (rule ext)
  26.160 -          fix x show "?P x = ?Q x"
  26.161 +          show "?P x \<longleftrightarrow> ?Q x" for x
  26.162            proof
  26.163              assume "?P x"
  26.164 -            thus "?Q x"
  26.165 +            then show "?Q x"
  26.166              proof
  26.167 -              assume "x = False"
  26.168 -              from this and a have "x = False \<and> A" ..
  26.169 -              thus "?Q x" ..
  26.170 +              assume "x \<longleftrightarrow> False"
  26.171 +              from this and \<open>A\<close> have "(x \<longleftrightarrow> False) \<and> A" ..
  26.172 +              then show ?thesis ..
  26.173              next
  26.174 -              assume "x = True \<and> A"
  26.175 -              hence "x = True" ..
  26.176 -              thus "?Q x" ..
  26.177 +              assume "(x \<longleftrightarrow> True) \<and> A"
  26.178 +              then have "x \<longleftrightarrow> True" ..
  26.179 +              then show ?thesis ..
  26.180              qed
  26.181            next
  26.182              assume "?Q x"
  26.183 -            thus "?P x"
  26.184 +            then show "?P x"
  26.185              proof
  26.186 -              assume "x = False \<and> A"
  26.187 -              hence "x = False" ..
  26.188 -              thus "?P x" ..
  26.189 +              assume "(x \<longleftrightarrow> False) \<and> A"
  26.190 +              then have "x \<longleftrightarrow> False" ..
  26.191 +              then show ?thesis ..
  26.192              next
  26.193 -              assume "x = True"
  26.194 -              from this and a have "x = True \<and> A" ..
  26.195 -              thus "?P x" ..
  26.196 +              assume "x \<longleftrightarrow> True"
  26.197 +              from this and \<open>A\<close> have "(x \<longleftrightarrow> True) \<and> A" ..
  26.198 +              then show ?thesis ..
  26.199              qed
  26.200            qed
  26.201          qed
  26.202          with neq show False by contradiction
  26.203        qed
  26.204 -      thus ?thesis ..
  26.205 +      then show ?thesis ..
  26.206      qed
  26.207    qed
  26.208  qed
  26.209  
  26.210  
  26.211 -subsection \<open>Proof term of text\<close>
  26.212 -
  26.213 -prf tnd
  26.214 -
  26.215 +subsection \<open>Old proof script\<close>
  26.216  
  26.217 -subsection \<open>Proof script\<close>
  26.218 -
  26.219 -theorem tnd': "A \<or> \<not> A"
  26.220 +theorem tertium_non_datur2: "A \<or> \<not> A"
  26.221    apply (subgoal_tac
  26.222 -    "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
  26.223 +      "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
  26.224        ((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and>
  26.225 -     (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
  26.226 +      (((SOME x. x = False \<and> A \<or> x = True) = False) \<and> A \<or>
  26.227        ((SOME x. x = False \<and> A \<or> x = True) = True))")
  26.228 -  prefer 2
  26.229 -  apply (rule conjI)
  26.230 -  apply (rule someI)
  26.231 -  apply (rule disjI1)
  26.232 -  apply (rule refl)
  26.233 -  apply (rule someI)
  26.234 -  apply (rule disjI2)
  26.235 -  apply (rule refl)
  26.236 +   prefer 2
  26.237 +   apply (rule conjI)
  26.238 +    apply (rule someI)
  26.239 +    apply (rule disjI1)
  26.240 +    apply (rule refl)
  26.241 +   apply (rule someI)
  26.242 +   apply (rule disjI2)
  26.243 +   apply (rule refl)
  26.244    apply (erule conjE)
  26.245    apply (erule disjE)
  26.246 -  apply (erule disjE)
  26.247 -  apply (erule conjE)
  26.248 -  apply (erule disjI1)
  26.249 -  prefer 2
  26.250 -  apply (erule conjE)
  26.251 -  apply (erule disjI1)
  26.252 +   apply (erule disjE)
  26.253 +    apply (erule conjE)
  26.254 +    apply (erule disjI1)
  26.255 +   prefer 2
  26.256 +   apply (erule conjE)
  26.257 +   apply (erule disjI1)
  26.258    apply (subgoal_tac
  26.259 -    "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
  26.260 -     (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
  26.261 -  prefer 2
  26.262 -  apply (rule notI)
  26.263 -  apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
  26.264 -  apply (drule trans, assumption)
  26.265 -  apply (drule sym)
  26.266 -  apply (drule trans, assumption)
  26.267 -  apply (erule False_neq_True)
  26.268 +      "(\<lambda>x. (x = False) \<or> (x = True) \<and> A) \<noteq>
  26.269 +      (\<lambda>x. (x = False) \<and> A \<or> (x = True))")
  26.270 +   prefer 2
  26.271 +   apply (rule notI)
  26.272 +   apply (drule_tac f = "\<lambda>y. SOME x. y x" in arg_cong)
  26.273 +   apply (drule trans, assumption)
  26.274 +   apply (drule sym)
  26.275 +   apply (drule trans, assumption)
  26.276 +   apply (erule False_neq_True)
  26.277    apply (rule disjI2)
  26.278    apply (rule notI)
  26.279    apply (erule notE)
  26.280    apply (rule ext)
  26.281    apply (rule iffI)
  26.282 +   apply (erule disjE)
  26.283 +    apply (rule disjI1)
  26.284 +    apply (erule conjI)
  26.285 +    apply assumption
  26.286 +   apply (erule conjE)
  26.287 +   apply (erule disjI2)
  26.288    apply (erule disjE)
  26.289 -  apply (rule disjI1)
  26.290 -  apply (erule conjI)
  26.291 -  apply assumption
  26.292 -  apply (erule conjE)
  26.293 -  apply (erule disjI2)
  26.294 -  apply (erule disjE)
  26.295 -  apply (erule conjE)
  26.296 -  apply (erule disjI1)
  26.297 +   apply (erule conjE)
  26.298 +   apply (erule disjI1)
  26.299    apply (rule disjI2)
  26.300    apply (erule conjI)
  26.301    apply assumption
  26.302    done
  26.303  
  26.304  
  26.305 -subsection \<open>Proof term of script\<close>
  26.306 +subsection \<open>Proof terms\<close>
  26.307  
  26.308 -prf tnd'
  26.309 +prf tertium_non_datur
  26.310 +prf tertium_non_datur1
  26.311 +prf tertium_non_datur2
  26.312  
  26.313  end
    27.1 --- a/src/HOL/TPTP/mash_export.ML	Thu Nov 24 15:04:05 2016 +0100
    27.2 +++ b/src/HOL/TPTP/mash_export.ML	Sun Nov 27 20:25:38 2016 +0100
    27.3 @@ -286,16 +286,16 @@
    27.4         not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
    27.5         #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
    27.6  
    27.7 -fun generate_mash_suggestions algorithm =
    27.8 +fun generate_mash_suggestions algorithm ctxt =
    27.9    (Options.put_default @{system_option MaSh} algorithm;
   27.10 -   Sledgehammer_MaSh.mash_unlearn ();
   27.11 +   Sledgehammer_MaSh.mash_unlearn ctxt;
   27.12     generate_mepo_or_mash_suggestions
   27.13       (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} =>
   27.14            fn max_suggs => fn hyp_ts => fn concl_t =>
   27.15          tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false
   27.16            Sledgehammer_Util.one_year)
   27.17          #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t
   27.18 -        #> fst))
   27.19 +        #> fst) ctxt)
   27.20  
   27.21  fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
   27.22    let
    28.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Nov 24 15:04:05 2016 +0100
    28.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Sun Nov 27 20:25:38 2016 +0100
    28.3 @@ -68,6 +68,7 @@
    28.4  
    28.5  local
    28.6    fun cvc4_options ctxt = [
    28.7 +    "--no-statistics",
    28.8      "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    28.9      "--lang=smt2",
   28.10      "--continued-execution",
    29.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Nov 24 15:04:05 2016 +0100
    29.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sun Nov 27 20:25:38 2016 +0100
    29.3 @@ -324,10 +324,10 @@
    29.4      else if subcommand = supported_proversN then
    29.5        supported_provers ctxt
    29.6      else if subcommand = unlearnN then
    29.7 -      mash_unlearn ()
    29.8 +      mash_unlearn ctxt
    29.9      else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse
   29.10              subcommand = relearn_isarN orelse subcommand = relearn_proverN then
   29.11 -      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ()
   29.12 +      (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt
   29.13         else ();
   29.14         mash_learn ctxt
   29.15             (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
    30.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 24 15:04:05 2016 +0100
    30.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Nov 27 20:25:38 2016 +0100
    30.3 @@ -69,13 +69,13 @@
    30.4    val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term ->
    30.5      raw_fact list -> fact list * fact list
    30.6  
    30.7 -  val mash_unlearn : unit -> unit
    30.8 +  val mash_unlearn : Proof.context -> unit
    30.9    val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
   30.10    val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time ->
   30.11      raw_fact list -> string
   30.12    val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
   30.13    val mash_can_suggest_facts : Proof.context -> bool
   30.14 -  val mash_can_suggest_facts_fast : unit -> bool
   30.15 +  val mash_can_suggest_facts_fast : Proof.context -> bool
   30.16  
   30.17    val generous_max_suggestions : int -> int
   30.18    val mepo_weight : real
   30.19 @@ -274,6 +274,18 @@
   30.20    end
   30.21  
   30.22  
   30.23 +(*** Convenience functions for synchronized access ***)
   30.24 +
   30.25 +fun synchronized_timed_value var time_limit =
   30.26 +  Synchronized.timed_access var time_limit (fn value => SOME (value, value))
   30.27 +fun synchronized_timed_change_result var time_limit f =
   30.28 +  Synchronized.timed_access var time_limit (SOME o f)
   30.29 +fun synchronized_timed_change var time_limit f =
   30.30 +  synchronized_timed_change_result var time_limit (fn x => ((), f x))
   30.31 +
   30.32 +fun mash_time_limit _ = SOME (seconds 0.1)
   30.33 +
   30.34 +
   30.35  (*** Isabelle-agnostic machine learning ***)
   30.36  
   30.37  structure MaSh =
   30.38 @@ -640,7 +652,7 @@
   30.39  
   30.40  local
   30.41  
   30.42 -val version = "*** MaSh version 20160805 ***"
   30.43 +val version = "*** MaSh version 20161123 ***"
   30.44  
   30.45  exception FILE_VERSION_TOO_NEW of unit
   30.46  
   30.47 @@ -734,42 +746,49 @@
   30.48  in
   30.49  
   30.50  fun map_state ctxt f =
   30.51 -  Synchronized.change global_state (load_state ctxt ##> f #> save_state ctxt)
   30.52 +  (trace_msg ctxt (fn () => "Changing MaSh state");
   30.53 +   synchronized_timed_change global_state mash_time_limit
   30.54 +     (load_state ctxt ##> f #> save_state ctxt))
   30.55 +  |> ignore
   30.56    handle FILE_VERSION_TOO_NEW () => ()
   30.57  
   30.58 -fun peek_state () =
   30.59 -  let val state = Synchronized.value global_state in
   30.60 -    if would_load_state state then NONE else SOME state
   30.61 -  end
   30.62 +fun peek_state ctxt =
   30.63 +  (trace_msg ctxt (fn () => "Peeking at MaSh state");
   30.64 +   (case synchronized_timed_value global_state mash_time_limit of
   30.65 +     NONE => NONE
   30.66 +   | SOME state => if would_load_state state then NONE else SOME state))
   30.67  
   30.68  fun get_state ctxt =
   30.69 -  Synchronized.change_result global_state (perhaps (try (load_state ctxt)) #> `snd)
   30.70 +  (trace_msg ctxt (fn () => "Retrieving MaSh state");
   30.71 +   synchronized_timed_change_result global_state mash_time_limit
   30.72 +     (perhaps (try (load_state ctxt)) #> `snd))
   30.73  
   30.74 -fun clear_state () =
   30.75 -  Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state)))
   30.76 +fun clear_state ctxt =
   30.77 +  (trace_msg ctxt (fn () => "Clearing MaSh state");
   30.78 +   Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state))))
   30.79  
   30.80  end
   30.81  
   30.82  
   30.83  (*** Isabelle helpers ***)
   30.84  
   30.85 -fun crude_printed_term depth t =
   30.86 +fun crude_printed_term size t =
   30.87    let
   30.88      fun term _ (res, 0) = (res, 0)
   30.89 -      | term (t $ u) (res, depth) =
   30.90 +      | term (t $ u) (res, size) =
   30.91          let
   30.92 -          val (res, depth) = term t (res ^ "(", depth)
   30.93 -          val (res, depth) = term u (res ^ " ", depth)
   30.94 +          val (res, size) = term t (res ^ "(", size)
   30.95 +          val (res, size) = term u (res ^ " ", size)
   30.96          in
   30.97 -          (res ^ ")", depth)
   30.98 +          (res ^ ")", size)
   30.99          end
  30.100 -      | term (Abs (s, _, t)) (res, depth) = term t (res ^ "%" ^ s ^ ".", depth - 1)
  30.101 -      | term (Bound n) (res, depth) = (res ^ "#" ^ string_of_int n, depth - 1)
  30.102 -      | term (Const (s, _)) (res, depth) = (res ^ Long_Name.base_name s, depth - 1)
  30.103 -      | term (Free (s, _)) (res, depth) = (res ^ s, depth - 1)
  30.104 -      | term (Var ((s, _), _)) (res, depth) = (res ^ s, depth - 1)
  30.105 +      | term (Abs (s, _, t)) (res, size) = term t (res ^ "%" ^ s ^ ".", size - 1)
  30.106 +      | term (Bound n) (res, size) = (res ^ "#" ^ string_of_int n, size - 1)
  30.107 +      | term (Const (s, _)) (res, size) = (res ^ Long_Name.base_name s, size - 1)
  30.108 +      | term (Free (s, _)) (res, size) = (res ^ s, size - 1)
  30.109 +      | term (Var ((s, _), _)) (res, size) = (res ^ s, size - 1)
  30.110    in
  30.111 -    fst (term t ("", depth))
  30.112 +    fst (term t ("", size))
  30.113    end
  30.114  
  30.115  fun nickname_of_thm th =
  30.116 @@ -778,11 +797,11 @@
  30.117        (* There must be a better way to detect local facts. *)
  30.118        (case Long_Name.dest_local hint of
  30.119          SOME suf =>
  30.120 -        Long_Name.implode [Thm.theory_name_of_thm th, suf, crude_printed_term 50 (Thm.prop_of th)]
  30.121 +        Long_Name.implode [Thm.theory_name_of_thm th, suf, crude_printed_term 25 (Thm.prop_of th)]
  30.122        | NONE => hint)
  30.123      end
  30.124    else
  30.125 -    crude_printed_term 100 (Thm.prop_of th)
  30.126 +    crude_printed_term 50 (Thm.prop_of th)
  30.127  
  30.128  fun find_suggested_facts ctxt facts =
  30.129    let
  30.130 @@ -857,23 +876,17 @@
  30.131  
  30.132  val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
  30.133  
  30.134 -val pat_tvar_prefix = "_"
  30.135 -val pat_var_prefix = "_"
  30.136 +val crude_str_of_sort = space_implode "," o map Long_Name.base_name o subtract (op =) @{sort type}
  30.137  
  30.138 -(* try "Long_Name.base_name" for shorter names *)
  30.139 -fun massage_long_name s = s
  30.140 -
  30.141 -val crude_str_of_sort = space_implode "," o map massage_long_name o subtract (op =) @{sort type}
  30.142 -
  30.143 -fun crude_str_of_typ (Type (s, [])) = massage_long_name s
  30.144 -  | crude_str_of_typ (Type (s, Ts)) = massage_long_name s ^ implode (map crude_str_of_typ Ts)
  30.145 +fun crude_str_of_typ (Type (s, [])) = Long_Name.base_name s
  30.146 +  | crude_str_of_typ (Type (s, Ts)) = Long_Name.base_name s ^ implode (map crude_str_of_typ Ts)
  30.147    | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S
  30.148    | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S
  30.149  
  30.150 -fun maybe_singleton_str _ "" = []
  30.151 -  | maybe_singleton_str pref s = [pref ^ s]
  30.152 +fun maybe_singleton_str "" = []
  30.153 +  | maybe_singleton_str s = [s]
  30.154  
  30.155 -val max_pat_breadth = 10 (* FUDGE *)
  30.156 +val max_pat_breadth = 5 (* FUDGE *)
  30.157  
  30.158  fun term_features_of ctxt thy_name term_max_depth type_max_depth ts =
  30.159    let
  30.160 @@ -886,13 +899,12 @@
  30.161        | add_classes S =
  30.162          fold (`(Sorts.super_classes classes)
  30.163            #> swap #> op ::
  30.164 -          #> subtract (op =) @{sort type} #> map massage_long_name
  30.165 +          #> subtract (op =) @{sort type}
  30.166            #> map class_feature_of
  30.167            #> union (op =)) S
  30.168  
  30.169      fun pattify_type 0 _ = []
  30.170 -      | pattify_type _ (Type (s, [])) =
  30.171 -        if member (op =) bad_types s then [] else [massage_long_name s]
  30.172 +      | pattify_type depth (Type (s, [])) = if member (op =) bad_types s then [] else [s]
  30.173        | pattify_type depth (Type (s, U :: Ts)) =
  30.174          let
  30.175            val T = Type (s, Ts)
  30.176 @@ -901,8 +913,8 @@
  30.177          in
  30.178            map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
  30.179          end
  30.180 -      | pattify_type _ (TFree (_, S)) = maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
  30.181 -      | pattify_type _ (TVar (_, S)) = maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
  30.182 +      | pattify_type _ (TFree (_, S)) = maybe_singleton_str (crude_str_of_sort S)
  30.183 +      | pattify_type _ (TVar (_, S)) = maybe_singleton_str (crude_str_of_sort S)
  30.184  
  30.185      fun add_type_pat depth T =
  30.186        union (op =) (map type_feature_of (pattify_type depth T))
  30.187 @@ -918,17 +930,16 @@
  30.188        | add_subtypes T = add_type T
  30.189  
  30.190      fun pattify_term _ 0 _ = []
  30.191 -      | pattify_term _ _ (Const (s, _)) =
  30.192 -        if is_widely_irrelevant_const s then [] else [massage_long_name s]
  30.193 +      | pattify_term _ depth (Const (s, _)) =
  30.194 +        if is_widely_irrelevant_const s then [] else [s]
  30.195        | pattify_term _ _ (Free (s, T)) =
  30.196 -        maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
  30.197 -        |> (if member (op =) fixes s then
  30.198 -              cons (free_feature_of (massage_long_name (Long_Name.append thy_name s)))
  30.199 -            else
  30.200 -              I)
  30.201 -      | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
  30.202 +        maybe_singleton_str (crude_str_of_typ T)
  30.203 +        |> (if member (op =) fixes s then cons (free_feature_of (Long_Name.append thy_name s))
  30.204 +            else I)
  30.205 +      | pattify_term _ _ (Var (_, T)) =
  30.206 +        maybe_singleton_str (crude_str_of_typ T)
  30.207        | pattify_term Ts _ (Bound j) =
  30.208 -        maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
  30.209 +        maybe_singleton_str (crude_str_of_typ (nth Ts j))
  30.210        | pattify_term Ts depth (t $ u) =
  30.211          let
  30.212            val ps = take max_pat_breadth (pattify_term Ts depth t)
  30.213 @@ -972,9 +983,9 @@
  30.214  
  30.215  (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn
  30.216     from such proofs. *)
  30.217 -val max_dependencies = 20
  30.218 +val max_dependencies = 20 (* FUDGE *)
  30.219  
  30.220 -val prover_default_max_facts = 25
  30.221 +val prover_default_max_facts = 25 (* FUDGE *)
  30.222  
  30.223  (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
  30.224  val typedef_dep = nickname_of_thm @{thm CollectI}
  30.225 @@ -1161,7 +1172,7 @@
  30.226  fun maximal_wrt_access_graph _ [] = []
  30.227    | maximal_wrt_access_graph access_G (fact :: facts) =
  30.228      let
  30.229 -      fun cleanup_wrt (fact as (_, th)) =
  30.230 +      fun cleanup_wrt (_, th) =
  30.231          let val thy_id = Thm.theory_id_of_thm th in
  30.232            filter_out (fn (_, th') =>
  30.233              Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id))
  30.234 @@ -1224,54 +1235,57 @@
  30.235        [Thm.prop_of th]
  30.236        |> features_of ctxt (Thm.theory_name_of_thm th) stature
  30.237        |> map (rpair (weight * factor))
  30.238 -
  30.239 -    val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =
  30.240 -      get_state ctxt
  30.241 +  in
  30.242 +    (case get_state ctxt of
  30.243 +      NONE => ([], [])
  30.244 +    | SOME {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =>
  30.245 +      let
  30.246 +        val goal_feats0 =
  30.247 +          features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts)
  30.248 +        val chained_feats = chained
  30.249 +          |> map (rpair 1.0)
  30.250 +          |> map (chained_or_extra_features_of chained_feature_factor)
  30.251 +          |> rpair [] |-> fold (union (eq_fst (op =)))
  30.252 +        val extra_feats = facts
  30.253 +          |> take (Int.max (0, num_extra_feature_facts - length chained))
  30.254 +          |> filter fact_has_right_theory
  30.255 +          |> weight_facts_steeply
  30.256 +          |> map (chained_or_extra_features_of extra_feature_factor)
  30.257 +          |> rpair [] |-> fold (union (eq_fst (op =)))
  30.258  
  30.259 -    val goal_feats0 =
  30.260 -      features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts)
  30.261 -    val chained_feats = chained
  30.262 -      |> map (rpair 1.0)
  30.263 -      |> map (chained_or_extra_features_of chained_feature_factor)
  30.264 -      |> rpair [] |-> fold (union (eq_fst (op =)))
  30.265 -    val extra_feats = facts
  30.266 -      |> take (Int.max (0, num_extra_feature_facts - length chained))
  30.267 -      |> filter fact_has_right_theory
  30.268 -      |> weight_facts_steeply
  30.269 -      |> map (chained_or_extra_features_of extra_feature_factor)
  30.270 -      |> rpair [] |-> fold (union (eq_fst (op =)))
  30.271 -
  30.272 -    val goal_feats =
  30.273 -      fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
  30.274 -      |> debug ? sort (Real.compare o swap o apply2 snd)
  30.275 +        val goal_feats =
  30.276 +          fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
  30.277 +          |> debug ? sort (Real.compare o swap o apply2 snd)
  30.278  
  30.279 -    val parents = maximal_wrt_access_graph access_G facts
  30.280 -    val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
  30.281 +        val parents = maximal_wrt_access_graph access_G facts
  30.282 +        val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
  30.283  
  30.284 -    val suggs =
  30.285 -      if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then
  30.286 -        let
  30.287 -          val learns =
  30.288 -            Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
  30.289 -        in
  30.290 -          MaSh.query_external ctxt algorithm max_suggs learns goal_feats
  30.291 -        end
  30.292 -      else
  30.293 -        let
  30.294 -          val int_goal_feats =
  30.295 -            map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
  30.296 -        in
  30.297 -          MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts max_suggs
  30.298 -            goal_feats int_goal_feats
  30.299 -        end
  30.300 +        val suggs =
  30.301 +          if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then
  30.302 +            let
  30.303 +              val learns =
  30.304 +                Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps))
  30.305 +                  access_G
  30.306 +            in
  30.307 +              MaSh.query_external ctxt algorithm max_suggs learns goal_feats
  30.308 +            end
  30.309 +          else
  30.310 +            let
  30.311 +              val int_goal_feats =
  30.312 +                map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
  30.313 +            in
  30.314 +              MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts
  30.315 +                max_suggs goal_feats int_goal_feats
  30.316 +            end
  30.317  
  30.318 -    val unknown = filter_out (is_fact_in_graph access_G o snd) facts
  30.319 -  in
  30.320 -    find_mash_suggestions ctxt max_suggs suggs facts chained unknown
  30.321 -    |> apply2 (map fact_of_raw_fact)
  30.322 +        val unknown = filter_out (is_fact_in_graph access_G o snd) facts
  30.323 +      in
  30.324 +        find_mash_suggestions ctxt max_suggs suggs facts chained unknown
  30.325 +        |> apply2 (map fact_of_raw_fact)
  30.326 +      end)
  30.327    end
  30.328  
  30.329 -fun mash_unlearn () = (clear_state (); writeln "Reset MaSh")
  30.330 +fun mash_unlearn ctxt = (clear_state ctxt; writeln "Reset MaSh")
  30.331  
  30.332  fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
  30.333      (accum as (access_G, (fact_xtab, feat_xtab))) =
  30.334 @@ -1363,164 +1377,169 @@
  30.335    let
  30.336      val timer = Timer.startRealTimer ()
  30.337      fun next_commit_time () = Timer.checkRealTimer timer + commit_timeout
  30.338 -
  30.339 -    val {access_G, ...} = get_state ctxt
  30.340 -    val is_in_access_G = is_fact_in_graph access_G o snd
  30.341 -    val no_new_facts = forall is_in_access_G facts
  30.342    in
  30.343 -    if no_new_facts andalso not run_prover then
  30.344 -      if auto_level < 2 then
  30.345 -        "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^
  30.346 -        (if auto_level = 0 andalso not run_prover then
  30.347 -           "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover"
  30.348 -         else
  30.349 -           "")
  30.350 -      else
  30.351 -        ""
  30.352 -    else
  30.353 +    (case get_state ctxt of
  30.354 +      NONE => "MaSh is busy\nPlease try again later"
  30.355 +    | SOME {access_G, ...} =>
  30.356        let
  30.357 -        val name_tabs = build_name_tables nickname_of_thm facts
  30.358 +        val is_in_access_G = is_fact_in_graph access_G o snd
  30.359 +        val no_new_facts = forall is_in_access_G facts
  30.360 +      in
  30.361 +        if no_new_facts andalso not run_prover then
  30.362 +          if auto_level < 2 then
  30.363 +            "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^
  30.364 +            (if auto_level = 0 andalso not run_prover then
  30.365 +               "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover"
  30.366 +             else
  30.367 +               "")
  30.368 +          else
  30.369 +            ""
  30.370 +        else
  30.371 +          let
  30.372 +            val name_tabs = build_name_tables nickname_of_thm facts
  30.373  
  30.374 -        fun deps_of status th =
  30.375 -          if status = Non_Rec_Def orelse status = Rec_Def then
  30.376 -            SOME []
  30.377 -          else if run_prover then
  30.378 -            prover_dependencies_of ctxt params prover auto_level facts name_tabs th
  30.379 -            |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
  30.380 -          else
  30.381 -            isar_dependencies_of name_tabs th
  30.382 +            fun deps_of status th =
  30.383 +              if status = Non_Rec_Def orelse status = Rec_Def then
  30.384 +                SOME []
  30.385 +              else if run_prover then
  30.386 +                prover_dependencies_of ctxt params prover auto_level facts name_tabs th
  30.387 +                |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
  30.388 +              else
  30.389 +                isar_dependencies_of name_tabs th
  30.390  
  30.391 -        fun do_commit [] [] [] state = state
  30.392 -          | do_commit learns relearns flops
  30.393 -              {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =
  30.394 -            let
  30.395 -              val was_empty = Graph.is_empty access_G
  30.396 +            fun do_commit [] [] [] state = state
  30.397 +              | do_commit learns relearns flops
  30.398 +                  {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =
  30.399 +                let
  30.400 +                  val was_empty = Graph.is_empty access_G
  30.401  
  30.402 -              val (learns, (access_G', xtabs')) =
  30.403 -                fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
  30.404 -                |>> map_filter I
  30.405 -              val (relearns, access_G'') =
  30.406 -                fold_map (relearn_wrt_access_graph ctxt) relearns access_G'
  30.407 +                  val (learns, (access_G', xtabs')) =
  30.408 +                    fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
  30.409 +                    |>> map_filter I
  30.410 +                  val (relearns, access_G'') =
  30.411 +                    fold_map (relearn_wrt_access_graph ctxt) relearns access_G'
  30.412  
  30.413 -              val access_G''' = access_G'' |> fold flop_wrt_access_graph flops
  30.414 -              val dirty_facts' =
  30.415 -                (case (was_empty, dirty_facts) of
  30.416 -                  (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
  30.417 -                | _ => NONE)
  30.418 +                  val access_G''' = access_G'' |> fold flop_wrt_access_graph flops
  30.419 +                  val dirty_facts' =
  30.420 +                    (case (was_empty, dirty_facts) of
  30.421 +                      (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
  30.422 +                    | _ => NONE)
  30.423  
  30.424 -              val (ffds', freqs') =
  30.425 -                if null relearns then
  30.426 -                  recompute_ffds_freqs_from_learns
  30.427 -                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' num_facts0
  30.428 -                    ffds freqs
  30.429 -                else
  30.430 -                  recompute_ffds_freqs_from_access_G access_G''' xtabs'
  30.431 -            in
  30.432 -              {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs',
  30.433 -               dirty_facts = dirty_facts'}
  30.434 -            end
  30.435 +                  val (ffds', freqs') =
  30.436 +                    if null relearns then
  30.437 +                      recompute_ffds_freqs_from_learns
  30.438 +                        (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs'
  30.439 +                        num_facts0 ffds freqs
  30.440 +                    else
  30.441 +                      recompute_ffds_freqs_from_access_G access_G''' xtabs'
  30.442 +                in
  30.443 +                  {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs',
  30.444 +                   dirty_facts = dirty_facts'}
  30.445 +                end
  30.446  
  30.447 -        fun commit last learns relearns flops =
  30.448 -          (if debug andalso auto_level = 0 then writeln "Committing..." else ();
  30.449 -           map_state ctxt (do_commit (rev learns) relearns flops);
  30.450 -           if not last andalso auto_level = 0 then
  30.451 -             let val num_proofs = length learns + length relearns in
  30.452 -               writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
  30.453 -                 (if run_prover then "automatic" else "Isar") ^ " proof" ^
  30.454 -                 plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout)
  30.455 -             end
  30.456 -           else
  30.457 -             ())
  30.458 +            fun commit last learns relearns flops =
  30.459 +              (if debug andalso auto_level = 0 then writeln "Committing..." else ();
  30.460 +               map_state ctxt (do_commit (rev learns) relearns flops);
  30.461 +               if not last andalso auto_level = 0 then
  30.462 +                 let val num_proofs = length learns + length relearns in
  30.463 +                   writeln ("Learned " ^ string_of_int num_proofs ^ " " ^
  30.464 +                     (if run_prover then "automatic" else "Isar") ^ " proof" ^
  30.465 +                     plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout)
  30.466 +                 end
  30.467 +               else
  30.468 +                 ())
  30.469  
  30.470 -        fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
  30.471 -          | learn_new_fact (parents, ((_, stature as (_, status)), th))
  30.472 -              (learns, (num_nontrivial, next_commit, _)) =
  30.473 -            let
  30.474 -              val name = nickname_of_thm th
  30.475 -              val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
  30.476 -              val deps = these (deps_of status th)
  30.477 -              val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
  30.478 -              val learns = (name, parents, feats, deps) :: learns
  30.479 -              val (learns, next_commit) =
  30.480 -                if Timer.checkRealTimer timer > next_commit then
  30.481 -                  (commit false learns [] []; ([], next_commit_time ()))
  30.482 -                else
  30.483 -                  (learns, next_commit)
  30.484 -              val timed_out = Timer.checkRealTimer timer > learn_timeout
  30.485 -            in
  30.486 -              (learns, (num_nontrivial, next_commit, timed_out))
  30.487 -            end
  30.488 +            fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
  30.489 +              | learn_new_fact (parents, ((_, stature as (_, status)), th))
  30.490 +                  (learns, (num_nontrivial, next_commit, _)) =
  30.491 +                let
  30.492 +                  val name = nickname_of_thm th
  30.493 +                  val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
  30.494 +                  val deps = these (deps_of status th)
  30.495 +                  val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
  30.496 +                  val learns = (name, parents, feats, deps) :: learns
  30.497 +                  val (learns, next_commit) =
  30.498 +                    if Timer.checkRealTimer timer > next_commit then
  30.499 +                      (commit false learns [] []; ([], next_commit_time ()))
  30.500 +                    else
  30.501 +                      (learns, next_commit)
  30.502 +                  val timed_out = Timer.checkRealTimer timer > learn_timeout
  30.503 +                in
  30.504 +                  (learns, (num_nontrivial, next_commit, timed_out))
  30.505 +                end
  30.506  
  30.507 -        val (num_new_facts, num_nontrivial) =
  30.508 -          if no_new_facts then
  30.509 -            (0, 0)
  30.510 -          else
  30.511 -            let
  30.512 -              val new_facts = facts
  30.513 -                |> sort (crude_thm_ord ctxt o apply2 snd)
  30.514 -                |> attach_parents_to_facts []
  30.515 -                |> filter_out (is_in_access_G o snd)
  30.516 -              val (learns, (num_nontrivial, _, _)) =
  30.517 -                ([], (0, next_commit_time (), false))
  30.518 -                |> fold learn_new_fact new_facts
  30.519 -            in
  30.520 -              commit true learns [] []; (length new_facts, num_nontrivial)
  30.521 -            end
  30.522 +            val (num_new_facts, num_nontrivial) =
  30.523 +              if no_new_facts then
  30.524 +                (0, 0)
  30.525 +              else
  30.526 +                let
  30.527 +                  val new_facts = facts
  30.528 +                    |> sort (crude_thm_ord ctxt o apply2 snd)
  30.529 +                    |> attach_parents_to_facts []
  30.530 +                    |> filter_out (is_in_access_G o snd)
  30.531 +                  val (learns, (num_nontrivial, _, _)) =
  30.532 +                    ([], (0, next_commit_time (), false))
  30.533 +                    |> fold learn_new_fact new_facts
  30.534 +                in
  30.535 +                  commit true learns [] []; (length new_facts, num_nontrivial)
  30.536 +                end
  30.537  
  30.538 -        fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
  30.539 -          | relearn_old_fact ((_, (_, status)), th)
  30.540 -              ((relearns, flops), (num_nontrivial, next_commit, _)) =
  30.541 -            let
  30.542 -              val name = nickname_of_thm th
  30.543 -              val (num_nontrivial, relearns, flops) =
  30.544 -                (case deps_of status th of
  30.545 -                  SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
  30.546 -                | NONE => (num_nontrivial, relearns, name :: flops))
  30.547 -              val (relearns, flops, next_commit) =
  30.548 -                if Timer.checkRealTimer timer > next_commit then
  30.549 -                  (commit false [] relearns flops; ([], [], next_commit_time ()))
  30.550 -                else
  30.551 -                  (relearns, flops, next_commit)
  30.552 -              val timed_out = Timer.checkRealTimer timer > learn_timeout
  30.553 -            in
  30.554 -              ((relearns, flops), (num_nontrivial, next_commit, timed_out))
  30.555 -            end
  30.556 +            fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
  30.557 +              | relearn_old_fact ((_, (_, status)), th)
  30.558 +                  ((relearns, flops), (num_nontrivial, next_commit, _)) =
  30.559 +                let
  30.560 +                  val name = nickname_of_thm th
  30.561 +                  val (num_nontrivial, relearns, flops) =
  30.562 +                    (case deps_of status th of
  30.563 +                      SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
  30.564 +                    | NONE => (num_nontrivial, relearns, name :: flops))
  30.565 +                  val (relearns, flops, next_commit) =
  30.566 +                    if Timer.checkRealTimer timer > next_commit then
  30.567 +                      (commit false [] relearns flops; ([], [], next_commit_time ()))
  30.568 +                    else
  30.569 +                      (relearns, flops, next_commit)
  30.570 +                  val timed_out = Timer.checkRealTimer timer > learn_timeout
  30.571 +                in
  30.572 +                  ((relearns, flops), (num_nontrivial, next_commit, timed_out))
  30.573 +                end
  30.574  
  30.575 -        val num_nontrivial =
  30.576 -          if not run_prover then
  30.577 -            num_nontrivial
  30.578 -          else
  30.579 -            let
  30.580 -              val max_isar = 1000 * max_dependencies
  30.581 +            val num_nontrivial =
  30.582 +              if not run_prover then
  30.583 +                num_nontrivial
  30.584 +              else
  30.585 +                let
  30.586 +                  val max_isar = 1000 * max_dependencies
  30.587  
  30.588 -              fun priority_of th =
  30.589 -                Random.random_range 0 max_isar +
  30.590 -                (case try (Graph.get_node access_G) (nickname_of_thm th) of
  30.591 -                  SOME (Isar_Proof, _, deps) => ~100 * length deps
  30.592 -                | SOME (Automatic_Proof, _, _) => 2 * max_isar
  30.593 -                | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar
  30.594 -                | NONE => 0)
  30.595 +                  fun priority_of th =
  30.596 +                    Random.random_range 0 max_isar +
  30.597 +                    (case try (Graph.get_node access_G) (nickname_of_thm th) of
  30.598 +                      SOME (Isar_Proof, _, deps) => ~100 * length deps
  30.599 +                    | SOME (Automatic_Proof, _, _) => 2 * max_isar
  30.600 +                    | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar
  30.601 +                    | NONE => 0)
  30.602  
  30.603 -              val old_facts = facts
  30.604 -                |> filter is_in_access_G
  30.605 -                |> map (`(priority_of o snd))
  30.606 -                |> sort (int_ord o apply2 fst)
  30.607 -                |> map snd
  30.608 -              val ((relearns, flops), (num_nontrivial, _, _)) =
  30.609 -                (([], []), (num_nontrivial, next_commit_time (), false))
  30.610 -                |> fold relearn_old_fact old_facts
  30.611 -            in
  30.612 -              commit true [] relearns flops; num_nontrivial
  30.613 -            end
  30.614 -      in
  30.615 -        if verbose orelse auto_level < 2 then
  30.616 -          "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ " and " ^
  30.617 -          string_of_int num_nontrivial ^ " nontrivial " ^
  30.618 -          (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s num_nontrivial ^
  30.619 -          (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "")
  30.620 -        else
  30.621 -          ""
  30.622 -      end
  30.623 +                  val old_facts = facts
  30.624 +                    |> filter is_in_access_G
  30.625 +                    |> map (`(priority_of o snd))
  30.626 +                    |> sort (int_ord o apply2 fst)
  30.627 +                    |> map snd
  30.628 +                  val ((relearns, flops), (num_nontrivial, _, _)) =
  30.629 +                    (([], []), (num_nontrivial, next_commit_time (), false))
  30.630 +                    |> fold relearn_old_fact old_facts
  30.631 +                in
  30.632 +                  commit true [] relearns flops; num_nontrivial
  30.633 +                end
  30.634 +          in
  30.635 +            if verbose orelse auto_level < 2 then
  30.636 +              "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^
  30.637 +              " and " ^ string_of_int num_nontrivial ^ " nontrivial " ^
  30.638 +              (if run_prover then "automatic and " else "") ^ "Isar proof" ^
  30.639 +              plural_s num_nontrivial ^
  30.640 +              (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "")
  30.641 +            else
  30.642 +              ""
  30.643 +          end
  30.644 +      end)
  30.645    end
  30.646  
  30.647  fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover =
  30.648 @@ -1552,21 +1571,23 @@
  30.649    end
  30.650  
  30.651  fun mash_can_suggest_facts ctxt =
  30.652 -  not (Graph.is_empty (#access_G (get_state ctxt)))
  30.653 +  (case get_state ctxt of
  30.654 +    NONE => false
  30.655 +  | SOME {access_G, ...} => not (Graph.is_empty access_G))
  30.656  
  30.657 -fun mash_can_suggest_facts_fast () =
  30.658 -  (case peek_state () of
  30.659 +fun mash_can_suggest_facts_fast ctxt =
  30.660 +  (case peek_state ctxt of
  30.661      NONE => false
  30.662 -  | SOME (_, {access_G, ...}) => not (Graph.is_empty access_G));
  30.663 +  | SOME (_, {access_G, ...}) => not (Graph.is_empty access_G))
  30.664  
  30.665  (* Generate more suggestions than requested, because some might be thrown out later for various
  30.666     reasons (e.g., duplicates). *)
  30.667  fun generous_max_suggestions max_facts = 3 * max_facts div 2 + 25
  30.668  
  30.669 -val mepo_weight = 0.5
  30.670 -val mash_weight = 0.5
  30.671 +val mepo_weight = 0.5 (* FUDGE *)
  30.672 +val mash_weight = 0.5 (* FUDGE *)
  30.673  
  30.674 -val max_facts_to_learn_before_query = 100
  30.675 +val max_facts_to_learn_before_query = 100 (* FUDGE *)
  30.676  
  30.677  (* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer. *)
  30.678  val min_secs_for_learning = 10
  30.679 @@ -1600,27 +1621,29 @@
  30.680            ()
  30.681  
  30.682        val mash_enabled = is_mash_enabled ()
  30.683 -      val mash_fast = mash_can_suggest_facts_fast ()
  30.684 +      val mash_fast = mash_can_suggest_facts_fast ctxt
  30.685  
  30.686        fun please_learn () =
  30.687          if mash_fast then
  30.688 -          let
  30.689 -            val {access_G, xtabs = ((num_facts0, _), _), ...} = get_state ctxt
  30.690 -            val is_in_access_G = is_fact_in_graph access_G o snd
  30.691 -            val min_num_facts_to_learn = length facts - num_facts0
  30.692 -          in
  30.693 -            if min_num_facts_to_learn <= max_facts_to_learn_before_query then
  30.694 -              (case length (filter_out is_in_access_G facts) of
  30.695 -                0 => ()
  30.696 -              | num_facts_to_learn =>
  30.697 -                if num_facts_to_learn <= max_facts_to_learn_before_query then
  30.698 -                  mash_learn_facts ctxt params prover 2 false timeout facts
  30.699 -                  |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s))
  30.700 -                else
  30.701 -                  maybe_launch_thread true num_facts_to_learn)
  30.702 -            else
  30.703 -              maybe_launch_thread false min_num_facts_to_learn
  30.704 -          end
  30.705 +          (case get_state ctxt of
  30.706 +            NONE => maybe_launch_thread false (length facts)
  30.707 +          | SOME {access_G, xtabs = ((num_facts0, _), _), ...} =>
  30.708 +            let
  30.709 +              val is_in_access_G = is_fact_in_graph access_G o snd
  30.710 +              val min_num_facts_to_learn = length facts - num_facts0
  30.711 +            in
  30.712 +              if min_num_facts_to_learn <= max_facts_to_learn_before_query then
  30.713 +                (case length (filter_out is_in_access_G facts) of
  30.714 +                  0 => ()
  30.715 +                | num_facts_to_learn =>
  30.716 +                  if num_facts_to_learn <= max_facts_to_learn_before_query then
  30.717 +                    mash_learn_facts ctxt params prover 2 false timeout facts
  30.718 +                    |> (fn "" => () | s => writeln (MaShN ^ ": " ^ s))
  30.719 +                  else
  30.720 +                    maybe_launch_thread true num_facts_to_learn)
  30.721 +              else
  30.722 +                maybe_launch_thread false min_num_facts_to_learn
  30.723 +            end)
  30.724          else
  30.725            maybe_launch_thread false (length facts)
  30.726  
    31.1 --- a/src/HOL/Unix/Unix.thy	Thu Nov 24 15:04:05 2016 +0100
    31.2 +++ b/src/HOL/Unix/Unix.thy	Sun Nov 27 20:25:38 2016 +0100
    31.3 @@ -5,9 +5,9 @@
    31.4  section \<open>Unix file-systems \label{sec:unix-file-system}\<close>
    31.5  
    31.6  theory Unix
    31.7 -imports
    31.8 -  Nested_Environment
    31.9 -  "~~/src/HOL/Library/Sublist"
   31.10 +  imports
   31.11 +    Nested_Environment
   31.12 +    "~~/src/HOL/Library/Sublist"
   31.13  begin
   31.14  
   31.15  text \<open>
   31.16 @@ -296,26 +296,26 @@
   31.17  \<close>
   31.18  
   31.19  primrec uid_of :: "operation \<Rightarrow> uid"
   31.20 -where
   31.21 -  "uid_of (Read uid text path) = uid"
   31.22 -| "uid_of (Write uid text path) = uid"
   31.23 -| "uid_of (Chmod uid perms path) = uid"
   31.24 -| "uid_of (Creat uid perms path) = uid"
   31.25 -| "uid_of (Unlink uid path) = uid"
   31.26 -| "uid_of (Mkdir uid path perms) = uid"
   31.27 -| "uid_of (Rmdir uid path) = uid"
   31.28 -| "uid_of (Readdir uid names path) = uid"
   31.29 +  where
   31.30 +    "uid_of (Read uid text path) = uid"
   31.31 +  | "uid_of (Write uid text path) = uid"
   31.32 +  | "uid_of (Chmod uid perms path) = uid"
   31.33 +  | "uid_of (Creat uid perms path) = uid"
   31.34 +  | "uid_of (Unlink uid path) = uid"
   31.35 +  | "uid_of (Mkdir uid path perms) = uid"
   31.36 +  | "uid_of (Rmdir uid path) = uid"
   31.37 +  | "uid_of (Readdir uid names path) = uid"
   31.38  
   31.39  primrec path_of :: "operation \<Rightarrow> path"
   31.40 -where
   31.41 -  "path_of (Read uid text path) = path"
   31.42 -| "path_of (Write uid text path) = path"
   31.43 -| "path_of (Chmod uid perms path) = path"
   31.44 -| "path_of (Creat uid perms path) = path"
   31.45 -| "path_of (Unlink uid path) = path"
   31.46 -| "path_of (Mkdir uid perms path) = path"
   31.47 -| "path_of (Rmdir uid path) = path"
   31.48 -| "path_of (Readdir uid names path) = path"
   31.49 +  where
   31.50 +    "path_of (Read uid text path) = path"
   31.51 +  | "path_of (Write uid text path) = path"
   31.52 +  | "path_of (Chmod uid perms path) = path"
   31.53 +  | "path_of (Creat uid perms path) = path"
   31.54 +  | "path_of (Unlink uid path) = path"
   31.55 +  | "path_of (Mkdir uid perms path) = path"
   31.56 +  | "path_of (Rmdir uid path) = path"
   31.57 +  | "path_of (Readdir uid names path) = path"
   31.58  
   31.59  text \<open>
   31.60    \<^medskip>
   31.61 @@ -340,45 +340,43 @@
   31.62  
   31.63  inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
   31.64    ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
   31.65 -where
   31.66 -  read:
   31.67 -    "root \<midarrow>(Read uid text path)\<rightarrow> root"
   31.68 -    if "access root path uid {Readable} = Some (Val (att, text))"
   31.69 -| "write":
   31.70 -    "root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
   31.71 -    if "access root path uid {Writable} = Some (Val (att, text'))"
   31.72 -| chmod:
   31.73 -    "root \<midarrow>(Chmod uid perms path)\<rightarrow>
   31.74 -      update path (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"
   31.75 -    if "access root path uid {} = Some file" and "uid = 0 \<or> uid = owner (attributes file)"
   31.76 -| creat:
   31.77 -    "root \<midarrow>(Creat uid perms path)\<rightarrow>
   31.78 -      update path (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
   31.79 -    if "path = parent_path @ [name]"
   31.80 -    and "access root parent_path uid {Writable} = Some (Env att parent)"
   31.81 -    and "access root path uid {} = None"
   31.82 -| unlink:
   31.83 -    "root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
   31.84 -    if "path = parent_path @ [name]"
   31.85 -    and "access root parent_path uid {Writable} = Some (Env att parent)"
   31.86 -    and "access root path uid {} = Some (Val plain)"
   31.87 -| mkdir:
   31.88 -    "root \<midarrow>(Mkdir uid perms path)\<rightarrow>
   31.89 -      update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
   31.90 -    if "path = parent_path @ [name]"
   31.91 -    and "access root parent_path uid {Writable} = Some (Env att parent)"
   31.92 -    and "access root path uid {} = None"
   31.93 -|
   31.94 -  rmdir:
   31.95 -    "root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
   31.96 -    if "path = parent_path @ [name]"
   31.97 -    and "access root parent_path uid {Writable} = Some (Env att parent)"
   31.98 -    and "access root path uid {} = Some (Env att' empty)"
   31.99 -|
  31.100 -  readdir:
  31.101 -    "root \<midarrow>(Readdir uid names path)\<rightarrow> root"
  31.102 -    if "access root path uid {Readable} = Some (Env att dir)"
  31.103 -    and "names = dom dir"
  31.104 +  where
  31.105 +    read:
  31.106 +      "root \<midarrow>(Read uid text path)\<rightarrow> root"
  31.107 +      if "access root path uid {Readable} = Some (Val (att, text))"
  31.108 +  | "write":
  31.109 +      "root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
  31.110 +      if "access root path uid {Writable} = Some (Val (att, text'))"
  31.111 +  | chmod:
  31.112 +      "root \<midarrow>(Chmod uid perms path)\<rightarrow>
  31.113 +        update path (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"
  31.114 +      if "access root path uid {} = Some file" and "uid = 0 \<or> uid = owner (attributes file)"
  31.115 +  | creat:
  31.116 +      "root \<midarrow>(Creat uid perms path)\<rightarrow>
  31.117 +        update path (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
  31.118 +      if "path = parent_path @ [name]"
  31.119 +      and "access root parent_path uid {Writable} = Some (Env att parent)"
  31.120 +      and "access root path uid {} = None"
  31.121 +  | unlink:
  31.122 +      "root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
  31.123 +      if "path = parent_path @ [name]"
  31.124 +      and "access root parent_path uid {Writable} = Some (Env att parent)"
  31.125 +      and "access root path uid {} = Some (Val plain)"
  31.126 +  | mkdir:
  31.127 +      "root \<midarrow>(Mkdir uid perms path)\<rightarrow>
  31.128 +        update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
  31.129 +      if "path = parent_path @ [name]"
  31.130 +      and "access root parent_path uid {Writable} = Some (Env att parent)"
  31.131 +      and "access root path uid {} = None"
  31.132 +  | rmdir:
  31.133 +      "root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
  31.134 +      if "path = parent_path @ [name]"
  31.135 +      and "access root parent_path uid {Writable} = Some (Env att parent)"
  31.136 +      and "access root path uid {} = Some (Env att' empty)"
  31.137 +  | readdir:
  31.138 +      "root \<midarrow>(Readdir uid names path)\<rightarrow> root"
  31.139 +      if "access root path uid {Readable} = Some (Env att dir)"
  31.140 +      and "names = dom dir"
  31.141  
  31.142  text \<open>
  31.143    \<^medskip>
  31.144 @@ -480,11 +478,10 @@
  31.145    running processes over a finite amount of time.
  31.146  \<close>
  31.147  
  31.148 -inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
  31.149 -  ("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
  31.150 -where
  31.151 -  nil: "root \<Midarrow>[]\<Rightarrow> root"
  31.152 -| cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"
  31.153 +inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"  ("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
  31.154 +  where
  31.155 +    nil: "root \<Midarrow>[]\<Rightarrow> root"
  31.156 +  | cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"
  31.157  
  31.158  text \<open>
  31.159    \<^medskip>
  31.160 @@ -750,8 +747,7 @@
  31.161      fix xs
  31.162      assume Ps: "\<forall>x \<in> set xs. P x"
  31.163      assume can_exec: "can_exec root (xs @ [y])"
  31.164 -    then obtain root' root'' where
  31.165 -        xs: "root \<Midarrow>xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''"
  31.166 +    then obtain root' root'' where xs: "root \<Midarrow>xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''"
  31.167        by (blast dest: can_exec_snocD)
  31.168      from init_result have "Q root" by (rule init_inv)
  31.169      from preserve_inv xs this Ps have "Q root'"
  31.170 @@ -864,8 +860,7 @@
  31.171    from inv obtain "file" where "access root bogus_path user\<^sub>1 {} = Some file"
  31.172      unfolding invariant_def by blast
  31.173    moreover
  31.174 -  from rmdir obtain att where
  31.175 -      "access root [user\<^sub>1, name\<^sub>1] user\<^sub>1 {} = Some (Env att empty)"
  31.176 +  from rmdir obtain att where "access root [user\<^sub>1, name\<^sub>1] user\<^sub>1 {} = Some (Env att empty)"
  31.177      by cases auto
  31.178    then have "access root ([user\<^sub>1, name\<^sub>1] @ [name\<^sub>2]) user\<^sub>1 {} = empty name\<^sub>2"
  31.179      by (simp only: access_empty_lookup lookup_append_some) simp
    32.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Thu Nov 24 15:04:05 2016 +0100
    32.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Sun Nov 27 20:25:38 2016 +0100
    32.3 @@ -9,7 +9,7 @@
    32.4  section "Bool lists and integers"
    32.5  
    32.6  theory Bool_List_Representation
    32.7 -imports Complex_Main Bits_Int
    32.8 +imports Main Bits_Int
    32.9  begin
   32.10  
   32.11  definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
   32.12 @@ -1106,7 +1106,7 @@
   32.13    apply (case_tac m)
   32.14    apply simp
   32.15    apply (case_tac "m <= n")
   32.16 -   apply auto
   32.17 +   apply (auto simp add: div_add_self2)
   32.18    done
   32.19  
   32.20  lemma bin_rsplit_len: 
    33.1 --- a/src/Pure/Admin/build_history.scala	Thu Nov 24 15:04:05 2016 +0100
    33.2 +++ b/src/Pure/Admin/build_history.scala	Sun Nov 27 20:25:38 2016 +0100
    33.3 @@ -11,8 +11,6 @@
    33.4  import java.time.format.DateTimeFormatter
    33.5  import java.util.Locale
    33.6  
    33.7 -import scala.collection.mutable
    33.8 -
    33.9  
   33.10  object Build_History
   33.11  {
   33.12 @@ -105,7 +103,6 @@
   33.13    def build_history(
   33.14      hg: Mercurial.Repository,
   33.15      progress: Progress = Ignore_Progress,
   33.16 -    progress_result: (Process_Result, Path) => Unit = (result: Process_Result, path: Path) => (),
   33.17      rev: String = default_rev,
   33.18      isabelle_identifier: String = default_isabelle_identifier,
   33.19      components_base: String = "",
   33.20 @@ -259,9 +256,7 @@
   33.21  
   33.22        first_build = false
   33.23  
   33.24 -      val res = (build_result, log_path.ext("xz"))
   33.25 -      progress_result(res._1, res._2)
   33.26 -      res
   33.27 +      (build_result, log_path.ext("xz"))
   33.28      }
   33.29    }
   33.30  
   33.31 @@ -353,13 +348,14 @@
   33.32  
   33.33        val results =
   33.34          build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier,
   33.35 -          progress_result = (_, log_path) => Output.writeln(log_path.implode, stdout = true),
   33.36            components_base = components_base, fresh = fresh, nonfree = nonfree,
   33.37            multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
   33.38            heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
   33.39            max_heap = max_heap, more_settings = more_settings, verbose = verbose,
   33.40            build_tags = build_tags, build_args = build_args)
   33.41  
   33.42 +      for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true)
   33.43 +
   33.44        val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
   33.45        if (rc != 0) sys.exit(rc)
   33.46      }
   33.47 @@ -377,7 +373,6 @@
   33.48      self_update: Boolean = false,
   33.49      push_isabelle_home: Boolean = false,
   33.50      progress: Progress = Ignore_Progress,
   33.51 -    progress_result: (String, Bytes) => Unit = (log_name: String, bytes: Bytes) => (),
   33.52      options: String = "",
   33.53      args: String = ""): (List[(String, Bytes)], Process_Result) =
   33.54    {
   33.55 @@ -403,6 +398,9 @@
   33.56              isabelle_hg.id()
   33.57            }
   33.58          isabelle_hg.update(rev = rev, clean = true)
   33.59 +        ssh.execute(
   33.60 +          ssh.bash_path(isabelle_repos_self + Path.explode("bin/isabelle"))
   33.61 +            + " components -a").check
   33.62          ssh.execute(ssh.bash_path(isabelle_admin + Path.explode("build")) + " jars_fresh").check
   33.63          rev
   33.64        }
   33.65 @@ -417,24 +415,23 @@
   33.66  
   33.67      /* Admin/build_history */
   33.68  
   33.69 -    val result = new mutable.ListBuffer[(String, Bytes)]
   33.70 -
   33.71 -    def progress_stdout(line: String)
   33.72 -    {
   33.73 -      val log = Path.explode(line)
   33.74 -      val res = (log.base.implode, ssh.read_bytes(log))
   33.75 -      ssh.rm(log)
   33.76 -      progress_result(res._1, res._2)
   33.77 -      result += res
   33.78 -    }
   33.79 -
   33.80      val process_result =
   33.81        ssh.execute(
   33.82          ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
   33.83            ssh.bash_path(isabelle_repos_other) + " " + args,
   33.84 -        progress_stdout = progress_stdout _,
   33.85 -        progress_stderr = progress.echo(_))
   33.86 +        progress_stdout = progress.echo(_),
   33.87 +        progress_stderr = progress.echo(_),
   33.88 +        strict = false)
   33.89  
   33.90 -    (result.toList, process_result)
   33.91 +    val result =
   33.92 +      for (line <- process_result.out_lines)
   33.93 +      yield {
   33.94 +        val log = Path.explode(line)
   33.95 +        val bytes = ssh.read_bytes(log)
   33.96 +        ssh.rm(log)
   33.97 +        (log.base.implode, bytes)
   33.98 +      }
   33.99 +
  33.100 +    (result, process_result)
  33.101    }
  33.102  }
    34.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.2 +++ b/src/Pure/Admin/build_polyml.scala	Sun Nov 27 20:25:38 2016 +0100
    34.3 @@ -0,0 +1,224 @@
    34.4 +/*  Title:      Pure/Admin/build_polyml.scala
    34.5 +    Author:     Makarius
    34.6 +
    34.7 +Build Poly/ML from sources.
    34.8 +*/
    34.9 +
   34.10 +package isabelle
   34.11 +
   34.12 +
   34.13 +object Build_PolyML
   34.14 +{
   34.15 +  /** build_polyml **/
   34.16 +
   34.17 +  sealed case class Platform_Info(
   34.18 +    options: List[String] = Nil,
   34.19 +    options_multilib: List[String] = Nil,
   34.20 +    setup: String = "",
   34.21 +    copy_files: List[String] = Nil)
   34.22 +
   34.23 +  private val platform_info = Map(
   34.24 +    "x86-linux" ->
   34.25 +      Platform_Info(
   34.26 +        options_multilib =
   34.27 +          List("--build=i386", "CFLAGS=-m32 -O3", "CXXFLAGS=-m32 -O3", "CCASFLAGS=-m32")),
   34.28 +    "x86_64-linux" -> Platform_Info(),
   34.29 +    "x86-darwin" ->
   34.30 +      Platform_Info(
   34.31 +        options =
   34.32 +          List("--build=i686-darwin", "CFLAGS=-arch i686 -O3 -I../libffi/include",
   34.33 +            "CXXFLAGS=-arch i686 -O3 -I../libffi/include", "CCASFLAGS=-arch i686 -O3",
   34.34 +            "LDFLAGS=-segprot POLY rwx rwx"),
   34.35 +        setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin"),
   34.36 +    "x86_64-darwin" ->
   34.37 +      Platform_Info(
   34.38 +        options =
   34.39 +          List("--build=x86_64-darwin", "CFLAGS=-arch x86_64 -O3 -I../libffi/include",
   34.40 +            "CXXFLAGS=-arch x86_64 -O3 -I../libffi/include", "CCASFLAGS=-arch x86_64",
   34.41 +            "LDFLAGS=-segprot POLY rwx rwx"),
   34.42 +        setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin"),
   34.43 +    "x86-windows" ->
   34.44 +      Platform_Info(
   34.45 +        options =
   34.46 +          List("--host=i686-w32-mingw32", "CPPFLAGS=-I/mingw32/include", "--disable-windows-gui"),
   34.47 +        setup =
   34.48 +          """PATH=/usr/bin:/bin:/mingw32/bin
   34.49 +            export CONFIG_SITE=/etc/config.site""",
   34.50 +        copy_files =
   34.51 +          List("$MSYS/mingw32/bin/libgcc_s_dw2-1.dll",
   34.52 +            "$MSYS/mingw32/bin/libgmp-10.dll",
   34.53 +            "$MSYS/mingw32/bin/libstdc++-6.dll")),
   34.54 +    "x86_64-windows" ->
   34.55 +      Platform_Info(
   34.56 +        options =
   34.57 +          List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
   34.58 +        setup =
   34.59 +          """PATH=/usr/bin:/bin:/mingw64/bin
   34.60 +            export CONFIG_SITE=/etc/config.site""",
   34.61 +        copy_files =
   34.62 +          List("$MSYS/mingw64/bin/libgcc_s_seh-1.dll",
   34.63 +            "$MSYS/mingw64/bin/libgmp-10.dll",
   34.64 +            "$MSYS/mingw64/bin/libstdc++-6.dll")))
   34.65 +
   34.66 +  def build_polyml(
   34.67 +    root: Path,
   34.68 +    sha1_root: Option[Path] = None,
   34.69 +    progress: Progress = Ignore_Progress,
   34.70 +    arch_64: Boolean = false,
   34.71 +    options: List[String] = Nil,
   34.72 +    msys_root: Option[Path] = None,
   34.73 +    component_root: Option[Path] = None)
   34.74 +  {
   34.75 +    if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
   34.76 +      error("Bad Poly/ML root directory: " + root)
   34.77 +
   34.78 +    val platform =
   34.79 +      (if (arch_64) "x86_64" else "x86") +
   34.80 +      (if (Platform.is_windows) "-windows" else if (Platform.is_macos) "-darwin" else "-linux")
   34.81 +
   34.82 +    val info =
   34.83 +      platform_info.get(platform) getOrElse
   34.84 +        error("Bad platform identifier: " + quote(platform))
   34.85 +
   34.86 +    val settings =
   34.87 +      msys_root match {
   34.88 +        case None if Platform.is_windows =>
   34.89 +          error("Windows requires specification of msys root directory")
   34.90 +        case None => Isabelle_System.settings()
   34.91 +        case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode)
   34.92 +      }
   34.93 +
   34.94 +
   34.95 +    /* bash */
   34.96 +
   34.97 +    def bash(
   34.98 +      cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
   34.99 +    {
  34.100 +      val script1 =
  34.101 +        msys_root match {
  34.102 +          case None => script
  34.103 +          case Some(msys) =>
  34.104 +            File.bash_path(msys + Path.explode("usr/bin/bash")) + " -c " + Bash.string(script)
  34.105 +        }
  34.106 +      progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo)
  34.107 +    }
  34.108 +
  34.109 +
  34.110 +    /* component setup */
  34.111 +
  34.112 +    component_root match {
  34.113 +      case None =>
  34.114 +      case Some(component) =>
  34.115 +        val etc = component + Path.explode("etc")
  34.116 +        Isabelle_System.mkdirs(etc)
  34.117 +        File.copy(Path.explode("~~/Admin/polyml/settings"), etc)
  34.118 +        File.copy(Path.explode("~~/Admin/polyml/README"), component)
  34.119 +    }
  34.120 +
  34.121 +
  34.122 +    /* configure and make */
  34.123 +
  34.124 +    val configure_options =
  34.125 +      (if (!arch_64 && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux")
  34.126 +        info.options_multilib
  34.127 +       else info.options) ::: List("--enable-intinf-as-int") ::: options
  34.128 +
  34.129 +    bash(root,
  34.130 +      info.setup + "\n" +
  34.131 +      """
  34.132 +        [ -f Makefile ] && make distclean
  34.133 +        {
  34.134 +          ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
  34.135 +          rm -rf target
  34.136 +          make compiler && make compiler && make install
  34.137 +        } || { echo "Build failed" >&2; exit 2; }
  34.138 +      """, redirect = true, echo = true).check
  34.139 +
  34.140 +    val ldd_files =
  34.141 +      if (Platform.is_linux) {
  34.142 +        val libs = bash(root, "ldd target/bin/poly").check.out_lines
  34.143 +        val Pattern = """\s*libgmp.*=>\s*(\S+).*""".r
  34.144 +        for (Pattern(lib) <- libs) yield lib
  34.145 +      }
  34.146 +      else Nil
  34.147 +
  34.148 +
  34.149 +    /* sha1 library */
  34.150 +
  34.151 +    val sha1_files =
  34.152 +      if (sha1_root.isDefined) {
  34.153 +        val dir1 = sha1_root.get
  34.154 +        bash(dir1, "./build " + platform, redirect = true, echo = true).check
  34.155 +
  34.156 +        if (component_root.isDefined)
  34.157 +          Mercurial.repository(dir1).
  34.158 +            archive(File.standard_path(component_root.get + Path.explode("sha1")))
  34.159 +
  34.160 +        val dir2 = dir1 + Path.explode(platform)
  34.161 +        File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
  34.162 +      }
  34.163 +      else Nil
  34.164 +
  34.165 +
  34.166 +    /* target */
  34.167 +
  34.168 +    val target = component_root.getOrElse(Path.current) + Path.explode(platform)
  34.169 +    Isabelle_System.rm_tree(target)
  34.170 +    Isabelle_System.mkdirs(target)
  34.171 +
  34.172 +    for {
  34.173 +      d <- List("target/bin", "target/lib")
  34.174 +      dir = root + Path.explode(d)
  34.175 +      entry <- File.read_dir(dir)
  34.176 +    } File.move(dir + Path.explode(entry), target)
  34.177 +
  34.178 +    for (file <- "~~/Admin/polyml/polyi" :: info.copy_files ::: ldd_files ::: sha1_files)
  34.179 +      File.copy(Path.explode(file).expand_env(settings), target)
  34.180 +  }
  34.181 +
  34.182 +
  34.183 +
  34.184 +  /** Isabelle tool wrapper **/
  34.185 +
  34.186 +  val isabelle_tool = Isabelle_Tool("build_polyml", "build Poly/ML from sources", args =>
  34.187 +    {
  34.188 +      Command_Line.tool0 {
  34.189 +        var component_root: Option[Path] = None
  34.190 +        var msys_root: Option[Path] = None
  34.191 +        var arch_64 = false
  34.192 +        var sha1_root: Option[Path] = None
  34.193 +
  34.194 +        val getopts = Getopts("""
  34.195 +Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS]
  34.196 +
  34.197 +  Options are:
  34.198 +    -C DIR       Isabelle component root directory (for etc/settings ...)
  34.199 +    -M DIR       msys root directory (for Windows)
  34.200 +    -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
  34.201 +    -s DIR       sha1 sources, see https://bitbucket.org/isabelle_project/sha1
  34.202 +
  34.203 +  Build Poly/ML in the ROOT directory of its sources, with additional
  34.204 +  CONFIGURE_OPTIONS (e.g. --with-gmp).
  34.205 +""",
  34.206 +          "C:" -> (arg => component_root = Some(Path.explode(arg))),
  34.207 +          "M:" -> (arg => msys_root = Some(Path.explode(arg))),
  34.208 +          "m:" ->
  34.209 +            {
  34.210 +              case "32" | "x86" => arch_64 = false
  34.211 +              case "64" | "x86_64" => arch_64 = true
  34.212 +              case bad => error("Bad processor architecture: " + quote(bad))
  34.213 +            },
  34.214 +          "s:" -> (arg => sha1_root = Some(Path.explode(arg))))
  34.215 +
  34.216 +        val more_args = getopts(args)
  34.217 +        val (root, options) =
  34.218 +          more_args match {
  34.219 +            case root :: options => (Path.explode(root), options)
  34.220 +            case Nil => getopts.usage()
  34.221 +          }
  34.222 +        build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
  34.223 +          arch_64 = arch_64, options = options, component_root = component_root,
  34.224 +          msys_root = msys_root)
  34.225 +      }
  34.226 +    }, admin = true)
  34.227 +}
    35.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Nov 24 15:04:05 2016 +0100
    35.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 27 20:25:38 2016 +0100
    35.3 @@ -59,8 +59,8 @@
    35.4            Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
    35.5              parallel_jobs = 4, remote_mac = "macbroy31", website = Some(new_snapshot))
    35.6  
    35.7 -          if (release_snapshot.is_dir) File.mv(release_snapshot, old_snapshot)
    35.8 -          File.mv(new_snapshot, release_snapshot)
    35.9 +          if (release_snapshot.is_dir) File.move(release_snapshot, old_snapshot)
   35.10 +          File.move(new_snapshot, release_snapshot)
   35.11            Isabelle_System.rm_tree(old_snapshot)
   35.12          }))
   35.13  
   35.14 @@ -79,7 +79,7 @@
   35.15                hg, rev = "build_history_base", fresh = true, build_args = List("HOL"))
   35.16          } {
   35.17            result.check
   35.18 -          File.copy(log_path, logger.log_dir + log_path.base)
   35.19 +          File.move(log_path, logger.log_dir + log_path.base)
   35.20          }
   35.21        })
   35.22  
   35.23 @@ -96,7 +96,11 @@
   35.24  
   35.25    private val remote_builds =
   35.26      List(
   35.27 -      List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6 -N", args = "-g timing")),
   35.28 +      List(Remote_Build("lxbroy8",
   35.29 +        options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-7a7b742897e9'",
   35.30 +        args = "-N -g timing")),
   35.31 +      List(Remote_Build("lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")),
   35.32 +      List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
   35.33        List(
   35.34          Remote_Build("macbroy2", options = "-m32 -M8", args = "-a"),
   35.35          Remote_Build("macbroy2", options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty"),
   35.36 @@ -118,19 +122,21 @@
   35.37                val self_update = !r.shared_home
   35.38                val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
   35.39  
   35.40 -              def progress_result(log_name: String, bytes: Bytes): Unit =
   35.41 -                Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
   35.42 +              val (results, _) =
   35.43 +                Build_History.remote_build_history(ssh,
   35.44 +                  isabelle_repos,
   35.45 +                  isabelle_repos.ext(r.host),
   35.46 +                  isabelle_repos_source = isabelle_release_source,
   35.47 +                  self_update = self_update,
   35.48 +                  push_isabelle_home = push_isabelle_home,
   35.49 +                  options =
   35.50 +                    "-r " + Bash.string(rev) + " -N " + Bash.string(task_name) + " -f " + r.options,
   35.51 +                  args = "-o timeout=10800 " + r.args)
   35.52  
   35.53 -              Build_History.remote_build_history(ssh,
   35.54 -                isabelle_repos,
   35.55 -                isabelle_repos.ext(r.host),
   35.56 -                isabelle_repos_source = isabelle_dev_source,
   35.57 -                self_update = self_update,
   35.58 -                push_isabelle_home = push_isabelle_home,
   35.59 -                progress_result = progress_result _,
   35.60 -                options =
   35.61 -                  r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
   35.62 -                args = "-o timeout=10800 " + r.args)
   35.63 +              for ((log_name, bytes) <- results) {
   35.64 +                logger.log(Date.now(), log_name)
   35.65 +                Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
   35.66 +              }
   35.67              })
   35.68        })
   35.69    }
    36.1 --- a/src/Pure/General/file.scala	Thu Nov 24 15:04:05 2016 +0100
    36.2 +++ b/src/Pure/General/file.scala	Sun Nov 27 20:25:38 2016 +0100
    36.3 @@ -220,13 +220,13 @@
    36.4  
    36.5    def write_backup(path: Path, text: CharSequence)
    36.6    {
    36.7 -    if (path.is_file) mv(path, path.backup)
    36.8 +    if (path.is_file) move(path, path.backup)
    36.9      write(path, text)
   36.10    }
   36.11  
   36.12    def write_backup2(path: Path, text: CharSequence)
   36.13    {
   36.14 -    if (path.is_file) mv(path, path.backup2)
   36.15 +    if (path.is_file) move(path, path.backup2)
   36.16      write(path, text)
   36.17    }
   36.18  
   36.19 @@ -265,8 +265,12 @@
   36.20  
   36.21    /* move */
   36.22  
   36.23 -  def mv(file1: JFile, file2: JFile): Unit =
   36.24 -    Files.move(file1.toPath, file2.toPath, StandardCopyOption.REPLACE_EXISTING)
   36.25 +  def move(src: JFile, dst: JFile)
   36.26 +  {
   36.27 +    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
   36.28 +    if (!eq(src, target))
   36.29 +      Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
   36.30 +  }
   36.31  
   36.32 -  def mv(path1: Path, path2: Path): Unit = mv(path1.file, path2.file)
   36.33 +  def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file)
   36.34  }
    37.1 --- a/src/Pure/General/mercurial.scala	Thu Nov 24 15:04:05 2016 +0100
    37.2 +++ b/src/Pure/General/mercurial.scala	Sun Nov 27 20:25:38 2016 +0100
    37.3 @@ -54,7 +54,7 @@
    37.4          case None => root.is_dir
    37.5          case Some(ssh) => ssh.is_dir(root)
    37.6        }
    37.7 -    if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg }
    37.8 +    if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
    37.9      else clone_repository(source, root, options = "--noupdate", ssh = ssh)
   37.10    }
   37.11  
   37.12 @@ -92,6 +92,9 @@
   37.13        }
   37.14      }
   37.15  
   37.16 +    def archive(target: String, rev: String = "", options: String = ""): Unit =
   37.17 +      hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
   37.18 +
   37.19      def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
   37.20        hg.command("heads", opt_template(template), options).check.out_lines
   37.21  
    38.1 --- a/src/Pure/General/symbol.scala	Thu Nov 24 15:04:05 2016 +0100
    38.2 +++ b/src/Pure/General/symbol.scala	Sun Nov 27 20:25:38 2016 +0100
    38.3 @@ -197,7 +197,7 @@
    38.4    }
    38.5  
    38.6  
    38.7 -  /* text chunks */
    38.8 +  /* symbolic text chunks -- without actual text */
    38.9  
   38.10    object Text_Chunk
   38.11    {
    39.1 --- a/src/Pure/Isar/parse.scala	Thu Nov 24 15:04:05 2016 +0100
    39.2 +++ b/src/Pure/Isar/parse.scala	Sun Nov 27 20:25:38 2016 +0100
    39.3 @@ -64,12 +64,13 @@
    39.4      def string: Parser[String] = atom("string", _.is_string)
    39.5      def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
    39.6      def name: Parser[String] = atom("name", _.is_name)
    39.7 +    def embedded: Parser[String] = atom("embedded content", _.is_embedded)
    39.8      def text: Parser[String] = atom("text", _.is_text)
    39.9      def ML_source: Parser[String] = atom("ML source", _.is_text)
   39.10      def document_source: Parser[String] = atom("document source", _.is_text)
   39.11  
   39.12      def path: Parser[String] =
   39.13 -      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
   39.14 +      atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
   39.15  
   39.16      def theory_name: Parser[String] =
   39.17        atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
    40.1 --- a/src/Pure/Isar/token.scala	Thu Nov 24 15:04:05 2016 +0100
    40.2 +++ b/src/Pure/Isar/token.scala	Sun Nov 27 20:25:38 2016 +0100
    40.3 @@ -242,6 +242,11 @@
    40.4      kind == Token.Kind.SYM_IDENT ||
    40.5      kind == Token.Kind.STRING ||
    40.6      kind == Token.Kind.NAT
    40.7 +  def is_embedded: Boolean = is_name ||
    40.8 +    kind == Token.Kind.CARTOUCHE ||
    40.9 +    kind == Token.Kind.VAR ||
   40.10 +    kind == Token.Kind.TYPE_IDENT ||
   40.11 +    kind == Token.Kind.TYPE_VAR
   40.12    def is_text: Boolean = is_name || kind == Token.Kind.VERBATIM || kind == Token.Kind.CARTOUCHE
   40.13    def is_space: Boolean = kind == Token.Kind.SPACE
   40.14    def is_comment: Boolean = kind == Token.Kind.COMMENT
    41.1 --- a/src/Pure/PIDE/command.scala	Thu Nov 24 15:04:05 2016 +0100
    41.2 +++ b/src/Pure/PIDE/command.scala	Sun Nov 27 20:25:38 2016 +0100
    41.3 @@ -322,7 +322,7 @@
    41.4    private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
    41.5      if (tokens.exists({ case (t, _) => t.is_command })) {
    41.6        tokens.dropWhile({ case (t, _) => !t.is_command }).
    41.7 -        collectFirst({ case (t, i) if t.is_name => (t.content, i) })
    41.8 +        collectFirst({ case (t, i) if t.is_embedded => (t.content, i) })
    41.9      }
   41.10      else None
   41.11  
    42.1 --- a/src/Pure/PIDE/editor.scala	Thu Nov 24 15:04:05 2016 +0100
    42.2 +++ b/src/Pure/PIDE/editor.scala	Sun Nov 27 20:25:38 2016 +0100
    42.3 @@ -12,6 +12,7 @@
    42.4    def session: Session
    42.5    def flush(hidden: Boolean = true): Unit
    42.6    def invoke(): Unit
    42.7 +  def invoke_generated(): Unit
    42.8    def current_context: Context
    42.9    def current_node(context: Context): Option[Document.Node.Name]
   42.10    def current_node_snapshot(context: Context): Option[Document.Snapshot]
    43.1 --- a/src/Pure/System/isabelle_system.scala	Thu Nov 24 15:04:05 2016 +0100
    43.2 +++ b/src/Pure/System/isabelle_system.scala	Sun Nov 27 20:25:38 2016 +0100
    43.3 @@ -107,12 +107,14 @@
    43.4          dump.deleteOnExit
    43.5          try {
    43.6            val cmd1 =
    43.7 -            if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l") else Nil
    43.8 -          val cmd2 =
    43.9 -            List(isabelle_root1 + JFile.separator + "bin" + JFile.separator + "isabelle",
   43.10 -              "getenv", "-d", dump.toString)
   43.11 +            if (Platform.is_windows)
   43.12 +              List(cygwin_root1 + "\\bin\\bash", "-l",
   43.13 +                File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
   43.14 +            else
   43.15 +              List(isabelle_root1 + "/bin/isabelle")
   43.16 +          val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
   43.17  
   43.18 -          val (output, rc) = process_output(process(cmd1 ::: cmd2, env = env, redirect = true))
   43.19 +          val (output, rc) = process_output(process(cmd, env = env, redirect = true))
   43.20            if (rc != 0) error(output)
   43.21  
   43.22            val entries =
    44.1 --- a/src/Pure/System/isabelle_tool.scala	Thu Nov 24 15:04:05 2016 +0100
    44.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Nov 27 20:25:38 2016 +0100
    44.3 @@ -101,6 +101,7 @@
    44.4      List(
    44.5        Build.isabelle_tool,
    44.6        Build_Doc.isabelle_tool,
    44.7 +      Build_PolyML.isabelle_tool,
    44.8        Build_Stats.isabelle_tool,
    44.9        Check_Sources.isabelle_tool,
   44.10        Doc.isabelle_tool,
    45.1 --- a/src/Pure/System/numa.scala	Thu Nov 24 15:04:05 2016 +0100
    45.2 +++ b/src/Pure/System/numa.scala	Sun Nov 27 20:25:38 2016 +0100
    45.3 @@ -26,7 +26,7 @@
    45.4        }
    45.5  
    45.6      if (numa_nodes_linux.is_file) {
    45.7 -      Library.space_explode(',', Library.trim_line(File.read(numa_nodes_linux))).flatMap(read(_))
    45.8 +      Library.space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
    45.9      }
   45.10      else Nil
   45.11    }
    46.1 --- a/src/Pure/System/platform.scala	Thu Nov 24 15:04:05 2016 +0100
    46.2 +++ b/src/Pure/System/platform.scala	Sun Nov 27 20:25:38 2016 +0100
    46.3 @@ -14,6 +14,7 @@
    46.4  {
    46.5    /* main OS variants */
    46.6  
    46.7 +  val is_linux = System.getProperty("os.name", "") == "Linux"
    46.8    val is_macos = System.getProperty("os.name", "") == "Mac OS X"
    46.9    val is_windows = System.getProperty("os.name", "").startsWith("Windows")
   46.10  
    47.1 --- a/src/Pure/Thy/latex.ML	Thu Nov 24 15:04:05 2016 +0100
    47.2 +++ b/src/Pure/Thy/latex.ML	Sun Nov 27 20:25:38 2016 +0100
    47.3 @@ -106,21 +106,30 @@
    47.4    | Symbol.Malformed s => error (Symbol.malformed_msg s)
    47.5    | Symbol.EOF => error "Bad EOF symbol");
    47.6  
    47.7 +val scan_latex_length =
    47.8 +  Scan.many1 (fn (s, _) => Symbol.not_eof s andalso not (is_latex_control s))
    47.9 +    >> (Symbol.length o map Symbol_Pos.symbol) ||
   47.10 +  Scan.one (is_latex_control o Symbol_Pos.symbol) --
   47.11 +    Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
   47.12 +
   47.13  fun scan_latex known =
   47.14    Scan.one (is_latex_control o Symbol_Pos.symbol) |--
   47.15      Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) ||
   47.16    Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol);
   47.17  
   47.18 -fun read_latex known syms =
   47.19 -  (case Scan.read Symbol_Pos.stopper (Scan.repeat (scan_latex known))
   47.20 -      (map (rpair Position.none) syms) of
   47.21 -    SOME ss => implode ss
   47.22 -  | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)));
   47.23 +fun read scan syms =
   47.24 +  Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
   47.25  
   47.26  in
   47.27  
   47.28 +fun length_symbols syms =
   47.29 +  fold Integer.add (these (read scan_latex_length syms)) 0;
   47.30 +
   47.31  fun output_known_symbols known syms =
   47.32 -  if exists is_latex_control syms then read_latex known syms
   47.33 +  if exists is_latex_control syms then
   47.34 +    (case read (scan_latex known) syms of
   47.35 +      SOME ss => implode ss
   47.36 +    | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
   47.37    else implode (map (output_known_sym known) syms);
   47.38  
   47.39  val output_symbols = output_known_symbols (K true, K true);
   47.40 @@ -201,7 +210,7 @@
   47.41  
   47.42  fun latex_output str =
   47.43    let val syms = Symbol.explode str
   47.44 -  in (output_symbols syms, Symbol.length syms) end;
   47.45 +  in (output_symbols syms, length_symbols syms) end;
   47.46  
   47.47  fun latex_markup (s, _) =
   47.48    if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
    48.1 --- a/src/Pure/Tools/build.scala	Thu Nov 24 15:04:05 2016 +0100
    48.2 +++ b/src/Pure/Tools/build.scala	Sun Nov 27 20:25:38 2016 +0100
    48.3 @@ -751,7 +751,7 @@
    48.4  
    48.5    Build and manage Isabelle sessions, depending on implicit settings:
    48.6  
    48.7 -""" + Library.prefix_lines("  ", Build_Log.Settings.show()),
    48.8 +""" + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
    48.9        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   48.10        "N" -> (_ => numa_shuffling = true),
   48.11        "R" -> (_ => requirements = true),
    49.1 --- a/src/Pure/build-jars	Thu Nov 24 15:04:05 2016 +0100
    49.2 +++ b/src/Pure/build-jars	Sun Nov 27 20:25:38 2016 +0100
    49.3 @@ -12,6 +12,7 @@
    49.4    Admin/build_doc.scala
    49.5    Admin/build_history.scala
    49.6    Admin/build_log.scala
    49.7 +  Admin/build_polyml.scala
    49.8    Admin/build_release.scala
    49.9    Admin/build_stats.scala
   49.10    Admin/check_sources.scala
    50.1 --- a/src/Pure/theory.ML	Thu Nov 24 15:04:05 2016 +0100
    50.2 +++ b/src/Pure/theory.ML	Sun Nov 27 20:25:38 2016 +0100
    50.3 @@ -220,9 +220,6 @@
    50.4  
    50.5  fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
    50.6    let
    50.7 -    val thy = Proof_Context.theory_of ctxt;
    50.8 -    val consts = Sign.consts_of thy;
    50.9 -
   50.10      fun prep (item, args) =
   50.11        (case fold Term.add_tvarsT args [] of
   50.12          [] => (item, map Logic.varifyT_global args)
    51.1 --- a/src/Tools/Code/code_scala.ML	Thu Nov 24 15:04:05 2016 +0100
    51.2 +++ b/src/Tools/Code/code_scala.ML	Sun Nov 27 20:25:38 2016 +0100
    51.3 @@ -443,7 +443,7 @@
    51.4      else if c = "\\" then "\\\\"
    51.5      else let val k = ord c
    51.6      in if k < 32 orelse k > 126
    51.7 -    then "\\u" ^ align_right "0" 4 (radixstring (8, "0", k)) else c end
    51.8 +    then "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX k) else c end
    51.9    fun numeral_scala k =
   51.10      if ~2147483647 < k andalso k <= 2147483647
   51.11      then signed_string_of_int k
    52.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Nov 24 15:04:05 2016 +0100
    52.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Nov 27 20:25:38 2016 +0100
    52.3 @@ -111,7 +111,7 @@
    52.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    52.5      {
    52.6        // no robust_body
    52.7 -      PIDE.editor.invoke()
    52.8 +      PIDE.editor.invoke_generated()
    52.9      }
   52.10    }
   52.11  
    53.1 --- a/src/Tools/jEdit/src/isabelle.scala	Thu Nov 24 15:04:05 2016 +0100
    53.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sun Nov 27 20:25:38 2016 +0100
    53.3 @@ -338,9 +338,9 @@
    53.4                  JEdit_Lib.buffer_edit(buffer) {
    53.5                    if (padding) {
    53.6                      text_area.moveCaretPosition(start + range.length)
    53.7 +                    val start_line = text_area.getCaretLine + 1
    53.8                      text_area.setSelectedText("\n" + text)
    53.9                      val end_line = text_area.getCaretLine
   53.10 -                    val start_line = end_line - split_lines(text).length
   53.11                      buffer.indentLines(start_line, end_line)
   53.12                    }
   53.13                    else {
    54.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Nov 24 15:04:05 2016 +0100
    54.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 27 20:25:38 2016 +0100
    54.3 @@ -44,10 +44,14 @@
    54.4      session.update(doc_blobs, edits)
    54.5    }
    54.6  
    54.7 -  private val delay_flush =
    54.8 +  private val delay1_flush =
    54.9      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
   54.10  
   54.11 -  def invoke(): Unit = delay_flush.invoke()
   54.12 +  private val delay2_flush =
   54.13 +    GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
   54.14 +
   54.15 +  def invoke(): Unit = delay1_flush.invoke()
   54.16 +  def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
   54.17  
   54.18    def stable_tip_version(): Option[Document.Version] =
   54.19      GUI_Thread.require {
    55.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Nov 24 15:04:05 2016 +0100
    55.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 27 20:25:38 2016 +0100
    55.3 @@ -125,7 +125,7 @@
    55.4          else if (plugin != null) plugin.delay_init.invoke()
    55.5        }
    55.6  
    55.7 -      PIDE.editor.invoke()
    55.8 +      PIDE.editor.invoke_generated()
    55.9      }
   55.10    }
   55.11  
   55.12 @@ -223,7 +223,7 @@
   55.13              if (PIDE.options.bool("jedit_auto_resolve")) {
   55.14                PIDE.editor.stable_tip_version() match {
   55.15                  case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node)
   55.16 -                case None => Nil
   55.17 +                case None => delay_load.invoke(); Nil
   55.18                }
   55.19              }
   55.20              else Nil
   55.21 @@ -263,7 +263,7 @@
   55.22      }
   55.23    }
   55.24  
   55.25 -  lazy val delay_load =
   55.26 +  private lazy val delay_load =
   55.27      GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() }
   55.28  
   55.29  
    56.1 --- a/src/Tools/jEdit/src/text_structure.scala	Thu Nov 24 15:04:05 2016 +0100
    56.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Sun Nov 27 20:25:38 2016 +0100
    56.3 @@ -44,7 +44,7 @@
    56.4      private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open
    56.5      private val keyword_close = Keyword.proof_close
    56.6  
    56.7 -    def apply(buffer: JEditBuffer, current_line: Int, prev_line: Int, prev_prev_line: Int,
    56.8 +    def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
    56.9        actions: java.util.List[IndentAction])
   56.10      {
   56.11        Isabelle.buffer_syntax(buffer) match {
   56.12 @@ -68,6 +68,11 @@
   56.13                case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
   56.14              }
   56.15  
   56.16 +          val prev_line: Int =
   56.17 +            Range.inclusive(current_line - 1, 0, -1).find(line =>
   56.18 +              Token_Markup.Line_Context.prev(buffer, line).get_context == Scan.Finished &&
   56.19 +              !Token_Markup.Line_Context.next(buffer, line).structure.improper) getOrElse -1
   56.20 +
   56.21            def prev_line_command: Option[Token] =
   56.22              nav.reverse_iterator(prev_line, 1).
   56.23                collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok })
   56.24 @@ -135,33 +140,36 @@
   56.25              else 0
   56.26  
   56.27            val indent =
   56.28 -            line_head(current_line) match {
   56.29 -              case None => indent_structure + indent_brackets + indent_extra
   56.30 -              case Some(info @ Text.Info(range, tok)) =>
   56.31 -                if (tok.is_begin ||
   56.32 -                    keywords.is_before_command(tok) ||
   56.33 -                    keywords.is_command(tok, Keyword.theory)) 0
   56.34 -                else if (keywords.is_command(tok, Keyword.proof_enclose))
   56.35 -                  indent_structure + script_indent(info) - indent_offset(tok)
   56.36 -                else if (keywords.is_command(tok, Keyword.proof))
   56.37 -                  (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
   56.38 -                else if (tok.is_command) indent_structure - indent_offset(tok)
   56.39 -                else {
   56.40 -                  prev_line_command match {
   56.41 -                    case None =>
   56.42 -                      val extra =
   56.43 -                        (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
   56.44 -                          case (true, true) | (false, false) => 0
   56.45 -                          case (true, false) => - indent_extra
   56.46 -                          case (false, true) => indent_extra
   56.47 -                        }
   56.48 -                      line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
   56.49 -                    case Some(prev_tok) =>
   56.50 -                      indent_structure + indent_brackets + indent_size - indent_offset(tok) -
   56.51 -                      indent_offset(prev_tok) - indent_indent(prev_tok)
   56.52 -                  }
   56.53 -               }
   56.54 +            if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
   56.55 +              line_head(current_line) match {
   56.56 +                case None => indent_structure + indent_brackets + indent_extra
   56.57 +                case Some(info @ Text.Info(range, tok)) =>
   56.58 +                  if (tok.is_begin ||
   56.59 +                      keywords.is_before_command(tok) ||
   56.60 +                      keywords.is_command(tok, Keyword.theory)) 0
   56.61 +                  else if (keywords.is_command(tok, Keyword.proof_enclose))
   56.62 +                    indent_structure + script_indent(info) - indent_offset(tok)
   56.63 +                  else if (keywords.is_command(tok, Keyword.proof))
   56.64 +                    (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
   56.65 +                  else if (tok.is_command) indent_structure - indent_offset(tok)
   56.66 +                  else {
   56.67 +                    prev_line_command match {
   56.68 +                      case None =>
   56.69 +                        val extra =
   56.70 +                          (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
   56.71 +                            case (true, true) | (false, false) => 0
   56.72 +                            case (true, false) => - indent_extra
   56.73 +                            case (false, true) => indent_extra
   56.74 +                          }
   56.75 +                        line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
   56.76 +                      case Some(prev_tok) =>
   56.77 +                        indent_structure + indent_brackets + indent_size - indent_offset(tok) -
   56.78 +                        indent_offset(prev_tok) - indent_indent(prev_tok)
   56.79 +                    }
   56.80 +                 }
   56.81 +              }
   56.82              }
   56.83 +            else line_indent(current_line)
   56.84  
   56.85            actions.clear()
   56.86            actions.add(new IndentAction.AlignOffset(indent max 0))