# HG changeset patch
# User wenzelm
# Date 1281091082 -7200
# Node ID c75e9dc841c72471333038ca17a9b89a4d6ce04c
# Parent  17d9808ed626b7c1640bd2148dc7f4b818e32f34# Parent  e9b4835a54ee864999a2c8eaf8055d15d37344e6
merged

diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/BijectionRel.thy
--- a/src/HOL/Old_Number_Theory/BijectionRel.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/BijectionRel.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/BijectionRel.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Bijections between sets *}
 
-theory BijectionRel imports Main begin
+theory BijectionRel
+imports Main
+begin
 
 text {*
   Inductive definitions of bijections between two different sets and
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Chinese.thy
--- a/src/HOL/Old_Number_Theory/Chinese.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/Chinese.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
@@ -19,17 +20,15 @@
 
 subsection {* Definitions *}
 
-consts
-  funprod :: "(nat => int) => nat => nat => int"
-  funsum :: "(nat => int) => nat => nat => int"
-
-primrec
+primrec funprod :: "(nat => int) => nat => nat => int"
+where
   "funprod f i 0 = f i"
-  "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
+| "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
 
-primrec
+primrec funsum :: "(nat => int) => nat => nat => int"
+where
   "funsum f i 0 = f i"
-  "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
+| "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
 
 definition
   m_cond :: "nat => (nat => int) => bool" where
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,19 +1,18 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Euler.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Euler.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* Euler's criterion *}
 
-theory Euler imports Residues EvenOdd begin
+theory Euler
+imports Residues EvenOdd
+begin
 
-definition
-  MultInvPair :: "int => int => int => int set" where
-  "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+definition MultInvPair :: "int => int => int => int set"
+  where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
 
-definition
-  SetS        :: "int => int => int set set" where
-  "SetS        a p   =  (MultInvPair a p ` SRStar p)"
+definition SetS :: "int => int => int set set"
+  where "SetS a p = MultInvPair a p ` SRStar p"
 
 
 subsection {* Property for MultInvPair *}
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,4 +1,5 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/EulerFermat.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
@@ -17,49 +18,40 @@
 
 subsection {* Definitions and lemmas *}
 
-inductive_set
-  RsetR :: "int => int set set"
-  for m :: int
-  where
-    empty [simp]: "{} \<in> RsetR m"
-  | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
-      \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
+inductive_set RsetR :: "int => int set set" for m :: int
+where
+  empty [simp]: "{} \<in> RsetR m"
+| insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
+    \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
 
-fun
-  BnorRset :: "int \<Rightarrow> int => int set"
-where
+fun BnorRset :: "int \<Rightarrow> int => int set" where
   "BnorRset a m =
    (if 0 < a then
     let na = BnorRset (a - 1) m
     in (if zgcd a m = 1 then insert a na else na)
     else {})"
 
-definition
-  norRRset :: "int => int set" where
-  "norRRset m = BnorRset (m - 1) m"
+definition norRRset :: "int => int set"
+  where "norRRset m = BnorRset (m - 1) m"
 
-definition
-  noXRRset :: "int => int => int set" where
-  "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
+definition noXRRset :: "int => int => int set"
+  where "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
 
-definition
-  phi :: "int => nat" where
-  "phi m = card (norRRset m)"
+definition phi :: "int => nat"
+  where "phi m = card (norRRset m)"
 
-definition
-  is_RRset :: "int set => int => bool" where
-  "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
+definition is_RRset :: "int set => int => bool"
+  where "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
 
-definition
-  RRset2norRR :: "int set => int => int => int" where
-  "RRset2norRR A m a =
-     (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
-        SOME b. zcong a b m \<and> b \<in> norRRset m
-      else 0)"
+definition RRset2norRR :: "int set => int => int => int"
+  where
+    "RRset2norRR A m a =
+       (if 1 < m \<and> is_RRset A m \<and> a \<in> A then
+          SOME b. zcong a b m \<and> b \<in> norRRset m
+        else 0)"
 
-definition
-  zcongm :: "int => int => int => bool" where
-  "zcongm m = (\<lambda>a b. zcong a b m)"
+definition zcongm :: "int => int => int => bool"
+  where "zcongm m = (\<lambda>a b. zcong a b m)"
 
 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
   -- {* LCP: not sure why this lemma is needed now *}
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/EvenOdd.thy
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Quadratic_Reciprocity/EvenOdd.thy
+(*  Title:      HOL/Old_Number_Theory/EvenOdd.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
@@ -8,13 +8,11 @@
 imports Int2
 begin
 
-definition
-  zOdd    :: "int set" where
-  "zOdd = {x. \<exists>k. x = 2 * k + 1}"
+definition zOdd :: "int set"
+  where "zOdd = {x. \<exists>k. x = 2 * k + 1}"
 
-definition
-  zEven   :: "int set" where
-  "zEven = {x. \<exists>k. x = 2 * k}"
+definition zEven :: "int set"
+  where "zEven = {x. \<exists>k. x = 2 * k}"
 
 subsection {* Some useful properties about even and odd *}
 
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Factorization.thy
--- a/src/HOL/Old_Number_Theory/Factorization.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,41 +1,39 @@
-(*  Author:     Thomas Marthedal Rasmussen
+(*  Title:      HOL/Old_Number_Theory/Factorization.thy
+    Author:     Thomas Marthedal Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *}
 
 theory Factorization
-imports Main "~~/src/HOL/Old_Number_Theory/Primes" Permutation
+imports Primes Permutation
 begin
 
 
 subsection {* Definitions *}
 
-definition
-  primel :: "nat list => bool" where
-  "primel xs = (\<forall>p \<in> set xs. prime p)"
+definition primel :: "nat list => bool"
+  where "primel xs = (\<forall>p \<in> set xs. prime p)"
 
-consts
-  nondec :: "nat list => bool "
-  prod :: "nat list => nat"
-  oinsert :: "nat => nat list => nat list"
-  sort :: "nat list => nat list"
-
-primrec
+primrec nondec :: "nat list => bool"
+where
   "nondec [] = True"
-  "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
+| "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
 
-primrec
+primrec prod :: "nat list => nat"
+where
   "prod [] = Suc 0"
-  "prod (x # xs) = x * prod xs"
+| "prod (x # xs) = x * prod xs"
 
-primrec
+primrec oinsert :: "nat => nat list => nat list"
+where
   "oinsert x [] = [x]"
-  "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
+| "oinsert x (y # ys) = (if x \<le> y then x # y # ys else y # oinsert x ys)"
 
-primrec
+primrec sort :: "nat list => nat list"
+where
   "sort [] = []"
-  "sort (x # xs) = oinsert x (sort xs)"
+| "sort (x # xs) = oinsert x (sort xs)"
 
 
 subsection {* Arithmetic *}
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Fib.thy
--- a/src/HOL/Old_Number_Theory/Fib.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Fib.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,4 +1,4 @@
-(*  ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Fib.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 *)
@@ -19,8 +19,8 @@
 
 fun fib :: "nat \<Rightarrow> nat"
 where
-         "fib 0 = 0"
-|        "fib (Suc 0) = 1"
+  "fib 0 = 0"
+| "fib (Suc 0) = 1"
 | fib_2: "fib (Suc (Suc n)) = fib n + fib (Suc n)"
 
 text {*
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Finite2.thy
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,12 +1,11 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Finite2.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Finite2.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {*Finite Sets and Finite Sums*}
 
 theory Finite2
-imports Main IntFact Infinite_Set
+imports IntFact Infinite_Set
 begin
 
 text{*
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,6 +1,5 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
-    ID:         $Id$
-    Authors:    Jeremy Avigad, David Gray, and Adam Kramer)
+(*  Title:      HOL/Old_Number_Theory/Gauss.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* Gauss' Lemma *}
@@ -19,29 +18,12 @@
   assumes a_nonzero:    "0 < a"
 begin
 
-definition
-  A :: "int set" where
-  "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
-
-definition
-  B :: "int set" where
-  "B = (%x. x * a) ` A"
-
-definition
-  C :: "int set" where
-  "C = StandardRes p ` B"
-
-definition
-  D :: "int set" where
-  "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
-
-definition
-  E :: "int set" where
-  "E = C \<inter> {x. ((p - 1) div 2) < x}"
-
-definition
-  F :: "int set" where
-  "F = (%x. (p - x)) ` E"
+definition "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
+definition "B = (%x. x * a) ` A"
+definition "C = StandardRes p ` B"
+definition "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
+definition "E = C \<inter> {x. ((p - 1) div 2) < x}"
+definition "F = (%x. (p - x)) ` E"
 
 
 subsection {* Basic properties of p *}
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Int2.thy
--- a/src/HOL/Old_Number_Theory/Int2.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Int2.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
@@ -9,9 +8,8 @@
 imports Finite2 WilsonRuss
 begin
 
-definition
-  MultInv :: "int => int => int" where
-  "MultInv p x = x ^ nat (p - 2)"
+definition MultInv :: "int => int => int"
+  where "MultInv p x = x ^ nat (p - 2)"
 
 
 subsection {* Useful lemmas about dvd and powers *}
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/IntFact.thy
--- a/src/HOL/Old_Number_Theory/IntFact.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/IntFact.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/IntFact.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Factorial on integers *}
 
-theory IntFact imports IntPrimes begin
+theory IntFact
+imports IntPrimes
+begin
 
 text {*
   Factorial on integers and recursively defined set including all
@@ -14,15 +17,11 @@
   \bigskip
 *}
 
-fun
-  zfact :: "int => int"
-where
-  "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
+fun zfact :: "int => int"
+  where "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
 
-fun
-  d22set :: "int => int set"
-where
-  "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
+fun d22set :: "int => int set"
+  where "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
 
 
 text {*
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,11 +1,12 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/IntPrimes.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Divisibility and prime numbers (on integers) *}
 
 theory IntPrimes
-imports Main Primes
+imports Primes
 begin
 
 text {*
@@ -19,8 +20,7 @@
 
 subsection {* Definitions *}
 
-fun
-  xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
+fun xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
 where
   "xzgcda m n r' r s' s t' t =
         (if r \<le> 0 then (r', s', t')
@@ -28,17 +28,15 @@
                       s (s' - (r' div r) * s) 
                       t (t' - (r' div r) * t))"
 
-definition
-  zprime :: "int \<Rightarrow> bool" where
-  "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
+definition zprime :: "int \<Rightarrow> bool"
+  where "zprime p = (1 < p \<and> (\<forall>m. 0 <= m & m dvd p --> m = 1 \<or> m = p))"
 
-definition
-  xzgcd :: "int => int => int * int * int" where
-  "xzgcd m n = xzgcda m n m n 1 0 0 1"
+definition xzgcd :: "int => int => int * int * int"
+  where "xzgcd m n = xzgcda m n m n 1 0 0 1"
 
-definition
-  zcong :: "int => int => int => bool"  ("(1[_ = _] '(mod _'))") where
-  "[a = b] (mod m) = (m dvd (a - b))"
+definition zcong :: "int => int => int => bool"  ("(1[_ = _] '(mod _'))")
+  where "[a = b] (mod m) = (m dvd (a - b))"
+
 
 subsection {* Euclid's Algorithm and GCD *}
 
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -38,17 +38,17 @@
 
 subsection {* GCD on nat by Euclid's algorithm *}
 
-fun
-  gcd  :: "nat => nat => nat"
-where
-  "gcd m n = (if n = 0 then m else gcd n (m mod n))"
+fun gcd :: "nat => nat => nat"
+  where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
+
 lemma gcd_induct [case_names "0" rec]:
   fixes m n :: nat
   assumes "\<And>m. P m 0"
     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   shows "P m n"
 proof (induct m n rule: gcd.induct)
-  case (1 m n) with assms show ?case by (cases "n = 0") simp_all
+  case (1 m n)
+  with assms show ?case by (cases "n = 0") simp_all
 qed
 
 lemma gcd_0 [simp, algebra]: "gcd m 0 = m"
@@ -751,22 +751,22 @@
 
 lemma lcm_pos: 
   assumes mpos: "m > 0"
-  and npos: "n>0"
+    and npos: "n>0"
   shows "lcm m n > 0"
-proof(rule ccontr, simp add: lcm_def gcd_zero)
-assume h:"m*n div gcd m n = 0"
-from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
-hence gcdp: "gcd m n > 0" by simp
-with h
-have "m*n < gcd m n"
-  by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
-moreover 
-have "gcd m n dvd m" by simp
- with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
- with npos have t1:"gcd m n *n \<le> m*n" by simp
- have "gcd m n \<le> gcd m n*n" using npos by simp
- with t1 have "gcd m n \<le> m*n" by arith
-ultimately show "False" by simp
+proof (rule ccontr, simp add: lcm_def gcd_zero)
+  assume h:"m*n div gcd m n = 0"
+  from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
+  hence gcdp: "gcd m n > 0" by simp
+  with h
+  have "m*n < gcd m n"
+    by (cases "m * n < gcd m n") (auto simp add: div_if[OF gcdp, where m="m*n"])
+  moreover 
+  have "gcd m n dvd m" by simp
+  with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
+  with npos have t1:"gcd m n *n \<le> m*n" by simp
+  have "gcd m n \<le> gcd m n*n" using npos by simp
+  with t1 have "gcd m n \<le> m*n" by arith
+  ultimately show "False" by simp
 qed
 
 lemma zlcm_pos: 
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,11 +1,11 @@
-(*  Title:      HOL/Library/Pocklington.thy
+(*  Title:      HOL/Old_Number_Theory/Pocklington.thy
     Author:     Amine Chaieb
 *)
 
 header {* Pocklington's Theorem for Primes *}
 
 theory Pocklington
-imports Main Primes
+imports Primes
 begin
 
 definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Primes.thy
+(*  Title:      HOL/Old_Number_Theory/Primes.thy
     Author:     Amine Chaieb, Christophe Tabacznyj and Lawrence C Paulson
     Copyright   1996  University of Cambridge
 *)
@@ -9,13 +9,11 @@
 imports Complex_Main Legacy_GCD
 begin
 
-definition
-  coprime :: "nat => nat => bool" where
-  "coprime m n \<longleftrightarrow> gcd m n = 1"
+definition coprime :: "nat => nat => bool"
+  where "coprime m n \<longleftrightarrow> gcd m n = 1"
 
-definition
-  prime :: "nat \<Rightarrow> bool" where
-  "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+definition prime :: "nat \<Rightarrow> bool"
+  where "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
 
 lemma two_is_prime: "prime 2"
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,4 +1,5 @@
-(*  Authors:    Jeremy Avigad, David Gray, and Adam Kramer
+(*  Title:      HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
+    Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* The law of Quadratic reciprocity *}
@@ -165,33 +166,26 @@
   assumes p_neq_q:      "p \<noteq> q"
 begin
 
-definition
-  P_set :: "int set" where
-  "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
+definition P_set :: "int set"
+  where "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
 
-definition
-  Q_set :: "int set" where
-  "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
+definition Q_set :: "int set"
+  where "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
   
-definition
-  S :: "(int * int) set" where
-  "S = P_set <*> Q_set"
+definition S :: "(int * int) set"
+  where "S = P_set <*> Q_set"
 
-definition
-  S1 :: "(int * int) set" where
-  "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
+definition S1 :: "(int * int) set"
+  where "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
 
-definition
-  S2 :: "(int * int) set" where
-  "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
+definition S2 :: "(int * int) set"
+  where "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
 
-definition
-  f1 :: "int => (int * int) set" where
-  "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
+definition f1 :: "int => (int * int) set"
+  where "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
 
-definition
-  f2 :: "int => (int * int) set" where
-  "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
+definition f2 :: "int => (int * int) set"
+  where "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
 
 lemma p_fact: "0 < (p - 1) div 2"
 proof -
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/Residues.thy
--- a/src/HOL/Old_Number_Theory/Residues.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,41 +1,36 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Residues.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Residues.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* Residue Sets *}
 
-theory Residues imports Int2 begin
+theory Residues
+imports Int2
+begin
 
 text {*
   \medskip Define the residue of a set, the standard residue,
   quadratic residues, and prove some basic properties. *}
 
-definition
-  ResSet      :: "int => int set => bool" where
-  "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
+definition ResSet :: "int => int set => bool"
+  where "ResSet m X = (\<forall>y1 y2. (y1 \<in> X & y2 \<in> X & [y1 = y2] (mod m) --> y1 = y2))"
 
-definition
-  StandardRes :: "int => int => int" where
-  "StandardRes m x = x mod m"
+definition StandardRes :: "int => int => int"
+  where "StandardRes m x = x mod m"
 
-definition
-  QuadRes     :: "int => int => bool" where
-  "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
+definition QuadRes :: "int => int => bool"
+  where "QuadRes m x = (\<exists>y. ([(y ^ 2) = x] (mod m)))"
 
-definition
-  Legendre    :: "int => int => int" where
+definition Legendre :: "int => int => int" where
   "Legendre a p = (if ([a = 0] (mod p)) then 0
                      else if (QuadRes p a) then 1
                      else -1)"
 
-definition
-  SR          :: "int => int set" where
-  "SR p = {x. (0 \<le> x) & (x < p)}"
+definition SR :: "int => int set"
+  where "SR p = {x. (0 \<le> x) & (x < p)}"
 
-definition
-  SRStar      :: "int => int set" where
-  "SRStar p = {x. (0 < x) & (x < p)}"
+definition SRStar :: "int => int set"
+  where "SRStar p = {x. (0 < x) & (x < p)}"
 
 
 subsection {* Some useful properties of StandardRes *}
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/WilsonBij.thy
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/WilsonBij.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Wilson's Theorem using a more abstract approach *}
 
-theory WilsonBij imports BijectionRel IntFact begin
+theory WilsonBij
+imports BijectionRel IntFact
+begin
 
 text {*
   Wilson's Theorem using a more ``abstract'' approach based on
@@ -15,12 +18,10 @@
 
 subsection {* Definitions and lemmas *}
 
-definition
-  reciR :: "int => int => int => bool" where
-  "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
+definition reciR :: "int => int => int => bool"
+  where "reciR p = (\<lambda>a b. zcong (a * b) 1 p \<and> 1 < a \<and> a < p - 1 \<and> 1 < b \<and> b < p - 1)"
 
-definition
-  inv :: "int => int => int" where
+definition inv :: "int => int => int" where
   "inv p a =
     (if zprime p \<and> 0 < a \<and> a < p then
       (SOME x. 0 \<le> x \<and> x < p \<and> zcong (a * x) 1 p)
diff -r 17d9808ed626 -r c75e9dc841c7 src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Aug 06 12:38:02 2010 +0200
@@ -1,10 +1,13 @@
-(*  Author:     Thomas M. Rasmussen
+(*  Title:      HOL/Old_Number_Theory/WilsonRuss.thy
+    Author:     Thomas M. Rasmussen
     Copyright   2000  University of Cambridge
 *)
 
 header {* Wilson's Theorem according to Russinoff *}
 
-theory WilsonRuss imports EulerFermat begin
+theory WilsonRuss
+imports EulerFermat
+begin
 
 text {*
   Wilson's Theorem following quite closely Russinoff's approach
@@ -13,13 +16,10 @@
 
 subsection {* Definitions and lemmas *}
 
-definition
-  inv :: "int => int => int" where
-  "inv p a = (a^(nat (p - 2))) mod p"
+definition inv :: "int => int => int"
+  where "inv p a = (a^(nat (p - 2))) mod p"
 
-fun
-  wset :: "int \<Rightarrow> int => int set"
-where
+fun wset :: "int \<Rightarrow> int => int set" where
   "wset a p =
     (if 1 < a then
       let ws = wset (a - 1) p
@@ -29,7 +29,7 @@
 text {* \medskip @{term [source] inv} *}
 
 lemma inv_is_inv_aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)"
-by (subst int_int_eq [symmetric], auto)
+  by (subst int_int_eq [symmetric]) auto
 
 lemma inv_is_inv:
     "zprime p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> [a * inv p a = 1] (mod p)"
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/IsaMakefile	Fri Aug 06 12:38:02 2010 +0200
@@ -76,7 +76,7 @@
   ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
   ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
   ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
-  ML-Systems/use_context.ML Proof/extraction.ML				\
+  ML-Systems/use_context.ML Proof/extraction.ML PIDE/document.ML	\
   Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
   Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
   ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Fri Aug 06 12:38:02 2010 +0200
@@ -1,7 +1,11 @@
 (*  Title:      Pure/Isar/isar_document.ML
     Author:     Makarius
 
-Interactive Isar documents.
+Interactive Isar documents, which are structured as follows:
+
+  - history: tree of documents (i.e. changes without merge)
+  - document: graph of nodes (cf. theory files)
+  - node: linear set of commands, potentially with proof structure
 *)
 
 structure Isar_Document: sig end =
@@ -9,12 +13,6 @@
 
 (* unique identifiers *)
 
-type state_id = string;
-type command_id = string;
-type document_id = string;
-
-val no_id = "";
-
 local
   val id_count = Synchronized.var "id" 0;
 in
@@ -32,78 +30,84 @@
 
 (** documents **)
 
+datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
+type node = entry Symtab.table; (*unique command entries indexed by command_id, start with no_id*)
+type document = node Graph.T;   (*development graph via static imports*)
+
+
 (* command entries *)
 
-datatype entry = Entry of {next: command_id option, state: state_id option};
 fun make_entry next state = Entry {next = next, state = state};
 
-fun the_entry entries (id: command_id) =
-  (case Symtab.lookup entries id of
-    NONE => err_undef "document entry" id
+fun the_entry (node: node) (id: Document.command_id) =
+  (case Symtab.lookup node id of
+    NONE => err_undef "command entry" id
   | SOME (Entry entry) => entry);
 
-fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
+fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry);
 
-fun put_entry_state (id: command_id) state entries =
-  let val {next, ...} = the_entry entries id
-  in put_entry (id, make_entry next state) entries end;
+fun put_entry_state (id: Document.command_id) state (node: node) =
+  let val {next, ...} = the_entry node id
+  in put_entry (id, make_entry next state) node end;
 
 fun reset_entry_state id = put_entry_state id NONE;
 fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
 
 
-(* document *)
-
-datatype document = Document of
- {dir: Path.T,                   (*master directory*)
-  name: string,                  (*theory name*)
-  entries: entry Symtab.table};  (*unique command entries indexed by command_id, start with no_id*)
-
-fun make_document dir name entries =
-  Document {dir = dir, name = name, entries = entries};
-
-fun map_entries f (Document {dir, name, entries}) =
-  make_document dir name (f entries);
-
-
 (* iterate entries *)
 
-fun fold_entries id0 f (Document {entries, ...}) =
+fun fold_entries id0 f (node: node) =
   let
     fun apply NONE x = x
       | apply (SOME id) x =
-          let val entry = the_entry entries id
+          let val entry = the_entry node id
           in apply (#next entry) (f (id, entry) x) end;
-  in if Symtab.defined entries id0 then apply (SOME id0) else I end;
+  in if Symtab.defined node id0 then apply (SOME id0) else I end;
 
-fun first_entry P (Document {entries, ...}) =
+fun first_entry P (node: node) =
   let
     fun first _ NONE = NONE
       | first prev (SOME id) =
-          let val entry = the_entry entries id
+          let val entry = the_entry node id
           in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
-  in first NONE (SOME no_id) end;
+  in first NONE (SOME Document.no_id) end;
 
 
 (* modify entries *)
 
-fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>
-  let val {next, state} = the_entry entries id in
-    entries
+fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
+  let val {next, state} = the_entry node id in
+    node
     |> put_entry (id, make_entry (SOME id2) state)
     |> put_entry (id2, make_entry next NONE)
-  end);
+  end;
 
-fun delete_after (id: command_id) = map_entries (fn entries =>
-  let val {next, state} = the_entry entries id in
+fun delete_after (id: Document.command_id) (node: node) =
+  let val {next, state} = the_entry node id in
     (case next of
       NONE => error ("No next entry to delete: " ^ quote id)
     | SOME id2 =>
-        entries |>
-          (case #next (the_entry entries id2) of
+        node |>
+          (case #next (the_entry node id2) of
             NONE => put_entry (id, make_entry NONE state)
           | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
-  end);
+  end;
+
+
+(* node operations *)
+
+val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
+
+fun the_node (document: document) name =
+  Graph.get_node document name handle Graph.UNDEF _ => empty_node;
+
+fun edit_node (id, SOME id2) = insert_after id id2
+  | edit_node (id, NONE) = delete_after id;
+
+fun edit_nodes (name, SOME edits) =
+      Graph.default_node (name, empty_node) #>
+      Graph.map_node name (fold edit_node edits)
+  | edit_nodes (name, NONE) = Graph.del_node name;
 
 
 
@@ -113,16 +117,17 @@
 
 local
 
-val global_states = Unsynchronized.ref (Symtab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))]);
+val global_states =
+  Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
 
 in
 
-fun define_state (id: state_id) state =
+fun define_state (id: Document.state_id) state =
   NAMED_CRITICAL "Isar" (fn () =>
     Unsynchronized.change global_states (Symtab.update_new (id, state))
       handle Symtab.DUP dup => err_dup "state" dup);
 
-fun the_state (id: state_id) =
+fun the_state (id: Document.state_id) =
   (case Symtab.lookup (! global_states) id of
     NONE => err_undef "state" id
   | SOME state => state);
@@ -134,16 +139,16 @@
 
 local
 
-val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
+val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]);
 
 in
 
-fun define_command (id: command_id) tr =
+fun define_command (id: Document.command_id) tr =
   NAMED_CRITICAL "Isar" (fn () =>
     Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
       handle Symtab.DUP dup => err_dup "command" dup);
 
-fun the_command (id: command_id) =
+fun the_command (id: Document.command_id) =
   (case Symtab.lookup (! global_commands) id of
     NONE => err_undef "command" id
   | SOME tr => tr);
@@ -151,20 +156,20 @@
 end;
 
 
-(* documents *)
+(* document versions *)
 
 local
 
-val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
+val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]);
 
 in
 
-fun define_document (id: document_id) document =
+fun define_document (id: Document.version_id) document =
   NAMED_CRITICAL "Isar" (fn () =>
     Unsynchronized.change global_documents (Symtab.update_new (id, document))
       handle Symtab.DUP dup => err_dup "document" dup);
 
-fun the_document (id: document_id) =
+fun the_document (id: Document.version_id) =
   (case Symtab.lookup (! global_documents) id of
     NONE => err_undef "document" id
   | SOME document => document);
@@ -175,41 +180,47 @@
 
 (** main operations **)
 
-(* begin/end document *)
-
-val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))];
-
-fun begin_document (id: document_id) path =
-  let
-    val (dir, name) = Thy_Header.split_thy_path path;
-    val _ = define_document id (make_document dir name no_entries);
-  in () end;
-
-fun end_document (id: document_id) =
-  NAMED_CRITICAL "Isar" (fn () =>
-    let
-      val document as Document {name, ...} = the_document id;
-      val end_state =
-        the_state (the (#state (#3 (the
-          (first_entry (fn (_, {next, ...}) => is_none next) document)))));
-      val _ =  (* FIXME regular execution (??), result (??) *)
-        Future.fork (fn () =>
-          (case Lazy.force end_state of
-            SOME st => Toplevel.end_theory (Position.id_only id) st
-          | NONE => error ("Failed to finish theory " ^ quote name)));
-    in () end);
-
-
-(* document editing *)
+(* execution *)
 
 local
 
-fun is_changed entries' (id, {next = _, state}) =
-  (case try (the_entry entries') id of
+val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
+
+fun force_state NONE = ()
+  | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
+
+in
+
+fun execute document =
+  NAMED_CRITICAL "Isar" (fn () =>
+    let
+      val old_execution = ! execution;
+      val _ = List.app Future.cancel old_execution;
+      fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
+      (* FIXME proper node deps *)
+      val new_execution = Graph.keys document |> map (fn name =>
+        Future.fork_pri 1 (fn () =>
+          let
+            val _ = await_cancellation ();
+            val exec =
+              fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state)
+                (the_node document name);
+          in exec () end));
+    in execution := new_execution end);
+
+end;
+
+
+(* editing *)
+
+local
+
+fun is_changed node' (id, {next = _, state}) =
+  (case try (the_entry node') id of
     NONE => true
   | SOME {next = _, state = state'} => state' <> state);
 
-fun new_state name (id: command_id) (state_id, updates) =
+fun new_state name (id: Document.command_id) (state_id, updates) =
   let
     val state = the_state state_id;
     val state_id' = create_id ();
@@ -227,44 +238,31 @@
   |> Markup.markup Markup.assign
   |> Output.status;
 
-
-fun force_state NONE = ()
-  | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
-
-val execution = Unsynchronized.ref (Future.value ());
-
-fun execute document =
-  NAMED_CRITICAL "Isar" (fn () =>
-    let
-      val old_execution = ! execution;
-      val _ = Future.cancel old_execution;
-      val new_execution = Future.fork_pri 1 (fn () =>
-       (uninterruptible (K Future.join_result) old_execution;
-        fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));
-    in execution := new_execution end);
-
 in
 
-fun edit_document (old_id: document_id) (new_id: document_id) edits =
+fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
   NAMED_CRITICAL "Isar" (fn () =>
     let
-      val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
-      val new_document as Document {entries = new_entries, ...} = old_document
-        |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
+      val old_document = the_document old_id;
+      val new_document = fold edit_nodes edits old_document;
 
-      val (updates, new_document') =
-        (case first_entry (is_changed old_entries) new_document of
-          NONE => ([], new_document)
+      fun update_node name node =
+        (case first_entry (is_changed (the_node old_document name)) node of
+          NONE => ([], node)
         | SOME (prev, id, _) =>
             let
-              val prev_state_id = the (#state (the_entry new_entries (the prev)));
-              val (_, updates) =
-                fold_entries id (new_state name o #1) new_document (prev_state_id, []);
-              val new_document' = new_document |> map_entries (fold set_entry_state updates);
-            in (rev updates, new_document') end);
+              val prev_state_id = the (#state (the_entry node (the prev)));
+              val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
+              val node' = fold set_entry_state updates node;
+            in (rev updates, node') end);
+
+      (* FIXME proper node deps *)
+      val (updatess, new_document') =
+        (Graph.keys new_document, new_document)
+          |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
 
       val _ = define_document new_id new_document';
-      val _ = report_updates updates;
+      val _ = report_updates (flat updatess);
       val _ = execute new_document';
     in () end);
 
@@ -282,21 +280,13 @@
         define_command id (Outer_Syntax.prepare_command (Position.id id) text))));
 
 val _ =
-  Outer_Syntax.internal_command "Isar.begin_document"
-    (Parse.string -- Parse.string >> (fn (id, path) =>
-      Toplevel.imperative (fn () => begin_document id (Path.explode path))));
-
-val _ =
-  Outer_Syntax.internal_command "Isar.end_document"
-    (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
-
-val _ =
   Outer_Syntax.internal_command "Isar.edit_document"
     (Parse.string -- Parse.string --
-        Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
-      >> (fn ((id, new_id), edits) =>
-        Toplevel.position (Position.id_only new_id) o
-        Toplevel.imperative (fn () => edit_document id new_id edits)));
+      Parse_Value.list
+        (Parse.string -- Scan.option (Parse_Value.list (Parse.string -- Scan.option Parse.string)))
+      >> (fn ((old_id, new_id), edits) =>
+          Toplevel.position (Position.id_only new_id) o
+          Toplevel.imperative (fn () => edit_document old_id new_id edits)));
 
 end;
 
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -9,13 +9,6 @@
 
 object Isar_Document
 {
-  /* unique identifiers */
-
-  type State_ID = String
-  type Command_ID = String
-  type Document_ID = String
-
-
   /* reports */
 
   object Assign {
@@ -27,7 +20,7 @@
   }
 
   object Edit {
-    def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] =
+    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
       msg match {
         case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
           Some(cmd_id, state_id)
@@ -44,7 +37,7 @@
 
   /* commands */
 
-  def define_command(id: Command_ID, text: String) {
+  def define_command(id: Document.Command_ID, text: String) {
     output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
       Isabelle_Syntax.encode_string(text))
   }
@@ -52,36 +45,41 @@
 
   /* documents */
 
-  def begin_document(id: Document_ID, path: String) {
-    output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
-      Isabelle_Syntax.encode_string(path))
-  }
-
-  def end_document(id: Document_ID) {
-    output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
-  }
-
-  def edit_document(old_id: Document_ID, new_id: Document_ID,
-      edits: List[(Command_ID, Option[Command_ID])])
+  def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
+      edits: List[Document.Edit[Document.Command_ID]])
   {
-    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
+    def append_edit(
+        edit: (Option[Document.Command_ID], Option[Document.Command_ID]), result: StringBuilder)
     {
-      edit match {
-        case (id, None) => Isabelle_Syntax.append_string(id, result)
-        case (id, Some(id2)) =>
-          Isabelle_Syntax.append_string(id, result)
+      Isabelle_Syntax.append_string(edit._1 getOrElse Document.NO_ID, result)
+      edit._2 match {
+        case None =>
+        case Some(id2) =>
           result.append(" ")
           Isabelle_Syntax.append_string(id2, result)
       }
     }
 
+    def append_node_edit(
+        edit: (String, Option[List[(Option[Document.Command_ID], Option[Document.Command_ID])]]),
+        result: StringBuilder)
+    {
+      Isabelle_Syntax.append_string(edit._1, result)
+      edit._2 match {
+        case None =>
+        case Some(eds) =>
+          result.append(" ")
+          Isabelle_Syntax.append_list(append_edit, eds, result)
+      }
+    }
+
     val buf = new StringBuilder(40)
     buf.append("Isar.edit_document ")
     Isabelle_Syntax.append_string(old_id, buf)
     buf.append(" ")
     Isabelle_Syntax.append_string(new_id, buf)
     buf.append(" ")
-    Isabelle_Syntax.append_list(append_edit, edits, buf)
+    Isabelle_Syntax.append_list(append_node_edit, edits, buf)
     output_sync(buf.toString)
   }
 }
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/PIDE/change.scala
--- a/src/Pure/PIDE/change.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/PIDE/change.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -2,18 +2,34 @@
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
-Changes of plain text.
+Changes of plain text, resulting in document edits.
 */
 
 package isabelle
 
 
+object Change
+{
+  val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init))
+
+  abstract class Snapshot
+  {
+    val document: Document
+    val node: Document.Node
+    val is_outdated: Boolean
+    def convert(offset: Int): Int
+    def revert(offset: Int): Int
+  }
+}
+
 class Change(
-  val id: Isar_Document.Document_ID,
+  val id: Document.Version_ID,
   val parent: Option[Change],
-  val edits: List[Text_Edit],
-  val result: Future[(List[Document.Edit], Document)])
+  val edits: List[Document.Node_Text_Edit],
+  val result: Future[(List[Document.Edit[Command]], Document)])
 {
+  /* ancestor versions */
+
   def ancestors: Iterator[Change] = new Iterator[Change]
   {
     private var state: Option[Change] = Some(Change.this)
@@ -25,13 +41,13 @@
       }
   }
 
-  def join_document: Document = result.join._2
-  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
 
-  def edit(session: Session, edits: List[Text_Edit]): Change =
+  /* editing and state assignment */
+
+  def edit(session: Session, edits: List[Document.Node_Text_Edit]): Change =
   {
     val new_id = session.create_id()
-    val result: Future[(List[Document.Edit], Document)] =
+    val result: Future[(List[Document.Edit[Command]], Document)] =
       Future.fork {
         val old_doc = join_document
         old_doc.await_assignment
@@ -39,4 +55,30 @@
       }
     new Change(new_id, Some(this), edits, result)
   }
+
+  def join_document: Document = result.join._2
+  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
+
+
+  /* snapshot */
+
+  def snapshot(name: String, extra_edits: List[Text_Edit]): Change.Snapshot =
+  {
+    val latest = this
+    val stable = latest.ancestors.find(_.is_assigned)
+    require(stable.isDefined)
+
+    val edits =
+      (extra_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
+          (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+    lazy val reverse_edits = edits.reverse
+
+    new Change.Snapshot {
+      val document = stable.get.join_document
+      val node = document.nodes(name)
+      val is_outdated = !(extra_edits.isEmpty && latest == stable.get)
+      def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
+      def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+    }
+  }
 }
\ No newline at end of file
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -35,7 +35,7 @@
 }
 
 class Command(
-    val id: Isar_Document.Command_ID,
+    val id: Document.Command_ID,
     val span: Thy_Syntax.Span,
     val static_parent: Option[Command] = None)
   extends Session.Entity
@@ -91,7 +91,7 @@
     accumulator ! Consume(message, forward)
   }
 
-  def assign_state(state_id: Isar_Document.State_ID): Command =
+  def assign_state(state_id: Document.State_ID): Command =
   {
     val cmd = new Command(state_id, span, Some(this))
     accumulator !? Assign
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/PIDE/document.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document.ML	Fri Aug 06 12:38:02 2010 +0200
@@ -0,0 +1,36 @@
+(*  Title:      Pure/PIDE/document.ML
+    Author:     Makarius
+
+Document as collection of named nodes, each consisting of an editable
+list of commands.
+*)
+
+signature DOCUMENT =
+sig
+  type state_id = string
+  type command_id = string
+  type version_id = string
+  val no_id: string
+  type edit = string * ((command_id * command_id option) list) option
+end;
+
+structure Document: DOCUMENT =
+struct
+
+(* unique identifiers *)
+
+type state_id = string;
+type command_id = string;
+type version_id = string;
+
+val no_id = "";
+
+
+(* edits *)
+
+type edit =
+  string *  (*node name*)
+  ((command_id * command_id option) list) option;  (*NONE: remove, SOME: insert/remove commands*)
+
+end;
+
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -1,17 +1,28 @@
 /*  Title:      Pure/PIDE/document.scala
     Author:     Makarius
 
-Document as editable list of commands.
+Document as collection of named nodes, each consisting of an editable
+list of commands.
 */
 
 package isabelle
 
 
+import scala.collection.mutable
 import scala.annotation.tailrec
 
 
 object Document
 {
+  /* unique identifiers */
+
+  type State_ID = String
+  type Command_ID = String
+  type Version_ID = String
+
+  val NO_ID = ""
+
+
   /* command start positions */
 
   def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
@@ -25,23 +36,65 @@
   }
 
 
-  /* empty document */
+  /* named document nodes */
+
+  object Node
+  {
+    val empty: Node = new Node(Linear_Set())
+  }
+
+  class Node(val commands: Linear_Set[Command])
+  {
+    /* command ranges */
+
+    def command_starts: Iterator[(Command, Int)] =
+      Document.command_starts(commands.iterator)
+
+    def command_start(cmd: Command): Option[Int] =
+      command_starts.find(_._1 == cmd).map(_._2)
+
+    def command_range(i: Int): Iterator[(Command, Int)] =
+      command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
 
-  def empty(id: Isar_Document.Document_ID): Document =
+    def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
+      command_range(i) takeWhile { case (_, start) => start < j }
+
+    def command_at(i: Int): Option[(Command, Int)] =
+    {
+      val range = command_range(i)
+      if (range.hasNext) Some(range.next) else None
+    }
+
+    def proper_command_at(i: Int): Option[Command] =
+      command_at(i) match {
+        case Some((command, _)) =>
+          commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
+        case None => None
+      }
+  }
+
+
+  /* initial document */
+
+  val init: Document =
   {
-    val doc = new Document(id, Linear_Set(), Map())
+    val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
     doc.assign_states(Nil)
     doc
   }
 
 
 
-  /** document edits **/
+  /** editing **/
+
+  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
 
-  type Edit = (Option[Command], Option[Command])
+  type Edit[C] =
+   (String,  // node name
+    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
 
-  def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
-    edits: List[Text_Edit]): (List[Edit], Document) =
+  def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
+      edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
   {
     require(old_doc.assignment.is_finished)
 
@@ -56,7 +109,8 @@
 
     /* phase 1: edit individual command source */
 
-    def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
+    @tailrec def edit_text(eds: List[Text_Edit],
+        commands: Linear_Set[Command]): Linear_Set[Command] =
     {
       eds match {
         case e :: es =>
@@ -120,55 +174,38 @@
 
     /* phase 3: resulting document edits */
 
-    val commands0 = old_doc.commands
-    val commands1 = edit_text(edits, commands0)
-    val commands2 = parse_spans(commands1)
+    {
+      val doc_edits = new mutable.ListBuffer[Edit[Command]]
+      var nodes = old_doc.nodes
+      var former_states = old_doc.assignment.join
 
-    val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
-    val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
+      for ((name, text_edits) <- edits) {
+        val commands0 = nodes(name).commands
+        val commands1 = edit_text(text_edits, commands0)
+        val commands2 = parse_spans(commands1)
 
-    val doc_edits =
-      removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
-      inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
+        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
+        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
+
+        val cmd_edits =
+          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
+          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
-    val former_states = old_doc.assignment.join -- removed_commands
-
-    (doc_edits, new Document(new_id, commands2, former_states))
+        doc_edits += (name -> Some(cmd_edits))
+        nodes += (name -> new Node(commands2))
+        former_states --= removed_commands
+      }
+      (doc_edits.toList, new Document(new_id, nodes, former_states))
+    }
   }
 }
 
 
 class Document(
-    val id: Isar_Document.Document_ID,
-    val commands: Linear_Set[Command],
-    former_states: Map[Command, Command])
+    val id: Document.Version_ID,
+    val nodes: Map[String, Document.Node],
+    former_states: Map[Command, Command])  // FIXME !?
 {
-  /* command ranges */
-
-  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands.iterator)
-
-  def command_start(cmd: Command): Option[Int] =
-    command_starts.find(_._1 == cmd).map(_._2)
-
-  def command_range(i: Int): Iterator[(Command, Int)] =
-    command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
-
-  def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
-    command_range(i) takeWhile { case (_, start) => start < j }
-
-  def command_at(i: Int): Option[(Command, Int)] =
-  {
-    val range = command_range(i)
-    if (range.hasNext) Some(range.next) else None
-  }
-
-  def proper_command_at(i: Int): Option[Command] =
-    command_at(i) match {
-      case Some((command, _)) => commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
-      case None => None
-    }
-
-
   /* command state assignment */
 
   val assignment = Future.promise[Map[Command, Command]]
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/PIDE/text_edit.scala
--- a/src/Pure/PIDE/text_edit.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/PIDE/text_edit.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -21,8 +21,8 @@
     else if (is_insert == do_insert) offset + text.length
     else (offset - text.length) max start
 
-  def after(offset: Int): Int = transform(true, offset)
-  def before(offset: Int): Int = transform(false, offset)
+  def convert(offset: Int): Int = transform(true, offset)
+  def revert(offset: Int): Int = transform(false, offset)
 
 
   /* edit strings */
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/ROOT.ML	Fri Aug 06 12:38:02 2010 +0200
@@ -234,6 +234,7 @@
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
 use "Thy/thy_syntax.ML";
+use "PIDE/document.ML";
 use "old_goals.ML";
 use "Isar/outer_syntax.ML";
 use "Thy/thy_info.ML";
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -76,7 +76,6 @@
 
   private case class Start(timeout: Int, args: List[String])
   private case object Stop
-  private case class Begin_Document(path: String)
 
   private lazy val session_actor = actor {
 
@@ -84,8 +83,9 @@
 
     def register(entity: Session.Entity) { entities += (entity.id -> entity) }
 
-    var documents = Map[Isar_Document.Document_ID, Document]()
+    var documents = Map[Document.Version_ID, Document]()
     def register_document(doc: Document) { documents += (doc.id -> doc) }
+    register_document(Document.init)
 
 
     /* document changes */
@@ -94,22 +94,31 @@
     {
       require(change.parent.isDefined)
 
-      val (changes, doc) = change.result.join
-      val id_changes = changes map {
-        case (c1, c2) =>
-          (c1.map(_.id).getOrElse(""),
-           c2 match {
-              case None => None
-              case Some(command) =>
-                if (!lookup_command(command.id).isDefined) {
-                  register(command)
-                  prover.define_command(command.id, system.symbols.encode(command.source))
-                }
-                Some(command.id)
-            })
-      }
+      val (node_edits, doc) = change.result.join
+      val id_edits =
+        node_edits map {
+          case (name, None) => (name, None)
+          case (name, Some(cmd_edits)) =>
+            val chs =
+              cmd_edits map {
+                case (c1, c2) =>
+                  val id1 = c1.map(_.id)
+                  val id2 =
+                    c2 match {
+                      case None => None
+                      case Some(command) =>
+                        if (!lookup_command(command.id).isDefined) {
+                          register(command)
+                          prover.define_command(command.id, system.symbols.encode(command.source))
+                        }
+                        Some(command.id)
+                    }
+                  (id1, id2)
+              }
+            (name -> Some(chs))
+        }
       register_document(doc)
-      prover.edit_document(change.parent.get.id, doc.id, id_changes)
+      prover.edit_document(change.parent.get.id, doc.id, id_edits)
     }
 
 
@@ -229,13 +238,6 @@
             prover = null
           }
 
-        case Begin_Document(path: String) if prover != null =>
-          val id = create_id()
-          val doc = Document.empty(id)
-          register_document(doc)
-          prover.begin_document(id, path)
-          reply(doc)
-
         case change: Change if prover != null =>
           handle_change(change)
 
@@ -304,7 +306,4 @@
 
   def stop() { session_actor ! Stop }
   def input(change: Change) { session_actor ! change }
-
-  def begin_document(path: String): Document =
-    (session_actor !? Begin_Document(path)).asInstanceOf[Document]
 }
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML	Fri Aug 06 12:38:02 2010 +0200
@@ -68,14 +68,14 @@
   end;
 
 
-(* file formats *)
+(* file name *)
 
 val thy_path = Path.ext "thy" o Path.basic;
 
 fun split_thy_path path =
   (case Path.split_ext path of
     (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
-  | _ => error ("Bad theory file specification " ^ Path.implode path));
+  | _ => error ("Bad theory file specification: " ^ Path.implode path));
 
 fun consistent_name name name' =
   if name = name' then ()
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -9,6 +9,7 @@
 
 import scala.collection.mutable
 import scala.util.parsing.input.{Reader, CharSequenceReader}
+import scala.util.matching.Regex
 
 import java.io.File
 
@@ -24,6 +25,19 @@
   val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
   final case class Header(val name: String, val imports: List[String], val uses: List[String])
+
+
+  /* file name */
+
+  val Thy_Path1 = new Regex("([^/]*)\\.thy")
+  val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy")
+
+  def split_thy_path(path: String): (String, String) =
+    path match {
+      case Thy_Path1(name) => ("", name)
+      case Thy_Path2(dir, name) => (dir, name)
+      case _ => error("Bad theory file specification: " + path)
+    }
 }
 
 
diff -r 17d9808ed626 -r c75e9dc841c7 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Aug 06 12:38:02 2010 +0200
@@ -17,6 +17,7 @@
   val loaded_files: string -> Path.T list
   val remove_thy: string -> unit
   val kill_thy: string -> unit
+  val use_thys_wrt: Path.T -> string list -> unit
   val use_thys: string list -> unit
   val use_thy: string -> unit
   val toplevel_begin_theory: string -> string list -> (Path.T * bool) list -> theory
@@ -34,7 +35,7 @@
 local
   val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
 in
-  fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
+  fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f));
   fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
 end;
 
@@ -64,9 +65,9 @@
 
 type deps =
  {master: (Path.T * File.ident),  (*master dependencies for thy file*)
-  parents: string list};          (*source specification of parents (partially qualified)*)
+  imports: string list};          (*source specification of imports (partially qualified)*)
 
-fun make_deps master parents : deps = {master = master, parents = parents};
+fun make_deps master imports : deps = {master = master, imports = imports};
 
 fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 fun base_name s = Path.implode (Path.base (Path.explode s));
@@ -75,7 +76,7 @@
   val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
 in
   fun get_thys () = ! database;
-  fun change_thys f = CRITICAL (fn () => Unsynchronized.change database f);
+  fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f);
 end;
 
 
@@ -116,7 +117,7 @@
 
 fun lookup_theory name =
   (case lookup_thy name of
-    SOME (_, SOME thy) => SOME thy
+    SOME (_, SOME theory) => SOME theory
   | _ => NONE);
 
 fun get_theory name =
@@ -124,41 +125,30 @@
     SOME theory => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
-fun loaded_files name =
+fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   (case get_deps name of
     NONE => []
-  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name));
+  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));
 
 
 
 (** thy operations **)
 
-(* abstract update time *)
-
-structure Update_Time = Theory_Data
-(
-  type T = int;
-  val empty = 0;
-  fun extend _ = empty;
-  fun merge _ = empty;
-);
-
-
 (* remove theory *)
 
-fun remove_thy name =
+fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
   if is_finished name then error (loader_msg "attempt to change finished theory" [name])
   else
     let
       val succs = thy_graph Graph.all_succs [name];
       val _ = priority (loader_msg "removing" succs);
-      val _ = CRITICAL (fn () =>
-        (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)));
-    in () end;
+      val _ = List.app (perform Remove) succs;
+      val _ = change_thys (Graph.del_nodes succs);
+    in () end);
 
-fun kill_thy name =
+fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
   if known_thy name then remove_thy name
-  else ();
+  else ());
 
 
 (* scheduling loader tasks *)
@@ -185,8 +175,6 @@
 fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
   let
     val tasks = Graph.topological_order task_graph;
-    val par_proofs = ! parallel_proofs >= 1;
-
     val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
       (case Graph.get_node task_graph name of
         Task (parents, body) =>
@@ -200,12 +188,8 @@
                 [] => body (map (#1 o Future.join o get) parents)
               | bad => error (loader_msg
                   ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
-            val future' =
-              if par_proofs then future
-              else Future.map (fn (thy, after_load) => (after_load (); (thy, I))) future;
-          in Symtab.update (name, future') tab end
+          in Symtab.update (name, future) tab end
       | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
-
     val _ =
       tasks |> maps (fn name =>
         let
@@ -246,17 +230,17 @@
     val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
     fun init () =
       Thy_Load.begin_theory dir name parent_thys uses
-      |> Present.begin_theory update_time dir uses
-      |> Update_Time.put update_time;
+      |> Present.begin_theory update_time dir uses;
 
     val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
 
-    val parent_names = map Context.theory_name parent_thys;
+    val parents = map Context.theory_name parent_thys;
     fun after_load' () =
      (after_load ();
-      CRITICAL (fn () =>
-        (change_thys (new_entry name parent_names (SOME deps, SOME theory));
-          perform Update name)));
+      NAMED_CRITICAL "Thy_Info" (fn () =>
+       (map get_theory parents;
+        change_thys (new_entry name parents (SOME deps, SOME theory));
+        perform Update name)));
 
   in (theory, after_load') end;
 
@@ -264,21 +248,21 @@
   (case lookup_deps name of
     SOME NONE => (true, NONE, get_parents name, NONE)
   | NONE =>
-      let val {master, text, imports = parents, ...} = Thy_Load.deps_thy dir name
-      in (false, SOME (make_deps master parents), parents, SOME text) end
-  | SOME (SOME {master, parents}) =>
+      let val {master, text, imports, ...} = Thy_Load.deps_thy dir name
+      in (false, SOME (make_deps master imports), imports, SOME text) end
+  | SOME (SOME {master, imports}) =>
       let val master' = Thy_Load.check_thy dir name in
         if #2 master <> #2 master' then
-          let val {text = text', imports = parents', ...} = Thy_Load.deps_thy dir name;
-          in (false, SOME (make_deps master' parents'), parents', SOME text') end
+          let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name;
+          in (false, SOME (make_deps master' imports'), imports', SOME text') end
         else
           let
             val current =
               (case lookup_theory name of
                 NONE => false
               | SOME theory => Thy_Load.all_current theory);
-            val deps' = SOME (make_deps master' parents);
-          in (current, deps', parents, NONE) end
+            val deps' = SOME (make_deps master' imports);
+          in (current, deps', imports, NONE) end
       end);
 
 in
@@ -296,14 +280,14 @@
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
-          val (current, deps, parents, opt_text) = check_deps dir' name
+          val (current, deps, imports, opt_text) = check_deps dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
                 required_by "\n" initiators);
 
-          val parent_names = map base_name parents;
+          val parents = map base_name imports;
           val (parents_current, tasks') =
-            require_thys (name :: initiators) (Path.append dir (master_dir deps)) parents tasks;
+            require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
@@ -315,8 +299,8 @@
                   let
                     val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
                     val update_time = serial ();
-                  in Task (parent_names, load_thy initiators update_time dep text name) end);
-        in (all_current, new_entry name parent_names task tasks') end)
+                  in Task (parents, load_thy initiators update_time dep text name) end);
+        in (all_current, new_entry name parents task tasks') end)
   end;
 
 end;
@@ -324,10 +308,10 @@
 
 (* use_thy *)
 
-fun use_thys_dir dir arg =
+fun use_thys_wrt dir arg =
   schedule_tasks (snd (require_thys [] dir arg Graph.empty));
 
-val use_thys = use_thys_dir Path.current;
+val use_thys = use_thys_wrt Path.current;
 val use_thy = use_thys o single;
 
 
@@ -337,9 +321,9 @@
   let
     val dir = Thy_Load.get_master_path ();
     val _ = kill_thy name;
-    val _ = use_thys_dir dir imports;
-    val parents = map (get_theory o base_name) imports;
-  in Thy_Load.begin_theory dir name parents uses end;
+    val _ = use_thys_wrt dir imports;
+    val parent_thys = map (get_theory o base_name) imports;
+  in Thy_Load.begin_theory dir name parent_thys uses end;
 
 
 (* register theory *)
@@ -347,15 +331,14 @@
 fun register_thy theory =
   let
     val name = Context.theory_name theory;
-    val _ = kill_thy name;
-    val _ = priority ("Registering theory " ^ quote name);
-
     val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
     val parents = map Context.theory_name (Theory.parents_of theory);
     val deps = make_deps master parents;
   in
-    CRITICAL (fn () =>
-     (map get_theory parents;
+    NAMED_CRITICAL "Thy_Info" (fn () =>
+     (kill_thy name;
+      priority ("Registering theory " ^ quote name);
+      map get_theory parents;
       change_thys (new_entry name parents (SOME deps, SOME theory));
       perform Update name))
   end;
diff -r 17d9808ed626 -r c75e9dc841c7 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD	Fri Aug 06 12:38:02 2010 +0200
@@ -5,13 +5,13 @@
 * Proper Java JRE/JDK from Sun, e.g. 1.6.0_21
   http://java.sun.com/javase/downloads/index.jsp
 
-* Netbeans 6.8
+* Netbeans 6.9
   http://www.netbeans.org/downloads/index.html
 
-* Scala for Netbeans: version 6.8v1.1.0rc2
+* Scala for Netbeans: version 6.9v1.1.0
   http://wiki.netbeans.org/Scala
-  http://sourceforge.net/projects/erlybird/files/nb-scala/6.8v1.1.0rc2
-  http://blogtrader.net/dcaoyuan/category/NetBeans
+  http://wiki.netbeans.org/Scala68v1
+  http://sourceforge.net/projects/erlybird/files/nb-scala/6.9v1.1.0
 
 * jEdit 4.3.2
   http://www.jedit.org/
diff -r 17d9808ed626 -r c75e9dc841c7 src/Tools/jEdit/dist-template/etc/settings
--- a/src/Tools/jEdit/dist-template/etc/settings	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/settings	Fri Aug 06 12:38:02 2010 +0200
@@ -1,3 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
 JEDIT_HOME="$COMPONENT"
 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
 
diff -r 17d9808ed626 -r c75e9dc841c7 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -15,11 +15,136 @@
 
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
-import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
+import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
+import org.gjt.sp.jedit.textarea.TextArea
+
+import java.awt.font.TextAttribute
+import javax.swing.text.Segment;
 
 
 object Document_Model
 {
+  object Token_Markup
+  {
+    /* extended token styles */
+
+    private val plain_range: Int = Token.ID_COUNT
+    private val full_range: Int = 3 * plain_range
+    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
+
+    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
+    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
+
+    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
+    {
+      import scala.collection.JavaConversions._
+      val script_font =
+        style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
+      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
+    }
+
+    def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
+    {
+      val new_styles = new Array[SyntaxStyle](full_range)
+      for (i <- 0 until plain_range) {
+        val style = styles(i)
+        new_styles(i) = style
+        new_styles(subscript(i.toByte)) = script_style(style, -1)
+        new_styles(superscript(i.toByte)) = script_style(style, 1)
+      }
+      new_styles
+    }
+
+
+    /* line context */
+
+    private val rule_set = new ParserRuleSet("isabelle", "MAIN")
+    class LineContext(val line: Int, prev: LineContext)
+      extends TokenMarker.LineContext(rule_set, prev)
+
+
+    /* mapping to jEdit token types */
+    // TODO: as properties or CSS style sheet
+
+    val command_style: Map[String, Byte] =
+    {
+      import Token._
+      Map[String, Byte](
+        Keyword.THY_END -> KEYWORD2,
+        Keyword.THY_SCRIPT -> LABEL,
+        Keyword.PRF_SCRIPT -> LABEL,
+        Keyword.PRF_ASM -> KEYWORD3,
+        Keyword.PRF_ASM_GOAL -> KEYWORD3
+      ).withDefaultValue(KEYWORD1)
+    }
+
+    val token_style: Map[String, Byte] =
+    {
+      import Token._
+      Map[String, Byte](
+        // logical entities
+        Markup.TCLASS -> NULL,
+        Markup.TYCON -> NULL,
+        Markup.FIXED_DECL -> FUNCTION,
+        Markup.FIXED -> NULL,
+        Markup.CONST_DECL -> FUNCTION,
+        Markup.CONST -> NULL,
+        Markup.FACT_DECL -> FUNCTION,
+        Markup.FACT -> NULL,
+        Markup.DYNAMIC_FACT -> LABEL,
+        Markup.LOCAL_FACT_DECL -> FUNCTION,
+        Markup.LOCAL_FACT -> NULL,
+        // inner syntax
+        Markup.TFREE -> NULL,
+        Markup.FREE -> NULL,
+        Markup.TVAR -> NULL,
+        Markup.SKOLEM -> NULL,
+        Markup.BOUND -> NULL,
+        Markup.VAR -> NULL,
+        Markup.NUM -> DIGIT,
+        Markup.FLOAT -> DIGIT,
+        Markup.XNUM -> DIGIT,
+        Markup.XSTR -> LITERAL4,
+        Markup.LITERAL -> OPERATOR,
+        Markup.INNER_COMMENT -> COMMENT1,
+        Markup.SORT -> NULL,
+        Markup.TYP -> NULL,
+        Markup.TERM -> NULL,
+        Markup.PROP -> NULL,
+        Markup.ATTRIBUTE -> NULL,
+        Markup.METHOD -> NULL,
+        // ML syntax
+        Markup.ML_KEYWORD -> KEYWORD1,
+        Markup.ML_DELIMITER -> OPERATOR,
+        Markup.ML_IDENT -> NULL,
+        Markup.ML_TVAR -> NULL,
+        Markup.ML_NUMERAL -> DIGIT,
+        Markup.ML_CHAR -> LITERAL1,
+        Markup.ML_STRING -> LITERAL1,
+        Markup.ML_COMMENT -> COMMENT1,
+        Markup.ML_MALFORMED -> INVALID,
+        // embedded source text
+        Markup.ML_SOURCE -> COMMENT3,
+        Markup.DOC_SOURCE -> COMMENT3,
+        Markup.ANTIQ -> COMMENT4,
+        Markup.ML_ANTIQ -> COMMENT4,
+        Markup.DOC_ANTIQ -> COMMENT4,
+        // outer syntax
+        Markup.KEYWORD -> KEYWORD2,
+        Markup.OPERATOR -> OPERATOR,
+        Markup.COMMAND -> KEYWORD1,
+        Markup.IDENT -> NULL,
+        Markup.VERBATIM -> COMMENT3,
+        Markup.COMMENT -> COMMENT1,
+        Markup.CONTROL -> COMMENT3,
+        Markup.MALFORMED -> INVALID,
+        Markup.STRING -> LITERAL3,
+        Markup.ALTSTRING -> LITERAL1
+      ).withDefaultValue(NULL)
+    }
+  }
+
+
   /* document model of buffer */
 
   private val key = "isabelle.document_model"
@@ -54,6 +179,7 @@
   }
 }
 
+
 class Document_Model(val session: Session, val buffer: Buffer)
 {
   /* visible line end */
@@ -69,40 +195,28 @@
   }
 
 
-  /* history */
-
-  private val document_0 = session.begin_document(buffer.getName)
+  /* global state -- owned by Swing thread */
 
-  @volatile private var history =  // owned by Swing thread
-    new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
-
-  def current_change(): Change = history
-  def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
+  @volatile private var history = Change.init // owned by Swing thread
+  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
 
 
-  /* transforming offsets */
+  /* snapshot */
+
+  // FIXME proper error handling
+  val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
 
-  private def changes_from(doc: Document): List[Text_Edit] =
-  {
-    Swing_Thread.assert()
-    (edits_buffer.toList /:
-      current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
-  }
+  def current_change(): Change = history
 
-  def from_current(doc: Document, offset: Int): Int =
-    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
-
-  def to_current(doc: Document, offset: Int): Int =
-    (offset /: changes_from(doc)) ((i, change) => change after i)
+  def snapshot(): Change.Snapshot =
+    Swing_Thread.now { history.snapshot(thy_name, edits_buffer.toList) }
 
 
   /* text edits */
 
-  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
-
   private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
     if (!edits_buffer.isEmpty) {
-      val new_change = current_change().edit(session, edits_buffer.toList)
+      val new_change = history.edit(session, List((thy_name, edits_buffer.toList)))
       edits_buffer.clear
       history = new_change
       new_change.result.map(_ => session.input(new_change))
@@ -130,9 +244,70 @@
   }
 
 
-  /* activation */
+  /* semantic token marker */
+
+  private val token_marker = new TokenMarker
+  {
+    override def markTokens(prev: TokenMarker.LineContext,
+        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
+    {
+      val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
+      val line = if (prev == null) 0 else previous.line + 1
+      val context = new Document_Model.Token_Markup.LineContext(line, previous)
+      val start = buffer.getLineStartOffset(line)
+      val stop = start + line_segment.count
+
+      val snapshot = Document_Model.this.snapshot()
+
+      /* FIXME
+      for (text_area <- Isabelle.jedit_text_areas(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)
 
-  private val token_marker = new Isabelle_Token_Marker(this)
+      var next_x = start
+      for {
+        (command, command_start) <-
+          snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
+        markup <- snapshot.document.current_state(command).highlight.flatten
+        val abs_start = snapshot.convert(command_start + markup.start)
+        val abs_stop = snapshot.convert(command_start + markup.stop)
+        if (abs_stop > start)
+        if (abs_start < stop)
+        val token_start = (abs_start - start) max 0
+        val token_length =
+          (abs_stop - abs_start) -
+          ((start - abs_start) max 0) -
+          ((abs_stop - stop) max 0)
+      }
+      {
+        val token_type =
+          markup.info match {
+            case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
+              Document_Model.Token_Markup.command_style(kind)
+            case Command.HighlightInfo(kind, _) =>
+              Document_Model.Token_Markup.token_style(kind)
+            case _ => Token.NULL
+          }
+        if (start + token_start > next_x)
+          handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
+        handle_token(token_type, token_start, token_length)
+        next_x = start + token_start + token_length
+      }
+      if (next_x < stop)
+        handle_token(Token.COMMENT1, next_x - start, stop - next_x)
+
+      handle_token(Token.END, line_segment.count, 0)
+      handler.setLineContext(context)
+      context
+    }
+  }
+
+
+  /* activation */
 
   def activate()
   {
diff -r 17d9808ed626 -r c75e9dc841c7 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -24,10 +24,11 @@
 
 object Document_View
 {
-  def choose_color(document: Document, command: Command): Color =
+  def choose_color(snapshot: Change.Snapshot, command: Command): Color =
   {
-    val state = document.current_state(command)
-    if (state.forks > 0) new Color(255, 228, 225)
+    val state = snapshot.document.current_state(command)
+    if (snapshot.is_outdated) new Color(240, 240, 240)
+    else if (state.forks > 0) new Color(255, 228, 225)
     else if (state.forks < 0) Color.red
     else
       state.status match {
@@ -86,7 +87,7 @@
   def extend_styles()
   {
     Swing_Thread.assert()
-    styles = Isabelle_Token_Marker.extend_styles(text_area.getPainter.getStyles)
+    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
   }
   extend_styles()
 
@@ -105,9 +106,9 @@
         case Command_Set(changed) =>
           Swing_Thread.now {
             // FIXME cover doc states as well!!?
-            val document = model.recent_document()
-            if (changed.exists(document.commands.contains))
-              full_repaint(document, changed)
+            val snapshot = model.snapshot()
+            if (changed.exists(snapshot.node.commands.contains))
+              full_repaint(snapshot, changed)
           }
 
         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
@@ -115,18 +116,18 @@
     }
   }
 
-  def full_repaint(document: Document, changed: Set[Command])
+  def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
   {
     Swing_Thread.assert()
 
     val buffer = model.buffer
     var visible_change = false
 
-    for ((command, start) <- document.command_starts) {
+    for ((command, start) <- snapshot.node.command_starts) {
       if (changed(command)) {
         val stop = start + command.length
-        val line1 = buffer.getLineOfOffset(model.to_current(document, start))
-        val line2 = buffer.getLineOfOffset(model.to_current(document, stop))
+        val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+        val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
         if (line2 >= text_area.getFirstLine &&
             line1 <= text_area.getFirstLine + text_area.getVisibleLines)
           visible_change = true
@@ -148,17 +149,15 @@
       start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
     {
       Swing_Thread.now {
-        val document = model.recent_document()
-        def from_current(pos: Int) = model.from_current(document, pos)
-        def to_current(pos: Int) = model.to_current(document, pos)
+        val snapshot = model.snapshot()
 
         val command_range: Iterable[(Command, Int)] =
         {
-          val range = document.command_range(from_current(start(0)))
+          val range = snapshot.node.command_range(snapshot.revert(start(0)))
           if (range.hasNext) {
             val (cmd0, start0) = range.next
             new Iterable[(Command, Int)] {
-              def iterator = Document.command_starts(document.commands.iterator(cmd0), start0)
+              def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
             }
           }
           else Iterable.empty
@@ -172,17 +171,19 @@
               val line_start = start(i)
               val line_end = model.visible_line_end(line_start, end(i))
 
-              val a = from_current(line_start)
-              val b = from_current(line_end)
+              val a = snapshot.revert(line_start)
+              val b = snapshot.revert(line_end)
               val cmds = command_range.iterator.
                 dropWhile { case (cmd, c) => c + cmd.length <= a } .
                 takeWhile { case (_, c) => c < b }
 
               for ((command, command_start) <- cmds if !command.is_ignored) {
-                val p = text_area.offsetToXY(line_start max to_current(command_start))
-                val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
+                val p =
+                  text_area.offsetToXY(line_start max snapshot.convert(command_start))
+                val q =
+                  text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
                 assert(p.y == q.y)
-                gfx.setColor(Document_View.choose_color(document, command))
+                gfx.setColor(Document_View.choose_color(snapshot, command))
                 gfx.fillRect(p.x, y, q.x - p.x, line_height)
               }
             }
@@ -195,11 +196,11 @@
 
     override def getToolTipText(x: Int, y: Int): String =
     {
-      val document = model.recent_document()
-      val offset = model.from_current(document, text_area.xyToOffset(x, y))
-      document.command_at(offset) match {
+      val snapshot = model.snapshot()
+      val offset = snapshot.revert(text_area.xyToOffset(x, y))
+      snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
-          document.current_state(command).type_at(offset - command_start) match {
+          snapshot.document.current_state(command).type_at(offset - command_start) match {
             case Some(text) => Isabelle.tooltip(text)
             case None => null
           }
@@ -212,7 +213,7 @@
   /* caret handling */
 
   def selected_command(): Option[Command] =
-    model.recent_document().proper_command_at(text_area.getCaretPosition)
+    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
 
   private val caret_listener = new CaretListener {
     private val delay = Swing_Thread.delay_last(session.input_delay) {
@@ -262,16 +263,15 @@
     {
       super.paintComponent(gfx)
       val buffer = model.buffer
-      val document = model.recent_document()
-      def to_current(pos: Int) = model.to_current(document, pos)
+      val snapshot = model.snapshot()
       val saved_color = gfx.getColor  // FIXME needed!?
       try {
-        for ((command, start) <- document.command_starts if !command.is_ignored) {
-          val line1 = buffer.getLineOfOffset(to_current(start))
-          val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
+        for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
+          val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+          val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
           val y = line_to_y(line1)
           val height = HEIGHT * (line2 - line1)
-          gfx.setColor(Document_View.choose_color(document, command))
+          gfx.setColor(Document_View.choose_color(snapshot, command))
           gfx.fillRect(0, y, getWidth - 1, height)
         }
       }
diff -r 17d9808ed626 -r c75e9dc841c7 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -42,25 +42,25 @@
   {
     Document_Model(buffer) match {
       case Some(model) =>
-        val document = model.recent_document()
-        val offset = model.from_current(document, original_offset)
-        document.command_at(offset) match {
+        val snapshot = model.snapshot()
+        val offset = snapshot.revert(original_offset)
+        snapshot.node.command_at(offset) match {
           case Some((command, command_start)) =>
-            document.current_state(command).ref_at(offset - command_start) match {
+            snapshot.document.current_state(command).ref_at(offset - command_start) match {
               case Some(ref) =>
-                val begin = model.to_current(document, command_start + ref.start)
+                val begin = snapshot.convert(command_start + ref.start)
                 val line = buffer.getLineOfOffset(begin)
-                val end = model.to_current(document, command_start + ref.stop)
+                val end = snapshot.convert(command_start + ref.stop)
                 ref.info match {
                   case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
                     new External_Hyperlink(begin, end, line, ref_file, ref_line)
                   case Command.RefInfo(_, _, Some(id), Some(offset)) =>
                     Isabelle.session.lookup_entity(id) match {
                       case Some(ref_cmd: Command) =>
-                        document.command_start(ref_cmd) match {
+                        snapshot.node.command_start(ref_cmd) match {
                           case Some(ref_cmd_start) =>
                             new Internal_Hyperlink(begin, end, line,
-                              model.to_current(document, ref_cmd_start + offset - 1))
+                              snapshot.convert(ref_cmd_start + offset - 1))
                           case None => null // FIXME external ref
                         }
                       case _ => null
diff -r 17d9808ed626 -r c75e9dc841c7 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -95,9 +95,9 @@
     import Isabelle_Sidekick.int_to_pos
 
     val root = data.root
-    val document = model.recent_document()
+    val doc = model.snapshot().node  // FIXME cover all nodes (!??)
     for {
-      (command, command_start) <- document.command_range(0)
+      (command, command_start) <- doc.command_range(0)
       if command.is_command && !stopped
     }
     {
@@ -128,9 +128,9 @@
     import Isabelle_Sidekick.int_to_pos
 
     val root = data.root
-    val document = model.recent_document()
-    for ((command, command_start) <- document.command_range(0) if !stopped) {
-      root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
+    val snapshot = model.snapshot()  // FIXME cover all nodes (!??)
+    for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
+      root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
           {
             val content = command.source(node.start, node.stop).replace('\n', ' ')
             val id = command.id
diff -r 17d9808ed626 -r c75e9dc841c7 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Fri Aug 06 11:37:33 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,202 +0,0 @@
-/*  Title:      Tools/jEdit/src/jedit/isabelle_token_marker.scala
-    Author:     Fabian Immler, TU Munich
-
-Include isabelle's command- and keyword-declarations live in jEdits
-syntax-highlighting.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, ParserRuleSet, SyntaxStyle}
-import org.gjt.sp.jedit.textarea.TextArea
-
-import java.awt.Font
-import java.awt.font.TextAttribute
-import javax.swing.text.Segment;
-
-
-object Isabelle_Token_Marker
-{
-  /* extended token styles */
-
-  private val plain_range: Int = Token.ID_COUNT
-  private val full_range: Int = 3 * plain_range
-  private def check_range(i: Int) { require(0 <= i && i < plain_range) }
-
-  def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
-  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
-
-  private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
-  {
-    import scala.collection.JavaConversions._
-    val script_font =
-      style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
-    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
-  }
-
-  def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
-  {
-    val new_styles = new Array[SyntaxStyle](full_range)
-    for (i <- 0 until plain_range) {
-      val style = styles(i)
-      new_styles(i) = style
-      new_styles(subscript(i.toByte)) = script_style(style, -1)
-      new_styles(superscript(i.toByte)) = script_style(style, 1)
-    }
-    new_styles
-  }
-
-
-  /* line context */
-
-  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
-  private class LineContext(val line: Int, prev: LineContext)
-    extends TokenMarker.LineContext(rule_set, prev)
-
-
-  /* mapping to jEdit token types */
-  // TODO: as properties or CSS style sheet
-
-  private val command_style: Map[String, Byte] =
-  {
-    import Token._
-    Map[String, Byte](
-      Keyword.THY_END -> KEYWORD2,
-      Keyword.THY_SCRIPT -> LABEL,
-      Keyword.PRF_SCRIPT -> LABEL,
-      Keyword.PRF_ASM -> KEYWORD3,
-      Keyword.PRF_ASM_GOAL -> KEYWORD3
-    ).withDefaultValue(KEYWORD1)
-  }
-
-  private val token_style: Map[String, Byte] =
-  {
-    import Token._
-    Map[String, Byte](
-      // logical entities
-      Markup.TCLASS -> NULL,
-      Markup.TYCON -> NULL,
-      Markup.FIXED_DECL -> FUNCTION,
-      Markup.FIXED -> NULL,
-      Markup.CONST_DECL -> FUNCTION,
-      Markup.CONST -> NULL,
-      Markup.FACT_DECL -> FUNCTION,
-      Markup.FACT -> NULL,
-      Markup.DYNAMIC_FACT -> LABEL,
-      Markup.LOCAL_FACT_DECL -> FUNCTION,
-      Markup.LOCAL_FACT -> NULL,
-      // inner syntax
-      Markup.TFREE -> NULL,
-      Markup.FREE -> NULL,
-      Markup.TVAR -> NULL,
-      Markup.SKOLEM -> NULL,
-      Markup.BOUND -> NULL,
-      Markup.VAR -> NULL,
-      Markup.NUM -> DIGIT,
-      Markup.FLOAT -> DIGIT,
-      Markup.XNUM -> DIGIT,
-      Markup.XSTR -> LITERAL4,
-      Markup.LITERAL -> OPERATOR,
-      Markup.INNER_COMMENT -> COMMENT1,
-      Markup.SORT -> NULL,
-      Markup.TYP -> NULL,
-      Markup.TERM -> NULL,
-      Markup.PROP -> NULL,
-      Markup.ATTRIBUTE -> NULL,
-      Markup.METHOD -> NULL,
-      // ML syntax
-      Markup.ML_KEYWORD -> KEYWORD1,
-      Markup.ML_DELIMITER -> OPERATOR,
-      Markup.ML_IDENT -> NULL,
-      Markup.ML_TVAR -> NULL,
-      Markup.ML_NUMERAL -> DIGIT,
-      Markup.ML_CHAR -> LITERAL1,
-      Markup.ML_STRING -> LITERAL1,
-      Markup.ML_COMMENT -> COMMENT1,
-      Markup.ML_MALFORMED -> INVALID,
-      // embedded source text
-      Markup.ML_SOURCE -> COMMENT3,
-      Markup.DOC_SOURCE -> COMMENT3,
-      Markup.ANTIQ -> COMMENT4,
-      Markup.ML_ANTIQ -> COMMENT4,
-      Markup.DOC_ANTIQ -> COMMENT4,
-      // outer syntax
-      Markup.KEYWORD -> KEYWORD2,
-      Markup.OPERATOR -> OPERATOR,
-      Markup.COMMAND -> KEYWORD1,
-      Markup.IDENT -> NULL,
-      Markup.VERBATIM -> COMMENT3,
-      Markup.COMMENT -> COMMENT1,
-      Markup.CONTROL -> COMMENT3,
-      Markup.MALFORMED -> INVALID,
-      Markup.STRING -> LITERAL3,
-      Markup.ALTSTRING -> LITERAL1
-    ).withDefaultValue(NULL)
-  }
-}
-
-
-class Isabelle_Token_Marker(model: Document_Model) extends TokenMarker
-{
-  override def markTokens(prev: TokenMarker.LineContext,
-      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
-  {
-    val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
-    val line = if (prev == null) 0 else previous.line + 1
-    val context = new Isabelle_Token_Marker.LineContext(line, previous)
-    val start = model.buffer.getLineStartOffset(line)
-    val stop = start + line_segment.count
-
-    val document = model.recent_document()
-    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)
-
-    var next_x = start
-    for {
-      (command, command_start) <- document.command_range(from(start), from(stop))
-      markup <- document.current_state(command).highlight.flatten
-      val abs_start = to(command_start + markup.start)
-      val abs_stop = to(command_start + markup.stop)
-      if (abs_stop > start)
-      if (abs_start < stop)
-      val token_start = (abs_start - start) max 0
-      val token_length =
-        (abs_stop - abs_start) -
-        ((start - abs_start) max 0) -
-        ((abs_stop - stop) max 0)
-    }
-    {
-      val token_type =
-        markup.info match {
-          case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
-            Isabelle_Token_Marker.command_style(kind)
-          case Command.HighlightInfo(kind, _) =>
-            Isabelle_Token_Marker.token_style(kind)
-          case _ => Token.NULL
-        }
-      if (start + token_start > next_x)
-        handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
-      handle_token(token_type, token_start, token_length)
-      next_x = start + token_start + token_length
-    }
-    if (next_x < stop)
-      handle_token(Token.COMMENT1, next_x - start, stop - next_x)
-
-    handle_token(Token.END, line_segment.count, 0)
-    handler.setLineContext(context)
-    context
-  }
-}
diff -r 17d9808ed626 -r c75e9dc841c7 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri Aug 06 11:37:33 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Fri Aug 06 12:38:02 2010 +0200
@@ -65,9 +65,9 @@
         case Some(doc_view) =>
           current_command match {
             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
-              val document = doc_view.model.recent_document
+              val snapshot = doc_view.model.snapshot()
               val filtered_results =
-                document.current_state(cmd).results filter {
+                snapshot.document.current_state(cmd).results filter {
                   case XML.Elem(Markup.TRACING, _, _) => show_tracing
                   case XML.Elem(Markup.DEBUG, _, _) => show_debug
                   case _ => true