--- a/ANNOUNCE Wed Sep 07 23:55:40 2011 +0200
+++ b/ANNOUNCE Thu Sep 08 00:23:23 2011 +0200
@@ -1,34 +1,15 @@
-Subject: Announcing Isabelle2011
+Subject: Announcing Isabelle2011-1
To: isabelle-users@cl.cam.ac.uk
-Isabelle2011 is now available.
-
-This version significantly improves upon Isabelle2009-2, see the NEWS
-file in the distribution for more details. Some notable changes are:
-
-* Experimental Prover IDE based on Isabelle/Scala and jEdit.
-
-* Coercive subtyping (configured in HOL/Complex_Main).
-
-* HOL code generation: Scala as another target language.
-
-* HOL: partial_function definitions.
+Isabelle2011-1 is now available.
-* HOL: various tool enhancements, including Quickcheck, Nitpick,
- Sledgehammer, SMT integration.
-
-* HOL: various additions to theory library, including HOL-Algebra,
- Imperative_HOL, Multivariate_Analysis, Probability.
+This version improves upon Isabelle2011, see the NEWS file in the
+distribution for more details. Some important changes are:
-* HOLCF: reorganization of library and related tools.
-
-* HOL/SPARK: interactive proof environment for verification conditions
- generated by the SPARK Ada program verifier.
-
-* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
+* FIXME
-You may get Isabelle2011 from the following mirror sites:
+You may get Isabelle2011-1 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
--- a/Admin/CHECKLIST Wed Sep 07 23:55:40 2011 +0200
+++ b/Admin/CHECKLIST Thu Sep 08 00:23:23 2011 +0200
@@ -3,9 +3,7 @@
- test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
-- test Proof General 4.1, 4.0, 3.7.1.1;
-
-- test Scala wrapper;
+- test Proof General 4.1, 3.7.1.1;
- check HTML header of library;
--- a/Admin/makebundle Wed Sep 07 23:55:40 2011 +0200
+++ b/Admin/makebundle Thu Sep 08 00:23:23 2011 +0200
@@ -75,7 +75,13 @@
)
case "$PLATFORM" in
- x86-cygwin)
+ *-darwin)
+ perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
+ "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
+ ;;
+ *-cygwin)
+ perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
+ "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
rm "$TMP/$ISABELLE_NAME/contrib/ProofGeneral"
ln -s ProofGeneral-3.7.1.1 "$TMP/$ISABELLE_NAME/contrib/ProofGeneral"
;;
--- a/CONTRIBUTORS Wed Sep 07 23:55:40 2011 +0200
+++ b/CONTRIBUTORS Thu Sep 08 00:23:23 2011 +0200
@@ -3,8 +3,8 @@
who is listed as an author in one of the source files of this Isabelle
distribution.
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2011-1
+-------------------------------
* September 2011: Peter Gammie
Theory HOL/Libary/Saturated: numbers with saturated arithmetic.
--- a/NEWS Wed Sep 07 23:55:40 2011 +0200
+++ b/NEWS Thu Sep 08 00:23:23 2011 +0200
@@ -1,8 +1,8 @@
Isabelle NEWS -- history user-relevant changes
==============================================
-New in this Isabelle version
-----------------------------
+New in Isabelle2011-1 (October 2011)
+------------------------------------
*** General ***
@@ -466,6 +466,9 @@
INCOMPATIBILITY, classical tactics and derived proof methods require
proper Proof.context.
+
+*** System ***
+
* Scala layer provides JVM method invocation service for static
methods of type (String)String, see Invoke_Scala.method in ML. For
example:
@@ -475,6 +478,10 @@
Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this
allows to pass structured values between ML and Scala.
+* The IsabelleText fonts includes some further glyphs to support the
+Prover IDE. Potential INCOMPATIBILITY: users who happen to have
+installed a local copy (which is normally *not* required) need to
+delete or update it from ~~/lib/fonts/.
New in Isabelle2011 (January 2011)
--- a/README Wed Sep 07 23:55:40 2011 +0200
+++ b/README Thu Sep 08 00:23:23 2011 +0200
@@ -16,8 +16,8 @@
* The Poly/ML compiler and runtime system (version 5.2.1 or later).
* The GNU bash shell (version 3.x or 2.x).
* Perl (version 5.x).
+ * Java 1.6.x from Oracle or Apple -- for Scala and jEdit.
* GNU Emacs (version 23) -- for the Proof General 4.x interface.
- * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
* A complete LaTeX installation -- for document preparation.
Installation
@@ -31,17 +31,18 @@
User interface
+ Isabelle/jEdit is an emerging Prover IDE based on advanced
+ technology of Isabelle/Scala. It provides a metaphor of continuous
+ proof checking of a versioned collection of theory sources, with
+ instantaneous feedback in real-time and rich semantic markup
+ associated with the formal text.
+
The classic Isabelle user interface is Proof General by David
Aspinall and others. It is a generic Emacs interface for proof
assistants, including Isabelle. Its most prominent feature is
script management, providing a metaphor of stepwise proof script
editing.
- Isabelle/jEdit is an experimental Prover IDE based on advanced
- technology of Isabelle/Scala. It provides a metaphor of continuous
- proof checking of a versioned collection of theory sources, with
- instantaneous feedback in real-time.
-
Other sources of information
The Isabelle Page
--- a/doc/Contents Wed Sep 07 23:55:40 2011 +0200
+++ b/doc/Contents Thu Sep 08 00:23:23 2011 +0200
@@ -1,4 +1,4 @@
-Learning and using Isabelle
+Miscellaneous tutorials
tutorial Tutorial on Isabelle/HOL
main What's in Main
isar-overview Tutorial on Isar
--- a/src/Pure/PIDE/document.ML Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Pure/PIDE/document.ML Thu Sep 08 00:23:23 2011 +0200
@@ -331,7 +331,6 @@
let
val is_init = Toplevel.is_init tr;
val is_proof = Keyword.is_proof (Toplevel.name_of tr);
- val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
val _ = Multithreading.interrupted ();
val _ = Toplevel.status tr Markup.forked;
@@ -343,13 +342,18 @@
in
(case result of
NONE =>
- (if null errs then Exn.interrupt () else ();
- Toplevel.status tr Markup.failed;
- (st, no_print))
+ let
+ val _ = if null errs then Exn.interrupt () else ();
+ val _ = Toplevel.status tr Markup.failed;
+ in (st, no_print) end
| SOME st' =>
- (Toplevel.status tr Markup.finished;
- proof_status tr st';
- (st', if do_print then print_state tr st' else no_print)))
+ let
+ val _ = Toplevel.status tr Markup.finished;
+ val _ = proof_status tr st';
+ val do_print =
+ not is_init andalso
+ (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+ in (st', if do_print then print_state tr st' else no_print) end)
end;
end;
--- a/src/Pure/PIDE/xml.ML Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Pure/PIDE/xml.ML Thu Sep 08 00:23:23 2011 +0200
@@ -47,6 +47,7 @@
val parse_element: string list -> tree * string list
val parse_document: string list -> tree * string list
val parse: string -> tree
+ val cache: unit -> tree -> tree
exception XML_ATOM of string
exception XML_BODY of body
structure Encode: XML_DATA_OPS
@@ -228,6 +229,48 @@
end;
+(** cache for substructural sharing **)
+
+fun tree_ord tu =
+ if pointer_eq tu then EQUAL
+ else
+ (case tu of
+ (Text _, Elem _) => LESS
+ | (Elem _, Text _) => GREATER
+ | (Text s, Text s') => fast_string_ord (s, s')
+ | (Elem e, Elem e') =>
+ prod_ord
+ (prod_ord fast_string_ord (list_ord (prod_ord fast_string_ord fast_string_ord)))
+ (list_ord tree_ord) (e, e'));
+
+structure Treetab = Table(type key = tree val ord = tree_ord);
+
+fun cache () =
+ let
+ val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table);
+ val trees = Unsynchronized.ref (Treetab.empty: unit Treetab.table);
+
+ fun string s =
+ if size s <= 1 then s
+ else
+ (case Symtab.lookup_key (! strings) s of
+ SOME (s', ()) => s'
+ | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s));
+
+ fun tree t =
+ (case Treetab.lookup_key (! trees) t of
+ SOME (t', ()) => t'
+ | NONE =>
+ let
+ val t' =
+ (case t of
+ Elem ((a, ps), b) => Elem ((string a, map (pairself string) ps), map tree b)
+ | Text s => Text (string s));
+ val _ = Unsynchronized.change trees (Treetab.update (t', ()));
+ in t' end);
+ in tree end;
+
+
(** XML as data representation language **)
--- a/src/Pure/PIDE/xml.scala Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Pure/PIDE/xml.scala Thu Sep 08 00:23:23 2011 +0200
@@ -84,7 +84,8 @@
def content(body: Body): Iterator[String] = content_stream(body).iterator
- /* pipe-lined cache for partial sharing */
+
+ /** cache for partial sharing (weak table) **/
class Cache(initial_size: Int = 131071, max_string: Int = 100)
{
--- a/src/Pure/Syntax/syntax.ML Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Thu Sep 08 00:23:23 2011 +0200
@@ -99,6 +99,7 @@
val string_of_sort_global: theory -> sort -> string
type syntax
val eq_syntax: syntax * syntax -> bool
+ val join_syntax: syntax -> unit
val lookup_const: syntax -> string -> string option
val is_keyword: syntax -> string -> bool
val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -508,6 +509,8 @@
fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
+fun join_syntax (Syntax ({gram, ...}, _)) = ignore (Future.join gram);
+
fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
--- a/src/Pure/System/session.scala Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Pure/System/session.scala Thu Sep 08 00:23:23 2011 +0200
@@ -22,7 +22,7 @@
//{{{
case object Global_Settings
- case object Perspective
+ case object Caret_Focus
case object Assignment
case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -52,7 +52,7 @@
/* pervasive event buses */
val global_settings = new Event_Bus[Session.Global_Settings.type]
- val perspective = new Event_Bus[Session.Perspective.type]
+ val caret_focus = new Event_Bus[Session.Caret_Focus.type]
val assignments = new Event_Bus[Session.Assignment.type]
val commands_changed = new Event_Bus[Session.Commands_Changed]
val phase_changed = new Event_Bus[Session.Phase]
--- a/src/Pure/theory.ML Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Pure/theory.ML Thu Sep 08 00:23:23 2011 +0200
@@ -147,6 +147,7 @@
|> Sign.local_path
|> Sign.map_naming (Name_Space.set_theory_name name)
|> apply_wrappers wrappers
+ |> tap (Syntax.join_syntax o Sign.syn_of)
end;
fun end_theory thy =
--- a/src/Tools/jEdit/README.html Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Tools/jEdit/README.html Thu Sep 08 00:23:23 2011 +0200
@@ -144,6 +144,11 @@
<em>Workaround:</em> Force re-parsing of files using such commands
via reload menu of jEdit.</li>
+ <li>No way to delete document nodes from the overall collection of
+ theories.<br/>
+ <em>Workaround:</em> Restart whole Isabelle/jEdit session in
+ worst-case situation.</li>
+
<li>No support for non-local markup, e.g. commands reporting on
previous commands (proof end on proof head), or markup produced by
loading external files.</li>
--- a/src/Tools/jEdit/src/document_view.scala Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Thu Sep 08 00:23:23 2011 +0200
@@ -362,7 +362,7 @@
private val caret_listener = new CaretListener {
private val delay = Swing_Thread.delay_last(session.input_delay) {
- session.perspective.event(Session.Perspective)
+ session.caret_focus.event(Session.Caret_Focus)
}
override def caretUpdate(e: CaretEvent) { delay() }
}
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Sep 07 23:55:40 2011 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Sep 08 00:23:23 2011 +0200
@@ -106,7 +106,7 @@
react {
case Session.Global_Settings => handle_resize()
case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
- case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
+ case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update()
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
}
}
@@ -116,14 +116,14 @@
{
Isabelle.session.global_settings += main_actor
Isabelle.session.commands_changed += main_actor
- Isabelle.session.perspective += main_actor
+ Isabelle.session.caret_focus += main_actor
}
override def exit()
{
Isabelle.session.global_settings -= main_actor
Isabelle.session.commands_changed -= main_actor
- Isabelle.session.perspective -= main_actor
+ Isabelle.session.caret_focus -= main_actor
}