author | wenzelm |
Mon, 11 Jan 2010 13:58:51 +0100 | |
changeset 34862 | a1d394600a92 |
parent 34860 | 847c00f5535a |
child 34863 | 3e655d0ff936 |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
34862 | 2 |
* Document as editable list of commands |
34407 | 3 |
* |
34485 | 4 |
* @author Makarius |
34407 | 5 |
*/ |
6 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.proofdocument |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
|
34760 | 9 |
|
34823 | 10 |
object Document |
34483 | 11 |
{ |
34859 | 12 |
/* command start positions */ |
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
13 |
|
34859 | 14 |
def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] = |
15 |
{ |
|
16 |
var offset = 0 |
|
17 |
for (cmd <- commands.elements) yield { |
|
18 |
val start = offset |
|
19 |
offset += cmd.length |
|
20 |
(cmd, start) |
|
21 |
} |
|
22 |
} |
|
23 |
||
24 |
||
25 |
/* empty document */ |
|
34485 | 26 |
|
34823 | 27 |
def empty(id: Isar_Document.Document_ID): Document = |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
28 |
{ |
34859 | 29 |
val doc = new Document(id, Linear_Set(), Map()) |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
30 |
doc.assign_states(Nil) |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
31 |
doc |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
32 |
} |
34660 | 33 |
|
34859 | 34 |
|
35 |
// FIXME |
|
36 |
var phase0: List[Text_Edit] = null |
|
37 |
var phase1: Linear_Set[Command] = null |
|
38 |
var phase2: Linear_Set[Command] = null |
|
39 |
var phase3: List[Edit] = null |
|
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
40 |
var raw_source: String = null |
34859 | 41 |
|
42 |
||
43 |
||
44 |
/** document edits **/ |
|
45 |
||
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
46 |
type Edit = (Option[Command], Option[Command]) |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
47 |
|
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
48 |
def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
49 |
edits: List[Text_Edit]): (List[Edit], Document) = |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
50 |
{ |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
51 |
require(old_doc.assignment.is_finished) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
52 |
|
34859 | 53 |
phase0 = edits |
54 |
||
55 |
||
56 |
/* unparsed dummy commands */ |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
57 |
|
34859 | 58 |
def unparsed(source: String) = |
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
59 |
new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) |
34859 | 60 |
|
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
61 |
def is_unparsed(command: Command) = command.id == null |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
62 |
|
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
63 |
assert(!old_doc.commands.exists(is_unparsed)) |
34859 | 64 |
|
65 |
||
66 |
/* phase 1: edit individual command source */ |
|
67 |
||
68 |
var commands = old_doc.commands |
|
34485 | 69 |
|
34859 | 70 |
def edit_text(eds: List[Text_Edit]): Unit = |
71 |
{ |
|
72 |
eds match { |
|
73 |
case e :: es => |
|
74 |
command_starts(commands).find { // FIXME relative search! |
|
75 |
case (cmd, cmd_start) => e.can_edit(cmd.length, cmd_start) |
|
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
76 |
} match { // FIXME try to append after command |
34859 | 77 |
case Some((cmd, cmd_start)) => |
78 |
val (rest, source) = e.edit(cmd.source, cmd_start) |
|
79 |
// FIXME Linear_Set.edit (?) |
|
80 |
commands = commands.insert_after(Some(cmd), unparsed(source)) |
|
81 |
commands -= cmd |
|
82 |
edit_text(rest.toList ::: es) |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
83 |
|
34859 | 84 |
case None => |
85 |
require(e.isInstanceOf[Text_Edit.Insert] && e.start == 0) |
|
86 |
commands = commands.insert_after(None, unparsed(e.text)) |
|
87 |
edit_text(es) |
|
88 |
} |
|
89 |
case Nil => |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
90 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
91 |
} |
34859 | 92 |
edit_text(edits) |
93 |
||
94 |
phase1 = commands |
|
34582 | 95 |
|
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
96 |
|
34859 | 97 |
/* phase 2: command range edits */ |
98 |
||
99 |
def edit_commands(): Unit = |
|
100 |
{ |
|
101 |
// FIXME relative search! |
|
102 |
commands.elements.find(is_unparsed) match { |
|
103 |
case Some(first_unparsed) => |
|
104 |
val prefix = commands.prev(first_unparsed) |
|
105 |
val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList |
|
106 |
val suffix = commands.next(body.last) |
|
107 |
||
108 |
val source = |
|
109 |
(prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)).mkString |
|
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
110 |
assert(source != "") |
34859 | 111 |
raw_source = source |
112 |
||
113 |
val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(source)) |
|
34485 | 114 |
|
34859 | 115 |
val (before_edit, spans1) = |
116 |
if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span)) |
|
117 |
(prefix, spans0.tail) |
|
118 |
else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) |
|
34544
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34541
diff
changeset
|
119 |
|
34859 | 120 |
val (after_edit, spans2) = |
121 |
if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) |
|
122 |
(suffix, spans1.take(spans1.length - 1)) |
|
123 |
else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) |
|
124 |
||
125 |
val new_commands = spans2.map(span => new Command(session.create_id(), span)) |
|
34485 | 126 |
|
34859 | 127 |
commands = commands.delete_between(before_edit, after_edit) |
128 |
commands = commands.append_after(before_edit, new_commands) |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
129 |
|
34859 | 130 |
edit_commands() |
131 |
||
132 |
case None => |
|
34485 | 133 |
} |
134 |
} |
|
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
135 |
edit_commands() |
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
136 |
|
34859 | 137 |
phase2 = commands |
34739 | 138 |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
139 |
|
34859 | 140 |
/* phase 3: resulting document edits */ |
141 |
||
142 |
val removed_commands = old_doc.commands.elements.filter(!commands.contains(_)).toList |
|
143 |
val inserted_commands = commands.elements.filter(!old_doc.commands.contains(_)).toList |
|
34660 | 144 |
|
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
145 |
// FIXME proper order |
34859 | 146 |
val doc_edits = |
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
147 |
removed_commands.reverse.map(cmd => (commands.prev(cmd), None)) ::: |
34859 | 148 |
inserted_commands.map(cmd => (commands.prev(cmd), Some(cmd))) |
34660 | 149 |
|
34859 | 150 |
val former_states = old_doc.assignment.join -- removed_commands |
151 |
||
152 |
phase3 = doc_edits |
|
153 |
(doc_edits, new Document(new_id, commands, former_states)) |
|
34485 | 154 |
} |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
155 |
} |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
156 |
|
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
157 |
|
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
158 |
class Document( |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
159 |
val id: Isar_Document.Document_ID, |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
160 |
val commands: Linear_Set[Command], |
34859 | 161 |
former_states: Map[Command, Command]) |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
162 |
{ |
34859 | 163 |
/* command ranges */ |
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
164 |
|
34859 | 165 |
def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands) |
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
166 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
167 |
def command_start(cmd: Command): Option[Int] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
168 |
command_starts.find(_._1 == cmd).map(_._2) |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
169 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
170 |
def command_range(i: Int): Iterator[(Command, Int)] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
171 |
command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
172 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
173 |
def command_range(i: Int, j: Int): Iterator[(Command, Int)] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
174 |
command_range(i) takeWhile { case (_, start) => start < j } |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
175 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
176 |
def command_at(i: Int): Option[(Command, Int)] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
177 |
{ |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
178 |
val range = command_range(i) |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
179 |
if (range.hasNext) Some(range.next) else None |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
180 |
} |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
181 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
182 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
183 |
/* command state assignment */ |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
184 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
185 |
val assignment = Future.promise[Map[Command, Command]] |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
186 |
def await_assignment { assignment.join } |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
187 |
|
34859 | 188 |
@volatile private var tmp_states = former_states |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
189 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
190 |
def assign_states(new_states: List[(Command, Command)]) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
191 |
{ |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
192 |
assignment.fulfill(tmp_states ++ new_states) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
193 |
tmp_states = Map() |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
194 |
} |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
195 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
196 |
def current_state(cmd: Command): State = |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
197 |
{ |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
198 |
require(assignment.is_finished) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
199 |
(assignment.join)(cmd).current_state |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
200 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
201 |
} |