5 * @author Fabian Immler, TU Munich |
5 * @author Fabian Immler, TU Munich |
6 */ |
6 */ |
7 |
7 |
8 package isabelle.proofdocument |
8 package isabelle.proofdocument |
9 |
9 |
10 abstract class Edit { |
10 sealed abstract class Edit |
|
11 { |
11 val start: Int |
12 val start: Int |
12 def from_where (x: Int): Int //where has x been before applying this edit |
13 def from_where (x: Int): Int //where has x been before applying this edit |
13 def where_to(x: Int): Int //where will x be when we apply this edit |
14 def where_to(x: Int): Int //where will x be when we apply this edit |
14 } |
15 } |
15 |
16 |
16 case class Insert(start: Int, added: String) extends Edit { |
17 case class Insert(start: Int, text: String) extends Edit |
|
18 { |
17 def from_where(x: Int) = |
19 def from_where(x: Int) = |
18 if (start > x) x |
20 if (start > x) x |
19 else (x - added.length) max start |
21 else (x - text.length) max start |
20 |
22 |
21 def where_to(x: Int) = |
23 def where_to(x: Int) = |
22 if (start <= x) x + added.length else x |
24 if (start <= x) x + text.length else x |
23 } |
25 } |
24 |
26 |
25 case class Remove(start: Int, removed: String) extends Edit { |
27 case class Remove(start: Int, text: String) extends Edit |
|
28 { |
26 def from_where(x: Int) = |
29 def from_where(x: Int) = |
27 if (start <= x) x + removed.length else x |
30 if (start <= x) x + text.length else x |
28 |
31 |
29 def where_to(x: Int) = |
32 def where_to(x: Int) = |
30 if (start > x) x |
33 if (start > x) x |
31 else (x - removed.length) max start |
34 else (x - text.length) max start |
32 } |
35 } |
33 // TODO: merge multiple inserts? |
36 // TODO: merge multiple inserts? |
34 |
37 |
35 class Change( |
38 class Change( |
36 val id: String, |
39 val id: String, |
37 val parent: Option[Change], |
40 val parent: Option[Change], |
38 edits: List[Edit]) extends Iterable[Edit] |
41 val edits: List[Edit]) |
39 { |
42 { |
40 override def elements = edits.reverse.elements |
43 def ancestors(done: Change => Boolean): List[Change] = |
41 |
44 if (done(this)) Nil |
42 def ancestors(root_p: Change => Boolean): List[Change] = |
45 else this :: parent.map(_.ancestors(done)).getOrElse(Nil) |
43 if (root_p(this)) Nil |
|
44 else this :: parent.map(_.ancestors(root_p)).getOrElse(Nil) |
|
45 def ancestors: List[Change] = ancestors(_ => false) |
46 def ancestors: List[Change] = ancestors(_ => false) |
46 |
47 |
47 override def toString = |
48 override def toString = |
48 "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")" |
49 "Change(" + id + " <- " + parent.map(_.id) + ", " + edits + ")" |
49 } |
50 } |