--- a/.hgtags Mon Jun 21 19:33:51 2010 +0200
+++ b/.hgtags Tue Jun 22 18:15:44 2010 +0200
@@ -25,5 +25,4 @@
fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
-935c75359742ccfd4abba0c33a440241e6ef2b1e isa2009-2-test0
-d1cdbc7524b619815236e8e2e61e36809ee2d338 isa2009-2-test1
+35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2
--- a/Admin/CHECKLIST Mon Jun 21 19:33:51 2010 +0200
+++ b/Admin/CHECKLIST Tue Jun 22 18:15:44 2010 +0200
@@ -15,7 +15,7 @@
- Admin/update-keywords;
-- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS;
+- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
- diff NEWS wrt. last official release, which is read-only;
--- a/Admin/makebundle Mon Jun 21 19:33:51 2010 +0200
+++ b/Admin/makebundle Tue Jun 22 18:15:44 2010 +0200
@@ -66,7 +66,7 @@
HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz"
[ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE"
echo "heaps"
-tar -C "$ISABELLE_HOME" -x -z -f "$HEAPS_ARCHIVE"
+tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE"
BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
--- a/Admin/makedist Mon Jun 21 19:33:51 2010 +0200
+++ b/Admin/makedist Tue Jun 22 18:15:44 2010 +0200
@@ -145,11 +145,14 @@
rm -rf doc-src
mkdir -p contrib
+cat >contrib/README <<EOF
+This directory contains add-on components that contribute to the main
+Isabelle distribution. Separate licensing conditions apply, see each
+directory individually.
+EOF
cp doc/isabelle*.eps lib/logo
-rm Isabelle Isabelle.exe
-
if [ -z "$RELEASE" ]; then
{
@@ -200,9 +203,8 @@
mv "$DISTNAME" "${DISTNAME}-old"
mkdir "$DISTNAME"
-mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
- "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
- "$DISTNAME"
+mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
+ "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
mkdir "$DISTNAME/doc"
mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
--- a/INSTALL Mon Jun 21 19:33:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-
-Isabelle installation notes
-===========================
-
-1) System installation
-----------------------
-
-The Isabelle distribution includes both complete sources and
-precompiled binary packages for common Unix-like platforms.
-
-
-Quick installation
-------------------
-
-Ready-to-go packages are provided for the ML compiler and runtime
-system, the Isabelle sources, and some major object-logics. A minimal
-site installation of Isabelle on Linux/x86 works like this:
-
- tar -C /usr/local -xzf Isabelle.tar.gz
- tar -C /usr/local -xzf polyml.tar.gz
- tar -C /usr/local -xzf HOL_x86-linux.tar.gz
-
-The install prefix given above may be changed as appropriate; there is
-no need to install into a system directory like /usr/local at all. By
-default the ML system (and other contributed packages) are expected in
-any of the following locations:
-
- 1) [ISABELLE_HOME]/contrib
- 2) [ISABELLE_HOME]/..
- 4) /usr/local
- 3) /usr/share
- 5) /opt
-
-This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
-
-The installation may be finished as follows:
-
- cd [ISABELLE_HOME]
- ./bin/isabelle install -p /usr/local/bin
-
-The install utility creates global references to the present Isabelle
-installation, enabling users to invoke the Isabelle executables
-without explicit path names. This is the only place where a static
-reference to [ISABELLE_HOME] is created; thus isabelle install has to
-be run again whenever the Isabelle distribution is moved later.
-
-
-Compiling logics
-----------------
-
-The Isabelle.tar.gz archive already contains all Isabelle sources (and
-documentation). Precompiled object-logics are provided for
-convenience.
-
-Assuming proper configuration of the underlying ML system
-(cf. Isabelle's etc/settings), further object-logics may be compiled
-like this:
-
- [ISABELLE_HOME]/build FOL
-
-Special object-logic targets may be specified as follows:
-
- [ISABELLE_HOME]/build -m HOL-Algebra HOL
-
-
-2) User installation
---------------------
-
-Running the Isabelle binaries
------------------------------
-
-Users may invoke the main Isabelle binaries (isabelle and
-isabelle-process) directly from their location within the distribution
-directory [ISABELLE_HOME] like this:
-
- [ISABELLE_HOME]/bin/isabelle tty -l HOL
-
-This starts an interactive Isabelle session within the current text
-terminal. [ISABELLE_HOME]/bin may be put into the shell's search
-PATH. An alternative is to create global references to the Isabelle
-executables as follows:
-
- [ISABELLE_HOME]/bin/isabelle install -p ~/bin
-
-Note that the site-wide Isabelle installation may already provide
-Isabelle executables in some global bin directory (such as
-/usr/local/bin).
--- a/NEWS Mon Jun 21 19:33:51 2010 +0200
+++ b/NEWS Tue Jun 22 18:15:44 2010 +0200
@@ -202,15 +202,15 @@
'quotient_definition' may be used for defining types and constants by
quotient constructions. An example is the type of integers created by
quotienting pairs of natural numbers:
-
+
fun
- intrel :: "(nat * nat) => (nat * nat) => bool"
+ intrel :: "(nat * nat) => (nat * nat) => bool"
where
"intrel (x, y) (u, v) = (x + v = u + y)"
- quotient_type int = "nat × nat" / intrel
+ quotient_type int = "nat * nat" / intrel
by (auto simp add: equivp_def expand_fun_eq)
-
+
quotient_definition
"0::int" is "(0::nat, 0::nat)"
@@ -292,6 +292,8 @@
* Theory PReal, including the type "preal" and related operations, has
been removed. INCOMPATIBILITY.
+* Real: new development using Cauchy Sequences.
+
* Split off theory "Big_Operators" containing setsum, setprod,
Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.
@@ -511,6 +513,17 @@
"sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
- Removed "nitpick_intro" attribute. INCOMPATIBILITY.
+* Method "induct" now takes instantiations of the form t, where t is not
+ a variable, as a shorthand for "x == t", where x is a fresh variable.
+ If this is not intended, t has to be enclosed in parentheses.
+ By default, the equalities generated by definitional instantiations
+ are pre-simplified, which may cause parameters of inductive cases
+ to disappear, or may even delete some of the inductive cases.
+ Use "induct (no_simp)" instead of "induct" to restore the old
+ behaviour. The (no_simp) option is also understood by the "cases"
+ and "nominal_induct" methods, which now perform pre-simplification, too.
+ INCOMPATIBILITY.
+
*** HOLCF ***
@@ -683,6 +696,13 @@
See src/Tools/jEdit or "isabelle jedit" provided by the properly built
component.
+* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
+and Bluesky TeX fonts. It provides the usual Isabelle symbols,
+similar to the default assignment of the document preparation system
+(cf. isabellesym.sty). The Isabelle/Scala class Isabelle_System
+provides some operations for direct access to the font without asking
+the user for manual installation.
+
New in Isabelle2009-1 (December 2009)
@@ -3410,8 +3430,6 @@
* Real: proper support for ML code generation, including 'quickcheck'.
Reals are implemented as arbitrary precision rationals.
-* Real: new development using Cauchy Sequences.
-
* Hyperreal: Several constants that previously worked only for the
reals have been generalized, so they now work over arbitrary vector
spaces. Type annotations may need to be added in some cases; potential
--- a/README Mon Jun 21 19:33:51 2010 +0200
+++ b/README Tue Jun 22 18:15:44 2010 +0200
@@ -21,10 +21,9 @@
Installation
- Binary packages are available for Isabelle/HOL etc. for several
- platforms from the Isabelle web page. The system may be also built
- from scratch, using the tar.gz source distribution. See file
- INSTALL as distributed with Isabelle for more information.
+ Completely integrated bundles including the full Isabelle sources,
+ documentation, add-on tools and precompiled logic images for
+ several platforms are available from the Isabelle web page.
Further background information may be found in the Isabelle System
Manual, distributed with the sources (directory doc).
--- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 21 19:33:51 2010 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Tue Jun 22 18:15:44 2010 +0200
@@ -1277,16 +1277,16 @@
``strengthened'' inductive statements within the object-logic.
\begin{rail}
- 'cases' (insts * 'and') rule?
+ 'cases' '(no_simp)'? (insts * 'and') rule?
;
- 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
+ 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
;
'coinduct' insts taking rule?
;
rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
;
- definst: name ('==' | equiv) term | inst
+ definst: name ('==' | equiv) term | '(' term ')' | inst
;
definsts: ( definst *)
;
@@ -1320,7 +1320,9 @@
of premises of the case rule; within each premise, the \emph{prefix}
of variables is instantiated. In most situations, only a single
term needs to be specified; this refers to the first variable of the
- last premise (it is usually the same for all cases).
+ last premise (it is usually the same for all cases). The @{text
+ "(no_simp)"} option can be used to disable pre-simplification of
+ cases (see the description of @{method induct} below for details).
\item @{method induct}~@{text "insts R"} is analogous to the
@{method cases} method, but refers to induction rules, which are
@@ -1342,15 +1344,28 @@
present in the induction rule. This enables the writer to specify
only induction variables, or both predicates and variables, for
example.
-
+
Instantiations may be definitional: equations @{text "x \<equiv> t"}
introduce local definitions, which are inserted into the claim and
discharged after applying the induction rule. Equalities reappear
in the inductive cases, but have been transformed according to the
induction principle being involved here. In order to achieve
practically useful induction hypotheses, some variables occurring in
- @{text t} need to be fixed (see below).
-
+ @{text t} need to be fixed (see below). Instantiations of the form
+ @{text t}, where @{text t} is not a variable, are taken as a
+ shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is a fresh
+ variable. If this is not intended, @{text t} has to be enclosed in
+ parentheses. By default, the equalities generated by definitional
+ instantiations are pre-simplified using a specific set of rules,
+ usually consisting of distinctness and injectivity theorems for
+ datatypes. This pre-simplification may cause some of the parameters
+ of an inductive case to disappear, or may even completely delete
+ some of the inductive cases, if one of the equalities occurring in
+ their premises can be simplified to @{text False}. The @{text
+ "(no_simp)"} option can be used to disable pre-simplification.
+ Additional rules to be used in pre-simplification can be declared
+ using the @{attribute_def induct_simp} attribute.
+
The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
specification generalizes variables @{text "x\<^sub>1, \<dots>,
x\<^sub>m"} of the original goal before applying induction. Thus
--- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 21 19:33:51 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue Jun 22 18:15:44 2010 +0200
@@ -1275,16 +1275,16 @@
``strengthened'' inductive statements within the object-logic.
\begin{rail}
- 'cases' (insts * 'and') rule?
+ 'cases' '(no_simp)'? (insts * 'and') rule?
;
- 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
+ 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
;
'coinduct' insts taking rule?
;
rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
;
- definst: name ('==' | equiv) term | inst
+ definst: name ('==' | equiv) term | '(' term ')' | inst
;
definsts: ( definst *)
;
@@ -1317,7 +1317,8 @@
of premises of the case rule; within each premise, the \emph{prefix}
of variables is instantiated. In most situations, only a single
term needs to be specified; this refers to the first variable of the
- last premise (it is usually the same for all cases).
+ last premise (it is usually the same for all cases). The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification of
+ cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
\item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the
\hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
@@ -1339,15 +1340,27 @@
present in the induction rule. This enables the writer to specify
only induction variables, or both predicates and variables, for
example.
-
+
Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
introduce local definitions, which are inserted into the claim and
discharged after applying the induction rule. Equalities reappear
in the inductive cases, but have been transformed according to the
induction principle being involved here. In order to achieve
practically useful induction hypotheses, some variables occurring in
- \isa{t} need to be fixed (see below).
-
+ \isa{t} need to be fixed (see below). Instantiations of the form
+ \isa{t}, where \isa{t} is not a variable, are taken as a
+ shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is a fresh
+ variable. If this is not intended, \isa{t} has to be enclosed in
+ parentheses. By default, the equalities generated by definitional
+ instantiations are pre-simplified using a specific set of rules,
+ usually consisting of distinctness and injectivity theorems for
+ datatypes. This pre-simplification may cause some of the parameters
+ of an inductive case to disappear, or may even completely delete
+ some of the inductive cases, if one of the equalities occurring in
+ their premises can be simplified to \isa{False}. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification.
+ Additional rules to be used in pre-simplification can be declared
+ using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}simp}}}} attribute.
+
The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus
induction hypotheses may become sufficiently general to get the
--- a/doc-src/Ref/introduction.tex Mon Jun 21 19:33:51 2010 +0200
+++ b/doc-src/Ref/introduction.tex Tue Jun 22 18:15:44 2010 +0200
@@ -5,9 +5,7 @@
\index{starting up|bold}\nobreak
%
We assume that your local Isabelle administrator (this might be you!) has
-already installed the Isabelle system together with appropriate object-logics
---- otherwise see the \texttt{README} and \texttt{INSTALL} files in the
-top-level directory of the distribution on how to do this.
+already installed the Isabelle system together with appropriate object-logics.
\medskip Let $\langle isabellehome \rangle$ denote the location where
the distribution has been installed. To run Isabelle from a the shell
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jun 21 19:33:51 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jun 22 18:15:44 2010 +0200
@@ -5284,7 +5284,7 @@
(* class constraint due to continuous_on_inverse *)
shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
\<Longrightarrow> s homeomorphic t"
- unfolding homeomorphic_def by(auto intro: homeomorphism_compact)
+ unfolding homeomorphic_def by (metis homeomorphism_compact)
text{* Preservation of topological properties. *}
--- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 21 19:33:51 2010 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Tue Jun 22 18:15:44 2010 +0200
@@ -491,11 +491,11 @@
and b: "\<Gamma> \<turnstile> e' : T'"
shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T"
using a b
-proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
+proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
case (t_VAR y T x e' \<Delta>)
then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)"
and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)"
- and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
+ and a3: "\<Gamma> \<turnstile> e' : T'" .
from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
{ assume eq: "x=y"
from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
--- a/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 21 19:33:51 2010 +0200
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Tue Jun 22 18:15:44 2010 +0200
@@ -141,11 +141,11 @@
and b: "\<Gamma> \<turnstile> e' : T'"
shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T"
using a b
-proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
+proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
case (t_Var y T x e' \<Delta>)
then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)"
and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)"
- and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
+ and a3: "\<Gamma> \<turnstile> e' : T'" .
from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
{ assume eq: "x=y"
from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
--- a/src/HOL/Nominal/INSTALL Mon Jun 21 19:33:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-
-Installation Notes for the Nominal Datatype Package
-===================================================
-
-Although the nominal datatype package is an official
-package in the development snapshot of Isabelle, we
-keep a semi-official snapshot of Isabelle and Nominal
-under
-
- http://isabelle.in.tum.de/nominal/
-
-This snapshot contains the latest stable release of the
-nominal datatype package.
-
-To install it, follow the instructions of Isabelle's INSTALL
-about how a snap-shot can be set up. The building process
-needs to be started inside the [ISABELLE_HOME] directory with
-the command:
-
- ./build -m HOL-Nominal
-
-After the build completes, install the files with the command
-
- ./bin/isabelle install -p /usr/local/bin
-
-where /usr/local/bin needs to be replaced by an appropriate
-directory, if you are not root on the system.
-
-The sources of the nominal datatype package can be found
-in the directory
-
- [ISABELLE_HOME]/src/HOL/Nominal
-
-The examples are in
-
- [ISABELLE_HOME]/src/HOL/Nominal/Examples
-
-Starting Isabelle with the Nominal Datatype Package Preloaded
-=============================================================
-
-Isabelle and the Proof-General interface can be started
-with
-
- Isabelle -L HOL-Nominal <<theory file to be opened>> &
-
-on the command-line. This automatically loads the correct
-keyword file needed for the nominal datatype package.
-
-Problems with starting Isabelle and Proof-General usually
-come from old versions of Proof-General. So make sure you
-have installed at least the version ProofGeneral-3.6pre050930.
-
-If you have problems or comments about the installation process,
-please make use of the nominal mailing list at
-
-https://mailmanbroy.informatik.tu-muenchen.de/pipermail/nominal-isabelle/
-
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Jun 21 19:33:51 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 22 18:15:44 2010 +0200
@@ -874,7 +874,7 @@
end
| Cst (cst, T, _) =>
if cst = Unknown orelse cst = Unrep then
- case (is_boolean_type T, polar) of
+ case (is_boolean_type T, polar |> unsound ? flip_polarity) of
(true, Pos) => Cst (False, T, Formula Pos)
| (true, Neg) => Cst (True, T, Formula Neg)
| _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 21 19:33:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 22 18:15:44 2010 +0200
@@ -137,7 +137,7 @@
fun mk_skolem_id t =
let val T = fastype_of t in
- Const (@{const_name skolem_id}, T --> T) $ Envir.beta_eta_contract t
+ Const (@{const_name skolem_id}, T --> T) $ Envir.beta_norm t
end
(*Traverse a theorem, accumulating Skolem function definitions.*)
@@ -409,6 +409,7 @@
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
+ val inline = false (* FIXME: temporary *)
val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in
@@ -446,7 +447,7 @@
(**** Translate a set of theorems into CNF ****)
-fun pair_name_cls k (n, []) = []
+fun pair_name_cls _ (_, []) = []
| pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
(*The combination of rev and tail recursion preserves the original order*)
--- a/src/Pure/General/pretty.scala Mon Jun 21 19:33:51 2010 +0200
+++ b/src/Pure/General/pretty.scala Tue Jun 22 18:15:44 2010 +0200
@@ -134,7 +134,7 @@
def string_of(input: List[XML.Tree], margin: Int = margin_default,
metric: String => Double = metric_default): String =
- formatted(input).iterator.flatMap(XML.content).mkString
+ formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
/* unformatted output */
--- a/src/Pure/Isar/runtime.ML Mon Jun 21 19:33:51 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Tue Jun 22 18:15:44 2010 +0200
@@ -54,6 +54,7 @@
val detailed = ! Output.debugging;
fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
+ | exn_msg _ (Exn.EXCEPTIONS []) = "Exception."
| exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
| exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
--- a/src/Pure/PIDE/command.scala Mon Jun 21 19:33:51 2010 +0200
+++ b/src/Pure/PIDE/command.scala Tue Jun 22 18:15:44 2010 +0200
@@ -48,8 +48,7 @@
def name: String = if (is_command) span.head.content else ""
override def toString =
- if (is_command) name + "(" + id + ")"
- else if (is_ignored) "<ignored>" else "<malformed>"
+ id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
/* source text */
--- a/src/Pure/System/isabelle_system.scala Mon Jun 21 19:33:51 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Jun 22 18:15:44 2010 +0200
@@ -12,6 +12,7 @@
BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
File, IOException}
import java.awt.{GraphicsEnvironment, Font}
+import java.awt.font.TextAttribute
import scala.io.Source
import scala.util.matching.Regex
@@ -336,31 +337,23 @@
/* fonts */
val font_family = getenv_strict("ISABELLE_FONT_FAMILY")
+ val font_family_default = "IsabelleText"
def get_font(size: Int = 1, bold: Boolean = false): Font =
new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
+ def create_default_font(bold: Boolean = false): Font =
+ if (bold)
+ Font.createFont(Font.TRUETYPE_FONT,
+ platform_file("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"))
+ else
+ Font.createFont(Font.TRUETYPE_FONT,
+ platform_file("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"))
+
def install_fonts()
{
- def create_font(bold: Boolean): Font =
- {
- val name =
- if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
- else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
- Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
- }
- def check_font() = get_font().getFamily == font_family
-
- if (!check_font()) {
- val font = create_font(false)
- val bold_font = create_font(true)
-
- val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
- ge.registerFont(font)
- // workaround strange problem with Apple's Java 1.6 font manager
- // FIXME does not quite work!?
- if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
- if (!check_font()) error("Failed to install IsabelleText fonts")
- }
+ val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
+ ge.registerFont(create_default_font(bold = false))
+ ge.registerFont(create_default_font(bold = true))
}
}
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jun 21 19:33:51 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Tue Jun 22 18:15:44 2010 +0200
@@ -155,9 +155,11 @@
def to: Int => Int = model.to_current(document, _)
def from: Int => Int = model.from_current(document, _)
+ /* FIXME
for (text_area <- Isabelle.jedit_text_areas(model.buffer)
if Document_View(text_area).isDefined)
Document_View(text_area).get.set_styles()
+ */
def handle_token(style: Byte, offset: Int, length: Int) =
handler.handleToken(line_segment, style, offset, length, context)
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jun 21 19:33:51 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Jun 22 18:15:44 2010 +0200
@@ -129,19 +129,18 @@
reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
}
tracing.selected = show_tracing
- tracing.tooltip =
- "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
+ tracing.tooltip = "Indicate output of tracing messages"
private val auto_update = new CheckBox("Auto update") {
reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
}
auto_update.selected = follow_caret
- auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>"
+ auto_update.tooltip = "Indicate automatic update following cursor movement"
private val update = new Button("Update") {
reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
}
- update.tooltip = "<html>Update display according to the command at cursor position</html>"
+ update.tooltip = "Update display according to the command at cursor position"
val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
add(controls.peer, BorderLayout.NORTH)