author | wenzelm |
Fri, 01 Jan 2010 17:29:35 +0100 | |
changeset 34824 | ac35eee85f5c |
parent 34759 | bfea7839d9e1 |
child 34825 | 7f72547f9b12 |
permissions | -rw-r--r-- |
34660 | 1 |
/* |
34703 | 2 |
* Changes of plain text |
34660 | 3 |
* |
4 |
* @author Johannes Hölzl, TU Munich |
|
5 |
* @author Fabian Immler, TU Munich |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle.proofdocument |
|
9 |
||
34703 | 10 |
|
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
11 |
import scala.actors.Future |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
12 |
|
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
13 |
|
34693 | 14 |
sealed abstract class Edit |
15 |
{ |
|
34660 | 16 |
val start: Int |
34695 | 17 |
def before(offset: Int): Int |
18 |
def after(offset: Int): Int |
|
34660 | 19 |
} |
20 |
||
34703 | 21 |
|
34693 | 22 |
case class Insert(start: Int, text: String) extends Edit |
23 |
{ |
|
34695 | 24 |
def before(offset: Int): Int = |
25 |
if (start > offset) offset |
|
26 |
else (offset - text.length) max start |
|
34660 | 27 |
|
34695 | 28 |
def after(offset: Int): Int = |
29 |
if (start <= offset) offset + text.length else offset |
|
34660 | 30 |
} |
31 |
||
34703 | 32 |
|
34693 | 33 |
case class Remove(start: Int, text: String) extends Edit |
34 |
{ |
|
34695 | 35 |
def before(offset: Int): Int = |
36 |
if (start <= offset) offset + text.length else offset |
|
34660 | 37 |
|
34695 | 38 |
def after(offset: Int): Int = |
39 |
if (start > offset) offset |
|
40 |
else (offset - text.length) max start |
|
34660 | 41 |
} |
42 |
// TODO: merge multiple inserts? |
|
43 |
||
34703 | 44 |
|
34660 | 45 |
class Change( |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
46 |
val id: Isar_Document.Document_ID, |
34660 | 47 |
val parent: Option[Change], |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
48 |
val edits: List[Edit], |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
49 |
val result: Future[Document.Result]) |
34660 | 50 |
{ |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
51 |
// FIXME iterator |
34693 | 52 |
def ancestors(done: Change => Boolean): List[Change] = |
53 |
if (done(this)) Nil |
|
54 |
else this :: parent.map(_.ancestors(done)).getOrElse(Nil) |
|
34660 | 55 |
def ancestors: List[Change] = ancestors(_ => false) |
56 |
||
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
57 |
def document: Document = result()._1 |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34759
diff
changeset
|
58 |
def document_edits: List[Document.Structure_Edit] = result()._2 |
34660 | 59 |
} |