--- 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
--- 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
--- 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 *}
--- 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 *}
--- 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 *}
--- 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 *}
--- 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 {*
--- 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{*
--- 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 *}
--- 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 *}
--- 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 {*
--- 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 *}
--- 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:
--- 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 _'))")
--- 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"
--- 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 -
--- 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 *}
--- 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)
--- 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)"
--- 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 \
--- 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;
--- 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)
}
}
--- 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
--- 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
--- /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;
+
--- 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]]
--- 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 */
--- 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";
--- 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]
}
--- 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 ()
--- 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)
+ }
}
--- 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;
--- 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/
--- 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"
--- 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()
{
--- 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)
}
}
--- 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
--- 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
--- 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
- }
-}
--- 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