merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
--- a/.hgtags Sun Aug 10 14:31:06 2014 +0200
+++ b/.hgtags Sun Aug 10 14:34:43 2014 +0200
@@ -29,3 +29,6 @@
9c1f2136532626c7cb5fae14a2aeac53be3aeb67 Isabelle2013-1
4dd08fe126bad63aa05741d55fb3e86a2dbfc795 Isabelle2013-2
251ef0202e719c824fe302d80a136dec025cf142 Isabelle2014-RC0
+c0fd03d13d28954f6b7018f273b6edb17fcdeaf7 Isabelle2014-RC1
+ee908fccabc220a5f2e5af533d13ebceeb0e09ff Isabelle2014-RC2
+91e188508bc9df5de2737325c390836603a3e409 Isabelle2014-RC3
--- a/Admin/Release/CHECKLIST Sun Aug 10 14:31:06 2014 +0200
+++ b/Admin/Release/CHECKLIST Sun Aug 10 14:34:43 2014 +0200
@@ -15,8 +15,6 @@
- test "#!/usr/bin/env isabelle_scala_script";
-- check HTML header of library;
-
- check sources:
isabelle java isabelle.Check_Source '~~' '$AFP_BASE'
@@ -40,6 +38,8 @@
ROOTS
lib/html/library_index_content.template
+- check HTML header of library;
+
- test separate compilation of Isabelle/Scala PIDE sources:
Admin/build jars_test
@@ -54,6 +54,8 @@
- Mac OS X: check app bundle with Retina display;
+- Windows: check dpi scaling with high-definition display;
+
Repository fork
===============
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/WinRun4J/manifest.xml Sun Aug 10 14:34:43 2014 +0200
@@ -0,0 +1,9 @@
+<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
+<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0" xmlns:asmv3="urn:schemas-microsoft-com:asm.v3" >
+ <asmv3:application>
+ <asmv3:windowsSettings xmlns="http://schemas.microsoft.com/SMI/2005/WindowsSettings">
+ <dpiAware>true</dpiAware>
+ </asmv3:windowsSettings>
+ </asmv3:application>
+</assembly>
+
--- a/Admin/components/components.sha1 Sun Aug 10 14:31:06 2014 +0200
+++ b/Admin/components/components.sha1 Sun Aug 10 14:34:43 2014 +0200
@@ -19,6 +19,7 @@
e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz
ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz
+23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
--- a/Admin/components/main Sun Aug 10 14:31:06 2014 +0200
+++ b/Admin/components/main Sun Aug 10 14:34:43 2014 +0200
@@ -2,7 +2,7 @@
cvc3-2.4.1
e-1.8
exec_process-1.0.3
-Haskabelle-2013
+Haskabelle-2014
jdk-7u65
jedit_build-20140722
jfreechart-1.0.14-1
--- a/Admin/lib/Tools/makedist_bundle Sun Aug 10 14:31:06 2014 +0200
+++ b/Admin/lib/Tools/makedist_bundle Sun Aug 10 14:34:43 2014 +0200
@@ -212,6 +212,7 @@
) > "$ISABELLE_TARGET/${ISABELLE_NAME}.ini"
cp "$TMP/windows_app/Isabelle.exe" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe"
+ cp "$ISABELLE_HOME/Admin/Windows/WinRun4J/manifest.xml" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe.manifest"
cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
"$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET"
--- a/Admin/user-aliases Sun Aug 10 14:31:06 2014 +0200
+++ b/Admin/user-aliases Sun Aug 10 14:34:43 2014 +0200
@@ -12,6 +12,7 @@
kaliszyk@in.tum.de kaliszyk
Philipp\ Meyer meyerp
noschinl@in.tum.de noschinl
+Lars Noschinski\ <noschinl@in.tum.de> noschinl
brianh@cs.pdx.edu huffman
nik sultana
griff Christian Sternagel
--- a/CONTRIBUTORS Sun Aug 10 14:31:06 2014 +0200
+++ b/CONTRIBUTORS Sun Aug 10 14:34:43 2014 +0200
@@ -19,13 +19,13 @@
semigroups and monoids, particularly products (resp. sums) on
finite sets.
-* June 2014: Florian Haftmann, TUM
- Internal reorganisation of the local theory / named target stack.
-
* Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
Work on exotic automatic theorem provers for Sledgehammer (LEO-II,
veriT, Waldmeister, etc.).
+* June 2014: Florian Haftmann, TUM
+ Internal reorganisation of the local theory / named target stack.
+
* June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM
Various properties of exponentially, Erlang, and normal distributed
random variables.
@@ -44,6 +44,9 @@
* Spring 2014: Lawrence C Paulson, Cambridge
Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory
+* Winter 2013 and Spring 2014: Ondrej Kuncar, TUM
+ Various improvements to Lifting/Transfer, integration with the BNF package.
+
* Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
--- a/NEWS Sun Aug 10 14:31:06 2014 +0200
+++ b/NEWS Sun Aug 10 14:34:43 2014 +0200
@@ -97,6 +97,9 @@
handling and propagation to enclosing text area -- avoid loosing
keystrokes with slow / remote graphics displays.
+* Completion popup supports both ENTER and TAB (default) to select an
+item, depending on Isabelle options.
+
* Refined insertion of completion items wrt. jEdit text: multiple
selections, rectangular selections, rectangular selection as "tall
caret".
@@ -120,6 +123,11 @@
* More support for remote files (e.g. http) using standard Java
networking operations instead of jEdit virtual file-systems.
+* Empty editors buffers that are no longer required (e.g.\ via theory
+imports) are automatically removed from the document model.
+
+* Improved monitor panel.
+
* Improved Console/Scala plugin: more uniform scala.Console output,
more robust treatment of threads and interrupts.
@@ -357,6 +365,42 @@
INCOMPATIBILITY.
+* Lifting and Transfer:
+ - a type variable as a raw type is supported
+ - stronger reflexivity prover
+ - rep_eq is always generated by lift_definition
+ - setup for Lifting/Transfer is now automated for BNFs
+ + holds for BNFs that do not contain a dead variable
+ + relator_eq, relator_mono, relator_distr, relator_domain,
+ relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
+ right_unique, right_total, left_unique, left_total are proved
+ automatically
+ + definition of a predicator is generated automatically
+ + simplification rules for a predicator definition are proved
+ automatically for datatypes
+ - consolidation of the setup of Lifting/Transfer
+ + property that a relator preservers reflexivity is not needed any
+ more
+ Minor INCOMPATIBILITY.
+ + left_total and left_unique rules are now transfer rules
+ (reflexivity_rule attribute not needed anymore)
+ INCOMPATIBILITY.
+ + Domainp does not have to be a separate assumption in
+ relator_domain theorems (=> more natural statement)
+ INCOMPATIBILITY.
+ - registration of code equations is more robust
+ Potential INCOMPATIBILITY.
+ - respectfulness proof obligation is preprocessed to a more readable
+ form
+ Potential INCOMPATIBILITY.
+ - eq_onp is always unfolded in respectfulness proof obligation
+ Potential INCOMPATIBILITY.
+ - unregister lifting setup for Code_Numeral.integer and
+ Code_Numeral.natural
+ Potential INCOMPATIBILITY.
+ - Lifting.invariant -> eq_onp
+ INCOMPATIBILITY.
+
* New internal SAT solver "cdclite" that produces models and proof
traces. This solver replaces the internal SAT solvers "enumerate" and
"dpll". Applications that explicitly used one of these two SAT
@@ -776,6 +820,9 @@
* HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it
is subsumed by session Kleene_Algebra in AFP.
+* HOL-Library / theory RBT: various constants and facts are hidden;
+lifting setup is unregistered. INCOMPATIBILITY.
+
* HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
* HOL-Word: bit representations prefer type bool over type bit.
@@ -868,6 +915,13 @@
bounded_linear_imp_linear ~> bounded_linear.linear
* HOL-Probability:
+ - Renamed positive_integral to nn_integral:
+
+ . Renamed all lemmas "*positive_integral*" to *nn_integral*"
+ positive_integral_positive ~> nn_integral_nonneg
+
+ . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
+
- replaced the Lebesgue integral on real numbers by the more general
Bochner integral for functions into a real-normed vector space.
@@ -882,14 +936,14 @@
integrable_nonneg ~> integrableI_nonneg
integral_positive ~> integral_nonneg_AE
integrable_abs_iff ~> integrable_abs_cancel
- positive_integral_lim_INF ~> positive_integral_liminf
+ positive_integral_lim_INF ~> nn_integral_liminf
lebesgue_real_affine ~> lborel_real_affine
borel_integral_has_integral ~> has_integral_lebesgue_integral
integral_indicator ~>
integral_real_indicator / integrable_real_indicator
- positive_integral_fst ~> positive_integral_fst'
- positive_integral_fst_measurable ~> positive_integral_fst
- positive_integral_snd_measurable ~> positive_integral_snd
+ positive_integral_fst ~> nn_integral_fst'
+ positive_integral_fst_measurable ~> nn_integral_fst
+ positive_integral_snd_measurable ~> nn_integral_snd
integrable_fst_measurable ~>
integral_fst / integrable_fst / AE_integrable_fst
@@ -915,7 +969,7 @@
integrable_has_integral_lebesgue_nonneg
lebesgue_integral_real_affine ~>
- positive_integral_real_affine
+ nn_integral_real_affine
has_integral_iff_positive_integral_lborel ~>
integral_has_integral_nonneg / integrable_has_integral_nonneg
@@ -930,13 +984,6 @@
integral_cmul_indicator
integral_real
- - Renamed positive_integral to nn_integral:
-
- . Renamed all lemmas "*positive_integral*" to *nn_integral*"
- positive_integral_positive ~> nn_integral_nonneg
-
- . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
-
- Formalized properties about exponentially, Erlang, and normal
distributed random variables.
--- a/etc/options Sun Aug 10 14:31:06 2014 +0200
+++ b/etc/options Sun Aug 10 14:34:43 2014 +0200
@@ -117,6 +117,9 @@
public option editor_output_delay : real = 0.1
-- "delay for prover output (markup, common messages etc.)"
+public option editor_prune_delay : real = 60.0
+ -- "delay to prune history (delete old versions)"
+
public option editor_update_delay : real = 0.5
-- "delay for physical GUI updates"
--- a/src/Doc/Implementation/ML.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Doc/Implementation/ML.thy Sun Aug 10 14:34:43 2014 +0200
@@ -722,9 +722,10 @@
\begin{description}
- \item @{text "@{make_string}"} inlines a function to print arbitrary
- values similar to the ML toplevel. The result is compiler dependent
- and may fall back on "?" in certain situations.
+ \item @{text "@{make_string}"} inlines a function to print arbitrary values
+ similar to the ML toplevel. The result is compiler dependent and may fall
+ back on "?" in certain situations. The value of configuration option
+ @{attribute_ref ML_print_depth} determines further details of output.
\item @{text "@{print f}"} uses the ML function @{text "f: string ->
unit"} to output the result of @{text "@{make_string}"} above,
--- a/src/Doc/Implementation/Syntax.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Doc/Implementation/Syntax.thy Sun Aug 10 14:34:43 2014 +0200
@@ -99,7 +99,7 @@
If particular type-constraints are required for some of the arguments, the
read operations needs to be split into its parse and check phases. Then it
is possible to use @{ML Type.constraint} on the intermediate pre-terms
- \secref{sec:term-check}.
+ (\secref{sec:term-check}).
\item @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a
simultaneous list of source strings as terms of the logic, with an implicit
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sun Aug 10 14:34:43 2014 +0200
@@ -1542,6 +1542,10 @@
@{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
@{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)"}
+ Preservation of predicates on relations (@{text "bi_unique, bi_total,
+ right_unique, right_total, left_unique, left_total"}) with the respect to a relator
+ is proved automatically if the involved type is BNF\cite{isabelle-datatypes} without dead variables.
+
\item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
of rules, which specify a domain of a transfer relation by a predicate.
E.g., given the transfer relation @{text "ZN x n \<equiv> (x = int n)"},
@@ -1550,15 +1554,19 @@
more readable transferred goals, e.g., when quantifiers are transferred.
\item @{attribute (HOL) relator_eq} attribute collects identity laws
- for relators of various type constructors, e.g. @{text "list_all2
+ for relators of various type constructors, e.g. @{term "rel_set
(op =) = (op =)"}. The @{method (HOL) transfer} method uses these
lemmas to infer transfer rules for non-polymorphic constants on
- the fly.
+ the fly. For examples see @{file
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute_def (HOL) "relator_domain"} attribute collects rules
- describing domains of relators by predicators. E.g., @{text "Domainp A = P \<Longrightarrow>
- Domainp (list_all2 A) = (list_all P)"}. This allows the package to lift transfer
- domain rules through type constructors.
+ describing domains of relators by predicators. E.g.,
+ @{term "Domainp (rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package
+ to lift transfer domain rules through type constructors. For examples see @{file
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\end{description}
@@ -1603,7 +1611,7 @@
@{rail \<open>
@@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \<newline>
- 'is' @{syntax term} (@'parametric' @{syntax thmref})?;
+ 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?;
\<close>}
@{rail \<open>
@@ -1625,10 +1633,10 @@
The command supports two modes. The first one is a low-level mode when
the user must provide as a first
argument of @{command (HOL) "setup_lifting"} a
- quotient theorem @{text "Quotient R Abs Rep T"}. The
+ quotient theorem @{term "Quotient R Abs Rep T"}. The
package configures a transfer rule for equality, a domain transfer
rules and sets up the @{command_def (HOL) "lift_definition"}
- command to work with the abstract type. An optional theorem @{text "reflp R"}, which certifies that
+ command to work with the abstract type. An optional theorem @{term "reflp R"}, which certifies that
the equivalence relation R is total,
can be provided as a second argument. This allows the package to generate stronger transfer
rules. And finally, the parametricity theorem for R can be provided as a third argument.
@@ -1671,9 +1679,9 @@
@{text f.transfer} for the Transfer package are generated by the
package.
- The user can specify a parametricity theorem for @{text t} after the keyword
+ The user can specify a parametricity theorems for @{text t} after the keyword
@{keyword "parametric"}, which allows the command
- to generate a parametric transfer rule for @{text f}.
+ to generate parametric transfer rules for @{text f}.
For each constant defined through trivial quotients (type copies or
subtypes) @{text f.rep_eq} is generated. The equation is a code certificate
@@ -1720,38 +1728,42 @@
theorems.
\item @{attribute (HOL) quot_map} registers a quotient map
- theorem. E.g., @{text "Quotient R Abs Rep T \<Longrightarrow>
- Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"}.
+ theorem, a theorem showing how to "lift" quotients over type constructors.
+ E.g., @{term "Quotient R Abs Rep T \<Longrightarrow>
+ Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)"}.
For examples see @{file
- "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
- in the same directory.
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute (HOL) relator_eq_onp} registers a theorem that
- shows a relationship between the constant @{text
- eq_onp} (used for internal encoding of proper subtypes)
- and a relator. Such theorems allows the package to hide @{text
+ shows that a relator applied to an equality restricted by a predicate @{term P} (i.e., @{term
+ "eq_onp P"}) is equal
+ to a predicator applied to the @{term P}. The combinator @{const eq_onp} is used for
+ internal encoding of proper subtypes. Such theorems allows the package to hide @{text
eq_onp} from a user in a user-readable form of a
respectfulness theorem. For examples see @{file
- "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.
- E.g., @{text "A \<le> B \<Longrightarrow> list_all2 A \<le> list_all2 B"}. For examples
- see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
- or Lifting_*.thy files in the same directory.
+ E.g., @{term "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
- when a parametricity theorem for the raw term is specified.
+ when a parametricity theorem for the raw term is specified and also for the reflexivity prover.
+ For examples see @{file
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute (HOL) "relator_distr"} registers a property describing a distributivity
of the relation composition and a relator. E.g.,
- @{text "list_all2 R \<circ>\<circ> list_all2 S = list_all2 (R \<circ>\<circ> S)"}.
+ @{text "rel_set R \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> S)"}.
This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
when a parametricity theorem for the raw term is specified.
When this equality does not hold unconditionally (e.g., for the function type), the user can specified
each direction separately and also register multiple theorems with different set of assumptions.
This attribute can be used only after the monotonicity property was already registered by
- @{attribute (HOL) "relator_mono"}. For examples
- see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
- or Lifting_*.thy files in the same directory.
+ @{attribute (HOL) "relator_mono"}. For examples see @{file
+ "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
+ This property is proved automatically if the involved type is BNF without dead variables.
\item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
from the Lifting infrastructure and thus de-register the corresponding quotient.
@@ -1773,6 +1785,14 @@
together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is
preferred for normal usage.
+ \item Integration with the BNF package\cite{isabelle-datatypes}:
+ As already mentioned, the theorems that are registered
+ by the following attributes are proved and registered automatically if the involved type
+ is BNF without dead variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},
+ @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also the definition of a
+ relator and predicator is provided automatically. Moreover, if the BNF represents a datatype,
+ simplification rules for a predicator are again proved automatically.
+
\end{description}
*}
--- a/src/Doc/JEdit/JEdit.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy Sun Aug 10 14:34:43 2014 +0200
@@ -1298,20 +1298,21 @@
A \emph{completion popup} is a minimally invasive GUI component over the
text area that offers a selection of completion items to be inserted into
the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to
- the frequency of selection, with persistent history. The popup interprets
- special keys @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim
- DOWN}, @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}, but all other key events
- are passed to the underlying text area. This allows to ignore unwanted
- completions most of the time and continue typing quickly. Thus the popup
- serves as a mechanism of confirmation of proposed items, but the default is
- to continue without completion.
+ the frequency of selection, with persistent history. The popup may interpret
+ special keys @{verbatim ENTER}, @{verbatim TAB}, @{verbatim ESCAPE},
+ @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP}, @{verbatim
+ PAGE_DOWN}, but all other key events are passed to the underlying text area.
+ This allows to ignore unwanted completions most of the time and continue
+ typing quickly. Thus the popup serves as a mechanism of confirmation of
+ proposed items, but the default is to continue without completion.
The meaning of special keys is as follows:
\medskip
\begin{tabular}{ll}
\textbf{key} & \textbf{action} \\\hline
- @{verbatim "TAB"} & select completion \\
+ @{verbatim "ENTER"} & select completion (if @{system_option jedit_completion_select_enter}) \\
+ @{verbatim "TAB"} & select completion (if @{system_option jedit_completion_select_tab}) \\
@{verbatim "ESCAPE"} & dismiss popup \\
@{verbatim "UP"} & move up one item \\
@{verbatim "DOWN"} & move down one item \\
@@ -1385,6 +1386,11 @@
regular jEdit key events (\secref{sec:completion-input}): it allows to
disable implicit completion altogether.
+ \item @{system_option_def jedit_completion_select_enter} and
+ @{system_option_def jedit_completion_select_tab} enable keys to select a
+ completion item from the popup (\secref{sec:completion-popup}). Note that a
+ regular mouse click on the list of items is always possible.
+
\item @{system_option_def jedit_completion_context} specifies whether the
language context provided by the prover should be used at all. Disabling
that option makes completion less ``semantic''. Note that incomplete or
@@ -1589,14 +1595,14 @@
@{system_option_ref jedit_timing_threshold}, which can be configured in
\emph{Plugin Options~/ Isabelle~/ General}.
- \medskip The \emph{Monitor} panel provides a general impression of
- recent activity of the farm of worker threads in Isabelle/ML. Its
- display is continuously updated according to @{system_option_ref
- editor_chart_delay}. Note that the painting of the chart takes
- considerable runtime itself --- on the Java Virtual Machine that
- runs Isabelle/Scala, not Isabelle/ML. Internally, the
- Isabelle/Scala module @{verbatim isabelle.ML_Statistics} provides
- further access to statistics of Isabelle/ML. *}
+ \medskip The \emph{Monitor} panel visualizes various data collections about
+ recent activity of the Isabelle/ML task farm and the underlying ML runtime
+ system. The display is continuously updated according to @{system_option_ref
+ editor_chart_delay}. Note that the painting of the chart takes considerable
+ runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not
+ Isabelle/ML. Internally, the Isabelle/Scala module @{verbatim
+ isabelle.ML_Statistics} provides further access to statistics of
+ Isabelle/ML. *}
section {* Low-level output *}
@@ -1662,11 +1668,11 @@
\textbf{Workaround:} Copy/paste complete command text from
elsewhere, or disable continuous checking temporarily.
- \item \textbf{Problem:} No way to delete document nodes from the overall
+ \item \textbf{Problem:} No direct support to remove document nodes from the
collection of theories.
- \textbf{Workaround:} Ignore unused files. Restart whole
- Isabelle/jEdit session in worst-case situation.
+ \textbf{Workaround:} Clear the buffer content of unused files and close
+ \emph{without} saving changes.
\item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
@{verbatim "C+MINUS"} for adjusting the editor font size depend on
--- a/src/Doc/Prog_Prove/document/root.bib Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Doc/Prog_Prove/document/root.bib Sun Aug 10 14:34:43 2014 +0200
@@ -18,7 +18,7 @@
@book{ConcreteSemantics,author={Tobias Nipkow and Gerwin Klein},
title="Concrete Semantics. A Proof Assistant Approach",
-publisher={\url{http://www.in.tum.de/~nipkow/Concrete}},year=2013}
+publisher={\url{http://www.concrete-semantics.org}},year=2013}
@manual{IsarRef,author={Makarius Wenzel},
title={The Isabelle/Isar Reference Manual},
--- a/src/Doc/System/Scala.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Doc/System/Scala.thy Sun Aug 10 14:34:43 2014 +0200
@@ -61,7 +61,7 @@
This allows to compile further Scala modules, depending on existing
Isabelle/Scala functionality. The resulting class or jar files can
- be added to the Java classpath the @{verbatim classpath} Bash
+ be added to the Java classpath using the @{verbatim classpath} Bash
function that is provided by the Isabelle process environment. Thus
add-on components can register themselves in a modular manner, see
also \secref{sec:components}.
--- a/src/Doc/manual.bib Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Doc/manual.bib Sun Aug 10 14:34:43 2014 +0200
@@ -351,6 +351,12 @@
pages = "93--110"
}
+@manual{isabelle-datatypes,
+ author = {Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
+ title = {Defining (Co)datatypes in Isabelle/HOL},
+ institution = {TU Munich},
+ note = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}}
+
@inproceedings{why3,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {{Why3}: Shepherd Your Herd of Provers},
--- a/src/HOL/Algebra/Divisibility.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Sun Aug 10 14:34:43 2014 +0200
@@ -74,7 +74,7 @@
have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)
- also have "\<dots> = \<one>" by (simp add: Units_l_inv)
+ also have "\<dots> = \<one>" by simp
finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
@@ -83,7 +83,7 @@
by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
by (simp add: m_assoc del: Units_l_inv)
- also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv)
+ also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
@@ -327,7 +327,7 @@
unfolding a
apply (intro associatedI)
apply (rule dividesI[of "inv u"], simp)
- apply (simp add: m_assoc Units_closed Units_r_inv)
+ apply (simp add: m_assoc Units_closed)
apply fast
done
@@ -1764,7 +1764,7 @@
note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
have "a = a \<otimes> \<one>" by simp
- also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: Units_r_inv uunit)
+ also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: uunit)
also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
finally
have a: "a = a' \<otimes> inv u" .
@@ -2646,7 +2646,7 @@
hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
from ya yb csmset
- have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count)
+ have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def)
thus "y divides c" by (rule fmsubset_divides) fact+
qed
@@ -3208,7 +3208,7 @@
and nyx: "\<not> y \<sim> x"
by - (fast elim: properfactorE2)+
hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"
- by (fast elim: dividesE)
+ by fast
from this obtain z
where zcarr: "z \<in> carrier G"
@@ -3327,7 +3327,7 @@
and afs': "wfactors G as' a"
hence ahdvda: "ah divides a"
by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
- hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
+ hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast
from this obtain a'
where a'carr: "a' \<in> carrier G"
and a: "a = ah \<otimes> a'"
@@ -3360,7 +3360,7 @@
have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
note carr = carr asicarr
- from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
+ from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by fast
from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
with carr irrasi[simplified asi]
@@ -3454,7 +3454,7 @@
next
show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
apply (simp add: list_all2_append)
- apply (simp add: asiah[symmetric] ahcarr asicarr)
+ apply (simp add: asiah[symmetric])
done
qed
@@ -3463,12 +3463,12 @@
also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
(take i as' @ as' ! i # drop (Suc i) as')"
apply (intro essentially_equalI)
- apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
+ apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
take i as' @ as' ! i # drop (Suc i) as'")
- apply simp
+ apply simp
apply (rule perm_append_Cons)
apply simp
- done
+ done
finally
have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp
then show "essentially_equal G (ah # as) as'" by (subst as', assumption)
@@ -3617,7 +3617,7 @@
also from ccarr acarr cunit
have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
also from ccarr cunit
- have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
+ have "\<dots> = a \<otimes> \<one>" by simp
also from acarr
have "\<dots> = a" by simp
finally have "a = b \<otimes> inv c" by simp
@@ -3706,7 +3706,7 @@
shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"
apply rule
proof clarify
- assume dcc: "divisor_chain_condition_monoid G"
+ assume dcc: "divisor_chain_condition_monoid G"
and gc: "gcd_condition_monoid G"
interpret divisor_chain_condition_monoid "G" by (rule dcc)
interpret gcd_condition_monoid "G" by (rule gc)
--- a/src/HOL/Algebra/Exponent.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Algebra/Exponent.thy Sun Aug 10 14:34:43 2014 +0200
@@ -249,7 +249,7 @@
apply (simp (no_asm))
(*induction step*)
apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
- prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
+ prefer 2 apply (simp, clarify)
apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
exponent p (Suc k)")
txt{*First, use the assumed equation. We simplify the LHS to
@@ -260,7 +260,7 @@
@{text Suc_times_binomial_eq} ...*}
apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
txt{*...then @{text exponent_mult_add} and the quantified premise.*}
-apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
+apply (simp del: bad_Sucs add: exponent_mult_add)
done
(*The lemma above, with two changes of variables*)
--- a/src/HOL/Algebra/UnivPoly.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Sun Aug 10 14:34:43 2014 +0200
@@ -528,7 +528,7 @@
case 0 with R show ?thesis by simp
next
case Suc with R show ?thesis
- using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def)
+ using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def)
qed
qed (simp_all add: R)
--- a/src/HOL/Library/AList_Mapping.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Library/AList_Mapping.thy Sun Aug 10 14:34:43 2014 +0200
@@ -60,7 +60,7 @@
have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
by (auto simp add: image_def intro!: bexI)
show ?thesis apply transfer
- by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
+ by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
qed
lemma [code nbe]:
--- a/src/HOL/Library/Diagonal_Subsequence.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Library/Diagonal_Subsequence.thy Sun Aug 10 14:34:43 2014 +0200
@@ -27,8 +27,10 @@
lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
proof (induct n)
- case (Suc n) thus ?case by (subst seqseq.simps) (auto simp: subseq_reduce intro!: subseq_o)
-qed (simp add: subseq_def)
+ case 0 thus ?case by (simp add: subseq_def)
+next
+ case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
+qed
lemma seqseq_holds:
"P n (seqseq (Suc n))"
--- a/src/HOL/Library/Float.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Library/Float.thy Sun Aug 10 14:34:43 2014 +0200
@@ -610,8 +610,7 @@
by (auto intro: exI[where x="m*2^nat (e+p)"]
simp add: ac_simps powr_add[symmetric] r powr_realpow)
with `\<not> p + e < 0` show ?thesis
- by transfer
- (auto simp add: round_down_def field_simps powr_add powr_minus inverse_eq_divide)
+ by transfer (auto simp add: round_down_def field_simps powr_add powr_minus)
qed
hide_fact (open) compute_float_down
@@ -682,8 +681,7 @@
by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
intro: exI[where x="m*2^nat (e+p)"])
then show ?thesis using `\<not> p + e < 0`
- by transfer
- (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
+ by transfer (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus)
qed
hide_fact (open) compute_float_up
@@ -840,7 +838,7 @@
have "(1::int) < 2" by simp
case False let ?S = "2^(nat (-e))"
have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"]
- by (auto simp: powr_minus field_simps inverse_eq_divide)
+ by (auto simp: powr_minus field_simps)
hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"]
by (auto simp: powr_minus)
hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
@@ -940,7 +938,7 @@
have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
moreover have "real x * real (2::int) powr real l / real y = x / real y'"
using `\<not> 0 \<le> l`
- by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide)
+ by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
ultimately show ?thesis
unfolding normfloat_def
using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
@@ -993,7 +991,7 @@
using rat_precision_pos[OF assms] by (rule power_aux)
finally show ?thesis
apply (transfer fixing: n x y)
- apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide powr1)
+ apply (simp add: round_up_def field_simps powr_minus powr1)
unfolding int_of_reals real_of_int_less_iff
apply (simp add: ceiling_less_eq)
done
@@ -1415,7 +1413,7 @@
by (simp add: powr_divide2[symmetric] powr_add powr_minus inverse_eq_divide)
also have "\<dots> = 2 powr (log 2 x - (real \<lfloor>log 2 x\<rfloor>) - 1)"
using `0 < x`
- by (auto simp: inverse_eq_divide field_simps powr_add powr_divide2[symmetric])
+ by (auto simp: field_simps powr_add powr_divide2[symmetric])
also have "\<dots> < 2 powr 0"
using real_of_int_floor_add_one_gt
unfolding neg_less_iff_less
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sun Aug 10 14:34:43 2014 +0200
@@ -808,7 +808,7 @@
then have tw: "cmod ?w \<le> cmod w"
using t(1) by (simp add: norm_mult)
from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
- by (simp add: inverse_eq_divide field_simps)
+ by (simp add: field_simps)
with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
by (metis comm_mult_strict_left_mono)
have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
--- a/src/HOL/Library/Lattice_Algebras.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy Sun Aug 10 14:34:43 2014 +0200
@@ -396,7 +396,7 @@
proof -
have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
(is "_=sup ?m ?n")
- by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
+ by (simp add: abs_lattice add_sup_inf_distribs ac_simps)
have a: "a + b \<le> sup ?m ?n"
by simp
have b: "- a - b \<le> ?n"
@@ -410,7 +410,7 @@
from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
apply -
apply (drule abs_leI)
- apply (simp_all only: algebra_simps ac_simps minus_add)
+ apply (simp_all only: algebra_simps minus_add)
apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
done
with g[symmetric] show ?thesis by simp
--- a/src/HOL/Library/Polynomial.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Library/Polynomial.thy Sun Aug 10 14:34:43 2014 +0200
@@ -1315,8 +1315,7 @@
then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
then have "finite (insert a {x. poly k x = 0})" by simp
then show "finite {x. poly p x = 0}"
- by (simp add: k uminus_add_conv_diff Collect_disj_eq
- del: mult_pCons_left)
+ by (simp add: k Collect_disj_eq del: mult_pCons_left)
qed
qed
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Aug 10 14:34:43 2014 +0200
@@ -137,17 +137,17 @@
end
*} "lift trivial vector statements to real arith statements"
-lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
-lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)
+lemma vec_0[simp]: "vec 0 = 0" by vector
+lemma vec_1[simp]: "vec 1 = 1" by vector
lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
-lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def)
-lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
-lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
-lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
+lemma vec_add: "vec(x + y) = vec x + vec y" by vector
+lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
+lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
+lemma vec_neg: "vec(- x) = - vec x " by vector
lemma vec_setsum:
assumes "finite S"
@@ -164,7 +164,7 @@
text{* Obvious "component-pushing". *}
lemma vec_component [simp]: "vec x $ i = x"
- by (vector vec_def)
+ by vector
lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
by vector
@@ -330,7 +330,7 @@
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) * e"
using setsum_norm_allsubsets_bound[OF assms]
- by (simp add: DIM_cart Basis_real_def)
+ by simp
subsection {* Matrix operations *}
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Aug 10 14:34:43 2014 +0200
@@ -1502,7 +1502,7 @@
by (intro convex_linear_vimage convex_translation convex_convex_hull,
simp add: linear_iff)
also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
- by (auto simp add: uminus_add_conv_diff image_def Bex_def)
+ by (auto simp add: image_def Bex_def)
finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
next
show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
@@ -1512,7 +1512,7 @@
by (intro convex_linear_vimage convex_translation convex_convex_hull,
simp add: linear_iff)
also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
- by (auto simp add: uminus_add_conv_diff image_def Bex_def)
+ by (auto simp add: image_def Bex_def)
finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
qed
qed
@@ -5504,12 +5504,12 @@
using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
OF convex_affinity compact_affinity]
using assms(1,2)
- by (auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
+ by (auto simp add: scaleR_right_diff_distrib)
then show ?thesis
apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
using `d>0` `e>0`
- apply (auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib)
+ apply (auto simp add: scaleR_right_diff_distrib)
done
qed
@@ -5808,7 +5808,7 @@
apply (rule_tac f="\<lambda>x. a + x" in arg_cong)
apply (rule setsum.cong [OF refl])
apply clarsimp
- apply (fast intro: set_plus_intro)
+ apply fast
done
lemma box_eq_set_setsum_Basis:
@@ -5895,7 +5895,7 @@
apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
using as
apply (subst euclidean_eq_iff)
- apply (auto simp: inner_setsum_left_Basis)
+ apply auto
done
qed auto
@@ -6430,7 +6430,7 @@
apply (subst (asm) euclidean_eq_iff)
using i
apply (erule_tac x=i in ballE)
- apply (auto simp add:field_simps inner_simps)
+ apply (auto simp add: field_simps inner_simps)
done
finally show "x \<bullet> i =
((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \<bullet> i"
@@ -8138,8 +8138,7 @@
and "convex S"
and "rel_open S"
shows "convex (f ` S) \<and> rel_open (f ` S)"
- by (metis assms convex_linear_image rel_interior_convex_linear_image
- linear_conv_bounded_linear rel_open_def)
+ by (metis assms convex_linear_image rel_interior_convex_linear_image rel_open_def)
lemma convex_rel_open_linear_preimage:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sun Aug 10 14:34:43 2014 +0200
@@ -69,7 +69,7 @@
lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
unfolding has_derivative_def Lim
- by (auto simp add: netlimit_within inverse_eq_divide field_simps)
+ by (auto simp add: netlimit_within field_simps)
lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
@@ -1773,9 +1773,9 @@
apply (rule lem3[rule_format])+
done
obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
- using assms(3) `x \<in> s` by (fast intro: zero_less_one order_refl)
+ using assms(3) `x \<in> s` by (fast intro: zero_less_one)
have "bounded_linear (f' N x)"
- using assms(2) `x \<in> s` by (fast dest: has_derivative_bounded_linear)
+ using assms(2) `x \<in> s` by fast
from bounded_linear.bounded [OF this]
obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
{
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sun Aug 10 14:34:43 2014 +0200
@@ -1125,7 +1125,7 @@
note fin = this
have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
using f
- by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
+ by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
also have "\<dots> = ereal r"
using fin r by (auto simp: ereal_real)
finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
@@ -1252,7 +1252,8 @@
apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
apply (drule sym)
apply auto
- by (metis INF_absorb centre_in_ball)
+ apply (metis INF_absorb centre_in_ball)
+ done
lemma suminf_ereal_offset_le:
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Aug 10 14:34:43 2014 +0200
@@ -343,7 +343,7 @@
using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
then have "y\<bullet>k < a\<bullet>k"
using e[THEN conjunct1] k
- by (auto simp add: field_simps abs_less_iff as inner_Basis inner_simps)
+ by (auto simp add: field_simps abs_less_iff as inner_simps)
then have "y \<notin> i"
unfolding ab mem_box by (auto intro!: bexI[OF _ k])
then show False using yi by auto
@@ -12092,7 +12092,7 @@
by (induct I) (auto intro!: bounded_linear_add bounded_linear_zero)
next
case False
- then show ?thesis by (simp add: bounded_linear_zero)
+ then show ?thesis by simp
qed
lemma absolutely_integrable_vector_abs:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Aug 10 14:34:43 2014 +0200
@@ -7307,27 +7307,27 @@
lemma real_affinity_le:
"0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_le_affinity:
"0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_affinity_lt:
"0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_lt_affinity:
"0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_affinity_eq:
"(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
lemma real_eq_affinity:
"(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
- by (simp add: field_simps inverse_eq_divide)
+ by (simp add: field_simps)
subsection {* Banach fixed point theorem (not really topological...) *}
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Aug 10 14:34:43 2014 +0200
@@ -1336,7 +1336,14 @@
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
- val sel_default_eqs = map (prepare_term lthy) raw_sel_default_eqs;
+ val sel_Tss = map (map (curry (op -->) fpT)) ctr_Tss;
+ val sel_bTs =
+ flat sel_bindingss ~~ flat sel_Tss
+ |> filter_out (Binding.is_empty o fst)
+ |> distinct (Binding.eq_name o pairself fst);
+ val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy;
+
+ val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
@@ -1570,7 +1577,8 @@
val thm = Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
- injects rel_inject_thms distincts rel_distinct_thms)
+ injects rel_inject_thms distincts rel_distinct_thms
+ (map rel_eq_of_bnf live_nesting_bnfs))
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Aug 10 14:34:43 2014 +0200
@@ -28,7 +28,7 @@
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
- thm list -> thm list -> tactic
+ thm list -> thm list -> thm list -> tactic
val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> tactic
@@ -217,11 +217,11 @@
(1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
selsss));
-fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts =
+fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
hyp_subst_tac ctxt) THEN
- unfold_thms_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
+ unfold_thms_tac ctxt (rel_eqs @ injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
True_implies_equals conj_imp_eq_imp_imp} @
map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
map (fn thm => thm RS eqTrueI) rel_injects) THEN
@@ -261,7 +261,7 @@
unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
@{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
TRYALL (hyp_subst_tac ctxt) THEN
- unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
+ unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
Inr_Inl_False sum.inject prod.inject}) THEN
TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
@@ -270,7 +270,7 @@
HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
hyp_subst_tac ctxt) THEN
- Local_Defs.unfold_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
+ unfold_thms_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
((discs @ distincts) RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
(rel_injects RL @{thms iffD2[OF eq_True]}) @
(rel_distincts RL @{thms iffD2[OF eq_False]})) THEN
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Aug 10 14:34:43 2014 +0200
@@ -62,6 +62,7 @@
val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c
val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
+ val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context
val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
(((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
ctr_sugar * local_theory
@@ -328,6 +329,12 @@
malformed ()
end;
+(* Ideally, we would enrich the context with constants rather than free variables. *)
+fun fake_local_theory_for_sel_defaults sel_bTs =
+ Proof_Context.allow_dummies
+ #> Proof_Context.add_fixes (map (fn (b, T) => (b, SOME T, NoSyn)) sel_bTs)
+ #> snd;
+
type ('c, 'a) ctr_spec = (binding * 'c) * 'a list;
fun disc_of_ctr_spec ((disc, _), _) = disc;
@@ -501,30 +508,35 @@
(true, [], [], [], [], [], lthy')
else
let
- val sel_bindings = flat sel_bindingss;
- val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
- val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
+ val all_sel_bindings = flat sel_bindingss;
+ val num_all_sel_bindings = length all_sel_bindings;
+ val uniq_sel_bindings = distinct Binding.eq_name all_sel_bindings;
+ val all_sels_distinct = (length uniq_sel_bindings = num_all_sel_bindings);
val sel_binding_index =
- if all_sels_distinct then 1 upto length sel_bindings
- else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
+ if all_sels_distinct then
+ 1 upto num_all_sel_bindings
+ else
+ map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings;
- val all_proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
+ val all_proto_sels = flat (map3 (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
val sel_infos =
AList.group (op =) (sel_binding_index ~~ all_proto_sels)
|> sort (int_ord o pairself fst)
|> map snd |> curry (op ~~) uniq_sel_bindings;
val sel_bindings = map fst sel_infos;
- val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos;
-
- val sel_default_lthy = no_defs_lthy
- |> Proof_Context.allow_dummies
- |> Proof_Context.add_fixes
- (map2 (fn b => fn T => (b, SOME T, NoSyn)) sel_bindings sel_Ts)
- |> snd;
val sel_defaults =
- map (extract_sel_default sel_default_lthy o prep_term sel_default_lthy) sel_default_eqs;
+ if null sel_default_eqs then
+ []
+ else
+ let
+ val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos;
+ val fake_lthy =
+ fake_local_theory_for_sel_defaults (sel_bindings ~~ sel_Ts) no_defs_lthy;
+ in
+ map (extract_sel_default fake_lthy o prep_term fake_lthy) sel_default_eqs
+ end;
fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 10 14:34:43 2014 +0200
@@ -119,11 +119,13 @@
end
fun thms_in_proof max_thms name_tabs th =
- let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
- SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names
- (Proofterm.strip_thm (Thm.proof_body_of th)))
- handle TOO_MANY () => NONE
- end
+ (case try Thm.proof_body_of th of
+ NONE => NONE
+ | SOME body =>
+ let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
+ SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
+ handle TOO_MANY () => NONE
+ end)
fun thms_of_name ctxt name =
let
--- a/src/HOL/Tools/inductive_set.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Tools/inductive_set.ML Sun Aug 10 14:34:43 2014 +0200
@@ -275,7 +275,9 @@
Sign.typ_instance thy (U, T'))
(Symtab.lookup_list set_arities s')
then
- (warning ("Ignoring conversion rule for operator " ^ s'); tab)
+ (if Context_Position.is_really_visible ctxt then
+ warning ("Ignoring conversion rule for operator " ^ s')
+ else (); tab)
else
{to_set_simps = thm :: to_set_simps,
to_pred_simps =
@@ -289,8 +291,14 @@
| _ => raise Malformed "equation between predicates expected")
| _ => raise Malformed "equation expected")
handle Malformed msg =>
- (warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
- "\n" ^ Display.string_of_thm (Context.proof_of context) thm); tab);
+ let
+ val ctxt = Context.proof_of context
+ val _ =
+ if Context_Position.is_really_visible ctxt then
+ warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
+ "\n" ^ Display.string_of_thm ctxt thm)
+ else ();
+ in tab end;
val pred_set_conv_att = Thm.declaration_attribute
(fn thm => fn ctxt => Data.map (add ctxt thm) ctxt);
--- a/src/Provers/classical.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Provers/classical.ML Sun Aug 10 14:34:43 2014 +0200
@@ -309,7 +309,7 @@
else Tactic.make_elim th;
fun warn_thm (SOME (Context.Proof ctxt)) msg th =
- if Context_Position.is_visible ctxt
+ if Context_Position.is_really_visible ctxt
then warning (msg ^ Display.string_of_thm ctxt th) else ()
| warn_thm _ _ _ = ();
--- a/src/Pure/GUI/gui.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/GUI/gui.scala Sun Aug 10 14:34:43 2014 +0200
@@ -12,7 +12,7 @@
import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow,
+import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
JButton, JTextField}
import scala.collection.convert.WrapAsJava
@@ -208,8 +208,9 @@
def layered_pane(component: Component): Option[JLayeredPane] =
parent_window(component) match {
- case Some(window: JWindow) => Some(window.getLayeredPane)
- case Some(frame: JFrame) => Some(frame.getLayeredPane)
+ case Some(w: JWindow) => Some(w.getLayeredPane)
+ case Some(w: JFrame) => Some(w.getLayeredPane)
+ case Some(w: JDialog) => Some(w.getLayeredPane)
case _ => None
}
--- a/src/Pure/General/exn.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/General/exn.scala Sun Aug 10 14:34:43 2014 +0200
@@ -82,7 +82,7 @@
}
else if (exn.getClass == runtime_exception) {
val msg = exn.getMessage
- Some(if (msg == null) "Error" else msg)
+ Some(if (msg == null || msg == "") "Error" else msg)
}
else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
else None
--- a/src/Pure/General/symbol.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/General/symbol.scala Sun Aug 10 14:34:43 2014 +0200
@@ -203,6 +203,8 @@
case _ => false
}
+ override def toString: String = "Text_Chunk" + range.toString
+
def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
def incorporate(symbol_range: Range): Option[Text.Range] =
--- a/src/Pure/Isar/attrib.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Aug 10 14:34:43 2014 +0200
@@ -292,7 +292,7 @@
in
fun partial_evaluation ctxt facts =
- (facts, Context.Proof ctxt) |->
+ (facts, Context.Proof (Context_Position.not_really ctxt)) |->
fold_map (fn ((b, more_atts), fact) => fn context =>
let
val (fact', (decls, context')) =
--- a/src/Pure/Isar/element.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Isar/element.ML Sun Aug 10 14:34:43 2014 +0200
@@ -51,6 +51,7 @@
val satisfy_morphism: witness list -> morphism
val eq_morphism: theory -> thm list -> morphism option
val init: context_i -> Context.generic -> Context.generic
+ val init': context_i -> Context.generic -> Context.generic
val activate_i: context_i -> Proof.context -> context_i * Proof.context
val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
end;
@@ -473,18 +474,16 @@
(* init *)
-local
-
-fun init0 (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
- | init0 (Constrains _) = I
- | init0 (Assumes asms) = Context.map_proof (fn ctxt =>
+fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
+ | init (Constrains _) = I
+ | init (Assumes asms) = Context.map_proof (fn ctxt =>
let
val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (maps (map #1 o #2) asms')
|> Proof_Context.add_assms_i Assumption.assume_export asms';
in ctxt' end)
- | init0 (Defines defs) = Context.map_proof (fn ctxt =>
+ | init (Defines defs) = Context.map_proof (fn ctxt =>
let
val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
val asms = defs' |> map (fn (b, (t, ps)) =>
@@ -494,17 +493,15 @@
|> fold Variable.auto_fixes (map #1 asms)
|> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
in ctxt' end)
- | init0 (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
+ | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
-in
-
-fun init elem context =
+fun init' elem context =
context
- |> Context.mapping I Thm.unchecked_hyps
- |> init0 elem
- |> Context.mapping I (fn ctxt => Thm.restore_hyps (Context.proof_of context) ctxt);
-
-end;
+ |> Context.mapping I (Thm.unchecked_hyps #> Context_Position.not_really)
+ |> init elem
+ |> Context.mapping I (fn ctxt =>
+ let val ctxt0 = Context.proof_of context
+ in ctxt |> Context_Position.restore_visible ctxt0 |> Thm.restore_hyps ctxt0 end);
(* activate *)
--- a/src/Pure/Isar/expression.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Isar/expression.ML Sun Aug 10 14:34:43 2014 +0200
@@ -865,8 +865,8 @@
(* generic interpretation machinery *)
-fun meta_rewrite eqns ctxt =
- (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
+fun meta_rewrite ctxt eqns =
+ map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
let
@@ -874,7 +874,7 @@
(attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
val (eqns', ctxt') = ctxt
|> note Thm.lemmaK facts
- |-> meta_rewrite;
+ |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
val dep_morphs =
map2 (fn (dep, morph) => fn wits =>
(dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))
--- a/src/Pure/Isar/keyword.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Isar/keyword.scala Sun Aug 10 14:34:43 2014 +0200
@@ -44,21 +44,31 @@
/* categories */
- val minor = Set(MINOR)
+ val diag = Set(DIAG)
val control = Set(CONTROL)
- val diag = Set(DIAG)
+
+ val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
+ PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
+
val theory =
Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
- THY_DECL, THY_GOAL)
- val theory1 = Set(THY_BEGIN, THY_END)
- val theory2 = Set(THY_DECL, THY_GOAL)
+ THY_LOAD, THY_DECL, THY_GOAL)
+
+ val theory_body =
+ Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL)
+
val proof =
Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
- PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
- PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
- val proof1 =
- Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
- PRF_CHAIN, PRF_DECL)
- val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
+ PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL,
+ PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+
+ val proof_body =
+ Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN,
+ PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+
+ val theory_goal = Set(THY_GOAL)
+ val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
+ val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
+ val qed_global = Set(QED_GLOBAL)
}
--- a/src/Pure/Isar/locale.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Isar/locale.ML Sun Aug 10 14:34:43 2014 +0200
@@ -448,7 +448,7 @@
let
val thy = Context.theory_of context;
val activate =
- activate_notes Element.init
+ activate_notes Element.init'
(Morphism.transfer_morphism o Context.theory_of) context export;
in
roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
@@ -460,7 +460,7 @@
val context = Context.Proof (Proof_Context.init_global thy);
val marked = Idents.get context;
val (marked', context') = (empty_idents, context)
- |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of);
+ |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of);
in
context'
|> Idents.put (merge_idents (marked, marked'))
--- a/src/Pure/Isar/method.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Isar/method.ML Sun Aug 10 14:34:43 2014 +0200
@@ -347,10 +347,11 @@
let val table = get_methods ctxt
in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
-fun method_closure ctxt src0 =
+fun method_closure ctxt0 src0 =
let
- val (src1, meth) = check_src ctxt src0;
+ val (src1, meth) = check_src ctxt0 src0;
val src2 = Args.init_assignable src1;
+ val ctxt = Context_Position.not_really ctxt0;
val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
in Args.closure src2 end;
--- a/src/Pure/Isar/runtime.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Isar/runtime.ML Sun Aug 10 14:34:43 2014 +0200
@@ -99,6 +99,7 @@
TERMINATE => "Exit"
| TimeLimit.TimeOut => "Timeout"
| TOPLEVEL_ERROR => "Error"
+ | ERROR "" => "Error"
| ERROR msg => msg
| Fail msg => raised exn "Fail" [msg]
| THEORY (msg, thys) =>
--- a/src/Pure/ML-Systems/polyml.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Sun Aug 10 14:34:43 2014 +0200
@@ -174,5 +174,5 @@
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
val ml_make_string =
- "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))";
+ "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth ())))))";
--- a/src/Pure/ML/ml_antiquotation.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Sun Aug 10 14:34:43 2014 +0200
@@ -19,7 +19,7 @@
(* unique names *)
-val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
+val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
structure Names = Proof_Data
(
--- a/src/Pure/ML/ml_context.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/ML/ml_context.ML Sun Aug 10 14:34:43 2014 +0200
@@ -93,7 +93,10 @@
ML_Lex.tokenize
("structure Isabelle =\nstruct\n\
\val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
- " (ML_Context.the_local_context ());\n");
+ " (ML_Context.the_local_context ());\n\
+ \val ML_print_depth =\n\
+ \ let val default = ML_Options.get_print_depth ()\n\
+ \ in fn () => ML_Options.get_print_depth_default default end;\n");
val end_env = ML_Lex.tokenize "end;";
val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
--- a/src/Pure/ML/ml_options.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/ML/ml_options.ML Sun Aug 10 14:34:43 2014 +0200
@@ -14,6 +14,7 @@
val print_depth_raw: Config.raw
val print_depth: int Config.T
val get_print_depth: unit -> int
+ val get_print_depth_default: int -> int
end;
structure ML_Options: ML_OPTIONS =
@@ -47,4 +48,9 @@
NONE => get_default_print_depth ()
| SOME context => Config.get_generic context print_depth);
+fun get_print_depth_default default =
+ (case Context.thread_data () of
+ NONE => default
+ | SOME context => Config.get_generic context print_depth);
+
end;
--- a/src/Pure/PIDE/command.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/PIDE/command.ML Sun Aug 10 14:34:43 2014 +0200
@@ -204,7 +204,7 @@
in
(case res of
NONE => st0
- | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st))
+ | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
end) ();
fun run int tr st =
@@ -382,7 +382,7 @@
print_function "Execution.print"
(fn {args, exec_id, ...} =>
if null args then
- SOME {delay = NONE, pri = 1, persistent = false, strict = true,
+ SOME {delay = NONE, pri = 1, persistent = false, strict = false,
print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
else NONE);
--- a/src/Pure/PIDE/command.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/PIDE/command.scala Sun Aug 10 14:34:43 2014 +0200
@@ -356,14 +356,14 @@
/* blobs */
- def blobs_changed(doc_blobs: Document.Blobs): Boolean =
- blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
-
def blobs_names: List[Document.Node.Name] =
for (Exn.Res((name, _)) <- blobs) yield name
- def blobs_digests: List[SHA1.Digest] =
- for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
+ def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
+ for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest)
+
+ def blobs_changed(doc_blobs: Document.Blobs): Boolean =
+ blobs.exists({ case Exn.Res((name, _)) => doc_blobs.changed(name) case _ => false })
/* source chunks */
--- a/src/Pure/PIDE/document.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/PIDE/document.ML Sun Aug 10 14:34:43 2014 +0200
@@ -48,7 +48,7 @@
{required: bool, (*required node*)
visible: Inttab.set, (*visible commands*)
visible_last: Document_ID.command option, (*last visible command*)
- overlays: (string * string list) list Inttab.table}; (*command id -> print function with args*)
+ overlays: (string * string list) list Inttab.table}; (*command id -> print functions with args*)
structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
--- a/src/Pure/PIDE/document.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/PIDE/document.scala Sun Aug 10 14:34:43 2014 +0200
@@ -58,10 +58,6 @@
final class Blobs private(blobs: Map[Node.Name, Blob])
{
- private lazy val digests: Map[SHA1.Digest, Blob] =
- for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
-
- def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
def get(name: Node.Name): Option[Blob] = blobs.get(name)
def changed(name: Node.Name): Boolean =
@@ -648,7 +644,7 @@
(_, node) <- version.nodes.iterator
command <- node.commands.iterator
} {
- for (digest <- command.blobs_digests; if !blobs1.contains(digest))
+ for ((_, digest) <- command.blobs_defined; if !blobs1.contains(digest))
blobs1 += digest
if (!commands1.isDefinedAt(command.id))
--- a/src/Pure/PIDE/protocol.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML Sun Aug 10 14:34:43 2014 +0200
@@ -123,5 +123,9 @@
| Exn.Exn exn => (Runtime.exn_error_message exn; false));
in Output.protocol_message (Markup.use_theories_result id ok) [] end);
+val _ =
+ Isabelle_Process.protocol_command "ML_System.share_common_data"
+ (fn [] => ML_System.share_common_data ());
+
end;
--- a/src/Pure/PIDE/protocol.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Sun Aug 10 14:34:43 2014 +0200
@@ -145,8 +145,8 @@
val status = Status.merge(states.iterator.map(_.protocol_status))
if (status.is_running) running += 1
+ else if (status.is_failed) failed += 1
else if (status.is_warned) warned += 1
- else if (status.is_failed) failed += 1
else if (status.is_finished) finished += 1
else unprocessed += 1
}
--- a/src/Pure/PIDE/query_operation.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/PIDE/query_operation.ML Sun Aug 10 14:34:43 2014 +0200
@@ -2,7 +2,7 @@
Author: Makarius
One-shot query operations via asynchronous print functions and temporary
-document overlay.
+document overlays.
*)
signature QUERY_OPERATION =
--- a/src/Pure/PIDE/session.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/PIDE/session.scala Sun Aug 10 14:34:43 2014 +0200
@@ -47,7 +47,6 @@
sealed case class Change(
previous: Document.Version,
- doc_blobs: Document.Blobs,
syntax_changed: Boolean,
deps_changed: Boolean,
doc_edits: List[Document.Edit_Command],
@@ -177,8 +176,7 @@
/* tuning parameters */
def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages)
- def message_delay: Time = Time.seconds(0.1) // prover input/output messages
- def prune_delay: Time = Time.seconds(60.0) // prune history -- delete old versions
+ def prune_delay: Time = Time.seconds(60.0) // prune history (delete old versions)
def prune_size: Int = 0 // size of retained history
def syslog_limit: Int = 100
def reparse_limit: Int = 0
@@ -380,15 +378,15 @@
def id_command(command: Command)
{
for {
- digest <- command.blobs_digests
+ (name, digest) <- command.blobs_defined
if !global_state.value.defined_blob(digest)
} {
- change.doc_blobs.get(digest) match {
+ change.version.nodes(name).get_blob match {
case Some(blob) =>
global_state.change(_.define_blob(digest))
prover.get.define_blob(digest, blob.bytes)
case None =>
- Output.error_message("Missing blob for SHA1 digest " + digest)
+ Output.error_message("Missing blob " + quote(name.toString))
}
}
--- a/src/Pure/Thy/thy_syntax.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Sun Aug 10 14:34:43 2014 +0200
@@ -490,6 +490,6 @@
(doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(Some(syntax), nodes))
}
- Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
+ Session.Change(previous, syntax_changed, deps_changed, doc_edits, version)
}
}
--- a/src/Pure/Tools/ml_statistics.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/Tools/ml_statistics.scala Sun Aug 10 14:34:43 2014 +0200
@@ -33,6 +33,12 @@
/* standard fields */
+ val tasks_fields =
+ ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+
+ val workers_fields =
+ ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
+
val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
val heap_fields =
@@ -47,15 +53,9 @@
val speed_fields = ("Speed", List("speed_CPU", "speed_GC"))
- val tasks_fields =
- ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
-
- val workers_fields =
- ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
-
val standard_fields =
- List(GC_fields, heap_fields, threads_fields, time_fields, speed_fields,
- tasks_fields, workers_fields)
+ List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
+ time_fields, speed_fields)
}
final class ML_Statistics private(val name: String, val stats: List[Properties.T])
--- a/src/Pure/config.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/config.ML Sun Aug 10 14:34:43 2014 +0200
@@ -130,13 +130,10 @@
fun map_value f (context as Context.Proof ctxt) =
let val context' = update_value f context in
if global andalso
- Context_Position.is_visible ctxt andalso
+ Context_Position.is_really_visible ctxt andalso
print_value (get_value (Context.Theory (Context.theory_of context'))) <>
print_value (get_value context')
- then
- (if Context_Position.is_visible ctxt then
- warning ("Ignoring local change of global option " ^ quote name)
- else (); context)
+ then (warning ("Ignoring local change of global option " ^ quote name); context)
else context'
end
| map_value f context = update_value f context;
--- a/src/Pure/context_position.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/context_position.ML Sun Aug 10 14:34:43 2014 +0200
@@ -11,6 +11,8 @@
val is_visible_global: theory -> bool
val set_visible: bool -> Proof.context -> Proof.context
val set_visible_global: bool -> theory -> theory
+ val is_really_visible: Proof.context -> bool
+ val not_really: Proof.context -> Proof.context
val restore_visible: Proof.context -> Proof.context -> Proof.context
val restore_visible_global: theory -> theory -> theory
val is_reported_generic: Context.generic -> Position.T -> bool
@@ -28,21 +30,25 @@
structure Data = Generic_Data
(
- type T = bool option;
- val empty: T = NONE;
+ type T = bool option * bool option; (*really, visible*)
+ val empty: T = (NONE, NONE);
val extend = I;
- fun merge (x, y): T = if is_some x then x else y;
+ fun merge ((a, b), (a', b')) : T = (merge_options (a, a'), merge_options (b, b'));
);
-val is_visible_generic = the_default true o Data.get;
+val is_visible_generic = the_default true o snd o Data.get;
val is_visible = is_visible_generic o Context.Proof;
val is_visible_global = is_visible_generic o Context.Theory;
-val set_visible = Context.proof_map o Data.put o SOME;
-val set_visible_global = Context.theory_map o Data.put o SOME;
+val set_visible = Context.proof_map o Data.map o apsnd o K o SOME;
+val set_visible_global = Context.theory_map o Data.map o apsnd o K o SOME;
-val restore_visible = set_visible o is_visible;
-val restore_visible_global = set_visible_global o is_visible_global;
+val is_really = the_default true o fst o Data.get o Context.Proof;
+fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt;
+val not_really = Context.proof_map (Data.map (apfst (K (SOME false))));
+
+val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof;
+val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory;
fun is_reported_generic context pos = is_visible_generic context andalso Position.is_reported pos;
fun is_reported ctxt pos = is_visible ctxt andalso Position.is_reported pos;
--- a/src/Pure/library.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/library.ML Sun Aug 10 14:34:43 2014 +0200
@@ -266,6 +266,7 @@
fun error msg = raise ERROR msg;
fun cat_error "" msg = error msg
+ | cat_error msg "" = error msg
| cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
fun assert_all pred list msg =
--- a/src/Pure/library.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/library.scala Sun Aug 10 14:34:43 2014 +0200
@@ -25,6 +25,7 @@
def cat_message(msg1: String, msg2: String): String =
if (msg1 == "") msg2
+ else if (msg2 == "") msg1
else msg1 + "\n" + msg2
def cat_error(msg1: String, msg2: String): Nothing =
--- a/src/Pure/raw_simplifier.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Pure/raw_simplifier.ML Sun Aug 10 14:34:43 2014 +0200
@@ -385,7 +385,7 @@
val thy' = Proof_Context.theory_of ctxt';
in Context.theory_map (Simpset.map (K (simpset_of ctxt'))) thy' end;
-fun map_ss f = Context.mapping (map_theory_simpset f) f;
+fun map_ss f = Context.mapping (map_theory_simpset (f o Context_Position.not_really)) f;
val clear_simpset =
map_simpset (fn Simpset ({depth, ...}, {mk_rews, termless, subgoal_tac, solvers, ...}) =>
@@ -428,7 +428,7 @@
val simp_trace = Config.bool simp_trace_raw;
fun cond_warning ctxt msg =
- if Context_Position.is_visible ctxt then warning (msg ()) else ();
+ if Context_Position.is_really_visible ctxt then warning (msg ()) else ();
fun cond_tracing' ctxt flag msg =
if Config.get ctxt flag then
@@ -593,6 +593,7 @@
fun add_simp thm ctxt = ctxt addsimps [thm];
fun del_simp thm ctxt = ctxt delsimps [thm];
+
(* congs *)
local
--- a/src/Sequents/prover.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Sequents/prover.ML Sun Aug 10 14:34:43 2014 +0200
@@ -78,11 +78,13 @@
Pack (rules |> which (fn ths =>
if member Thm.eq_thm_prop ths th then
let
- val ctxt = Context.proof_of context;
val _ =
- if Context_Position.is_visible ctxt then
- warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
- else ();
+ (case context of
+ Context.Proof ctxt =>
+ if Context_Position.is_really_visible ctxt then
+ warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
+ else ()
+ | _ => ());
in ths end
else sort_rules (th :: ths))));
--- a/src/Tools/Code/lib/Tools/codegen Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/Code/lib/Tools/codegen Sun Aug 10 14:34:43 2014 +0200
@@ -50,8 +50,10 @@
## invoke code generation
-FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \
- (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \
+FORMAL_CMD="Runtime.toplevel_program (fn () => (use_thy thyname; ML_Context.eval_source_in \
+ (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) \
+ ML_Compiler.flags \
+ {delimited=true, text=ml_cmd, pos=Position.none})) \
handle _ => exit 1;"
ACTUAL_CMD="val thyname = \"$THYNAME\"; \
--- a/src/Tools/jEdit/etc/options Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/etc/options Sun Aug 10 14:34:43 2014 +0200
@@ -42,6 +42,12 @@
public option jedit_completion : bool = true
-- "enable completion popup"
+public option jedit_completion_select_enter : bool = false
+ -- "select completion item via ENTER"
+
+public option jedit_completion_select_tab : bool = true
+ -- "select completion item via TAB"
+
public option jedit_completion_context : bool = true
-- "use semantic language context for completion"
--- a/src/Tools/jEdit/src/active.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala Sun Aug 10 14:34:43 2014 +0200
@@ -48,8 +48,14 @@
GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
}
- case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
+ case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
+ val link =
+ props match {
+ case Position.Id(id) => PIDE.editor.hyperlink_command_id(snapshot, id)
+ case _ => None
+ }
GUI_Thread.later {
+ link.foreach(_.follow(view))
view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
}
--- a/src/Tools/jEdit/src/completion_popup.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Sun Aug 10 14:34:43 2014 +0200
@@ -702,7 +702,10 @@
{
if (!e.isConsumed) {
e.getKeyCode match {
- case KeyEvent.VK_TAB =>
+ case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
+ if (complete_selected()) e.consume
+ hide_popup()
+ case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
if (complete_selected()) e.consume
hide_popup()
case KeyEvent.VK_ESCAPE =>
--- a/src/Tools/jEdit/src/isabelle.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Sun Aug 10 14:34:43 2014 +0200
@@ -232,8 +232,8 @@
s: String)
{
if (!snapshot.is_outdated) {
- snapshot.state.find_command(snapshot.version, id) match {
- case Some((node, command)) =>
+ (snapshot.state.find_command(snapshot.version, id), PIDE.document_model(buffer)) match {
+ case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
node.command_start(command) match {
case Some(start) =>
JEdit_Lib.buffer_edit(buffer) {
@@ -248,7 +248,7 @@
}
case None =>
}
- case None =>
+ case _ =>
}
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Aug 10 14:34:43 2014 +0200
@@ -110,16 +110,16 @@
/* overlays */
- private var overlays = Document.Overlays.empty
+ private val overlays = Synchronized(Document.Overlays.empty)
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
- synchronized { overlays(name) }
+ overlays.value(name)
override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
- synchronized { overlays = overlays.insert(command, fn, args) }
+ overlays.change(_.insert(command, fn, args))
override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
- synchronized { overlays = overlays.remove(command, fn, args) }
+ overlays.change(_.remove(command, fn, args))
/* navigation */
@@ -246,7 +246,7 @@
def hyperlink_command_id(
snapshot: Document.Snapshot,
id: Document_ID.Generic,
- offset: Symbol.Offset): Option[Hyperlink] =
+ offset: Symbol.Offset = 0): Option[Hyperlink] =
{
snapshot.state.find_command(snapshot.version, id) match {
case Some((node, command)) => hyperlink_command(snapshot, command, offset)
--- a/src/Tools/jEdit/src/jedit_lib.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Aug 10 14:34:43 2014 +0200
@@ -295,7 +295,7 @@
def string_width(s: String): Double =
painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
- val unit = string_width(Pretty.space)
+ val unit = string_width(Pretty.space) max 1.0
val average = string_width("mix") / (3 * unit)
def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sun Aug 10 14:34:43 2014 +0200
@@ -49,7 +49,8 @@
override def append(dir: String, source_path: Path): String =
{
val path = source_path.expand
- if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
+ if (dir == "" || path.is_absolute)
+ MiscUtilities.resolveSymlinks(Isabelle_System.platform_path(path))
else if (path.is_current) dir
else {
val vfs = VFSManager.getVFSForPath(dir)
--- a/src/Tools/jEdit/src/monitor_dockable.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Sun Aug 10 14:34:43 2014 +0200
@@ -1,7 +1,7 @@
/* Title: Tools/jEdit/src/monitor_dockable.scala
Author: Makarius
-Monitor for runtime statistics.
+Monitor for ML statistics.
*/
package isabelle.jedit
@@ -9,7 +9,10 @@
import isabelle._
-import scala.swing.{TextArea, ScrollPane, Component}
+import java.awt.BorderLayout
+
+import scala.swing.{TextArea, ScrollPane, Component, ComboBox, Button}
+import scala.swing.event.{SelectionChanged, ButtonClicked}
import org.jfree.chart.ChartPanel
import org.jfree.data.xy.XYSeriesCollection
@@ -24,16 +27,51 @@
/* chart data -- owned by GUI thread */
+ private var data_name = ML_Statistics.standard_fields(0)._1
private val chart = ML_Statistics.empty.chart(null, Nil)
private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection]
- private val delay_update =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
- ML_Statistics("", rev_stats.value.reverse)
- .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
+ private def update_chart: Unit =
+ ML_Statistics.standard_fields.find(_._1 == data_name) match {
+ case None =>
+ case Some((_, fields)) =>
+ ML_Statistics("", rev_stats.value.reverse).update_data(data, fields)
}
+ private val delay_update =
+ GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
+
+
+ /* controls */
+
+ private val select_data = new ComboBox[String](
+ ML_Statistics.standard_fields.map(_._1))
+ {
+ tooltip = "Select visualized data collection"
+ listenTo(selection)
+ reactions += {
+ case SelectionChanged(_) =>
+ data_name = selection.item
+ update_chart
+ }
+ }
+
+ val reset_data = new Button("Reset") {
+ tooltip = "Reset accumulated data"
+ reactions += {
+ case ButtonClicked(_) =>
+ rev_stats.change(_ => Nil)
+ update_chart
+ }
+ }
+
+ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(select_data, reset_data)
+
+
+ /* layout */
+
set_content(new ChartPanel(chart))
+ add(controls.peer, BorderLayout.NORTH)
/* main */
--- a/src/Tools/jEdit/src/plugin.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Sun Aug 10 14:34:43 2014 +0200
@@ -391,6 +391,7 @@
PIDE.session = new Session(resources) {
override def output_delay = PIDE.options.seconds("editor_output_delay")
+ override def prune_delay = PIDE.options.seconds("editor_prune_delay")
override def reparse_limit = PIDE.options.int("editor_reparse_limit")
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sun Aug 10 14:34:43 2014 +0200
@@ -246,34 +246,32 @@
val screen = JEdit_Lib.screen_location(layered, location)
val size =
{
+ val bounds = Rendering.popup_bounds
+
+ val w_max = layered.getWidth min (screen.bounds.width * bounds).toInt
+ val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt
+
val painter = pretty_text_area.getPainter
+ val geometry = JEdit_Lib.window_geometry(tip, painter)
val metric = JEdit_Lib.pretty_metric(painter)
- val margin = rendering.tooltip_margin * metric.average
+
+ val margin =
+ ((rendering.tooltip_margin * metric.average) min
+ ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
val formatted = Pretty.formatted(info.info, margin, metric)
val lines =
XML.traverse_text(formatted)(0)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
- val geometry = JEdit_Lib.window_geometry(tip, tip.pretty_text_area.getPainter)
- val bounds = Rendering.popup_bounds
-
- val h0 = layered.getHeight
- val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
- val h2 = h0 min (screen.bounds.height * bounds).toInt
- val h = h1 min h2
-
+ val h = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
val margin1 =
- if (h1 <= h2)
+ if (h <= h_max)
(0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
else margin
+ val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
- val w0 = layered.getWidth
- val w1 = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
- val w2 = w0 min (screen.bounds.width * bounds).toInt
- val w = w1 min w2
-
- new Dimension(w, h)
+ new Dimension(w min w_max, h min h_max)
}
new Popup(layered, tip, screen.relative(layered, size), size)
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sun Aug 10 14:34:43 2014 +0200
@@ -205,6 +205,7 @@
private val mouse_motion_listener = new MouseMotionAdapter {
override def mouseDragged(evt: MouseEvent) {
robust_body(()) {
+ active_reset()
Completion_Popup.Text_Area.dismissed(text_area)
Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
}
--- a/src/Tools/jEdit/src/scala_console.scala Sun Aug 10 14:31:06 2014 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Sun Aug 10 14:34:43 2014 +0200
@@ -201,6 +201,7 @@
{
out.print(null,
"This shell evaluates Isabelle/Scala expressions.\n\n" +
+ "The contents of package isabelle and isabelle.jedit are imported.\n" +
"The following special toplevel bindings are provided:\n" +
" view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
" console -- jEdit Console plugin\n" +
--- a/src/ZF/Tools/datatype_package.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/ZF/Tools/datatype_package.ML Sun Aug 10 14:34:43 2014 +0200
@@ -51,9 +51,9 @@
FIXME: could insert all constant set expressions, e.g. nat->nat.*)
fun data_domain co (rec_tms, con_ty_lists) =
let val rec_hds = map head_of rec_tms
- val dummy = assert_all is_Const rec_hds
- (fn t => "Datatype set not previously declared as constant: " ^
- Syntax.string_of_term_global @{theory IFOL} t);
+ val dummy = rec_hds |> forall (fn t => is_Const t orelse
+ error ("Datatype set not previously declared as constant: " ^
+ Syntax.string_of_term_global @{theory IFOL} t));
val rec_names = (*nat doesn't have to be added*)
@{const_name nat} :: map (#1 o dest_Const) rec_hds
val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
@@ -69,9 +69,9 @@
val rec_hds = map head_of rec_tms;
- val dummy = assert_all is_Const rec_hds
- (fn t => "Datatype set not previously declared as constant: " ^
- Syntax.string_of_term_global thy t);
+ val dummy = rec_hds |> forall (fn t => is_Const t orelse
+ error ("Datatype set not previously declared as constant: " ^
+ Syntax.string_of_term_global thy t));
val rec_names = map (#1 o dest_Const) rec_hds
val rec_base_names = map Long_Name.base_name rec_names
--- a/src/ZF/Tools/inductive_package.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sun Aug 10 14:34:43 2014 +0200
@@ -69,31 +69,31 @@
(*recT and rec_params should agree for all mutually recursive components*)
val rec_hds = map head_of rec_tms;
- val dummy = assert_all is_Const rec_hds
- (fn t => "Recursive set not previously declared as constant: " ^
- Syntax.string_of_term ctxt t);
+ val dummy = rec_hds |> forall (fn t => is_Const t orelse
+ error ("Recursive set not previously declared as constant: " ^
+ Syntax.string_of_term ctxt t));
(*Now we know they are all Consts, so get their names, type and params*)
val rec_names = map (#1 o dest_Const) rec_hds
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
val rec_base_names = map Long_Name.base_name rec_names;
- val dummy = assert_all Symbol_Pos.is_identifier rec_base_names
- (fn a => "Base name of recursive set not an identifier: " ^ a);
+ val dummy = rec_base_names |> forall (fn a => Symbol_Pos.is_identifier a orelse
+ error ("Base name of recursive set not an identifier: " ^ a));
local (*Checking the introduction rules*)
val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms;
fun intr_ok set =
case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
in
- val dummy = assert_all intr_ok intr_sets
- (fn t => "Conclusion of rule does not name a recursive set: " ^
- Syntax.string_of_term ctxt t);
+ val dummy = intr_sets |> forall (fn t => intr_ok t orelse
+ error ("Conclusion of rule does not name a recursive set: " ^
+ Syntax.string_of_term ctxt t));
end;
- val dummy = assert_all is_Free rec_params
- (fn t => "Param in recursion term not a free variable: " ^
- Syntax.string_of_term ctxt t);
+ val dummy = rec_params |> forall (fn t => is_Free t orelse
+ error ("Param in recursion term not a free variable: " ^
+ Syntax.string_of_term ctxt t));
(*** Construct the fixedpoint definition ***)
val mk_variant = singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] intr_tms));