# HG changeset patch
# User wenzelm
# Date 1315434203 -7200
# Node ID 7798deb6f8fa9e01365edb893c30e1f0ca33b81f
# Parent  fe33d66551860470552a44950262f7b48007cccc# Parent  df3626d1066ee623a642183d58c32490c5c0bdf4
merged

diff -r fe33d6655186 -r 7798deb6f8fa ANNOUNCE
--- 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/
diff -r fe33d6655186 -r 7798deb6f8fa Admin/CHECKLIST
--- 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;
 
diff -r fe33d6655186 -r 7798deb6f8fa Admin/makebundle
--- 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"
     ;;
diff -r fe33d6655186 -r 7798deb6f8fa CONTRIBUTORS
--- 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.
diff -r fe33d6655186 -r 7798deb6f8fa NEWS
--- 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)
diff -r fe33d6655186 -r 7798deb6f8fa README
--- 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
diff -r fe33d6655186 -r 7798deb6f8fa doc/Contents
--- 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
diff -r fe33d6655186 -r 7798deb6f8fa src/Pure/PIDE/document.ML
--- 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;
diff -r fe33d6655186 -r 7798deb6f8fa src/Pure/PIDE/xml.ML
--- 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 **)
 
diff -r fe33d6655186 -r 7798deb6f8fa src/Pure/PIDE/xml.scala
--- 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)
   {
diff -r fe33d6655186 -r 7798deb6f8fa src/Pure/Syntax/syntax.ML
--- 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;
diff -r fe33d6655186 -r 7798deb6f8fa src/Pure/System/session.scala
--- 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]
diff -r fe33d6655186 -r 7798deb6f8fa src/Pure/theory.ML
--- 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 =
diff -r fe33d6655186 -r 7798deb6f8fa src/Tools/jEdit/README.html
--- 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>
diff -r fe33d6655186 -r 7798deb6f8fa src/Tools/jEdit/src/document_view.scala
--- 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() }
   }
diff -r fe33d6655186 -r 7798deb6f8fa src/Tools/jEdit/src/output_dockable.scala
--- 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
   }