author | wenzelm |
Wed, 05 May 2010 22:23:45 +0200 | |
changeset 36676 | ac7961d42ac3 |
parent 36012 | src/Pure/Thy/document.scala@0614676f14d4 |
child 36761 | c8ae87ce6e4d |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/document.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Document as editable list of commands. |
|
5 |
*/ |
|
34407 | 6 |
|
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34868
diff
changeset
|
7 |
package isabelle |
34318
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 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34871
diff
changeset
|
17 |
for (cmd <- commands.iterator) yield { |
34859 | 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 |
|
40 |
||
41 |
||
42 |
||
43 |
/** document edits **/ |
|
44 |
||
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
45 |
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
|
46 |
|
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
47 |
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
|
48 |
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
|
49 |
{ |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
50 |
require(old_doc.assignment.is_finished) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
51 |
|
34859 | 52 |
|
53 |
/* unparsed dummy commands */ |
|
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
54 |
|
34859 | 55 |
def unparsed(source: String) = |
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
56 |
new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) |
34859 | 57 |
|
34860
847c00f5535a
do not override Command.hashCode -- which was inconsistent with eq anyway;
wenzelm
parents:
34859
diff
changeset
|
58 |
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
|
59 |
|
34863 | 60 |
assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove |
34859 | 61 |
|
62 |
||
63 |
/* phase 1: edit individual command source */ |
|
64 |
||
34863 | 65 |
def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] = |
34859 | 66 |
{ |
67 |
eds match { |
|
68 |
case e :: es => |
|
69 |
command_starts(commands).find { // FIXME relative search! |
|
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
70 |
case (cmd, cmd_start) => |
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
71 |
e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length |
34863 | 72 |
} match { |
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
73 |
case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => |
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
74 |
val (rest, text) = e.edit(cmd.source, cmd_start) |
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
75 |
val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd |
34863 | 76 |
edit_text(rest.toList ::: es, new_commands) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
77 |
|
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
78 |
case Some((cmd, cmd_start)) => |
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
79 |
edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) |
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
80 |
|
34859 | 81 |
case None => |
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
82 |
require(e.is_insert && e.start == 0) |
34863 | 83 |
edit_text(es, commands.insert_after(None, unparsed(e.text))) |
34859 | 84 |
} |
34863 | 85 |
case Nil => commands |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
86 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
87 |
} |
34582 | 88 |
|
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
89 |
|
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
90 |
/* phase 2: recover command spans */ |
34859 | 91 |
|
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
92 |
def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = |
34859 | 93 |
{ |
94 |
// FIXME relative search! |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34871
diff
changeset
|
95 |
commands.iterator.find(is_unparsed) match { |
34859 | 96 |
case Some(first_unparsed) => |
97 |
val prefix = commands.prev(first_unparsed) |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34871
diff
changeset
|
98 |
val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList |
34859 | 99 |
val suffix = commands.next(body.last) |
100 |
||
34863 | 101 |
val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) |
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
102 |
val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) |
34485 | 103 |
|
34859 | 104 |
val (before_edit, spans1) = |
36012 | 105 |
if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span)) |
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
106 |
(prefix, spans0.tail) |
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
107 |
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
|
108 |
|
34859 | 109 |
val (after_edit, spans2) = |
110 |
if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) |
|
111 |
(suffix, spans1.take(spans1.length - 1)) |
|
112 |
else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) |
|
113 |
||
34863 | 114 |
val inserted = spans2.map(span => new Command(session.create_id(), span)) |
115 |
val new_commands = |
|
116 |
commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) |
|
34866
a4fe43df58b3
new unparsed span for text right after existing command;
wenzelm
parents:
34863
diff
changeset
|
117 |
parse_spans(new_commands) |
34485 | 118 |
|
34863 | 119 |
case None => commands |
34485 | 120 |
} |
121 |
} |
|
34739 | 122 |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
123 |
|
34859 | 124 |
/* phase 3: resulting document edits */ |
125 |
||
34867 | 126 |
val result = Library.timeit("text_edits") { |
127 |
val commands0 = old_doc.commands |
|
128 |
val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) } |
|
129 |
val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) } |
|
34660 | 130 |
|
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34871
diff
changeset
|
131 |
val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList |
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34871
diff
changeset
|
132 |
val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList |
34863 | 133 |
|
34867 | 134 |
val doc_edits = |
135 |
removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: |
|
136 |
inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) |
|
34660 | 137 |
|
34867 | 138 |
val former_states = old_doc.assignment.join -- removed_commands |
34859 | 139 |
|
34867 | 140 |
phase0 = edits |
141 |
phase1 = commands1 |
|
142 |
phase2 = commands2 |
|
143 |
phase3 = doc_edits |
|
34863 | 144 |
|
34867 | 145 |
(doc_edits, new Document(new_id, commands2, former_states)) |
146 |
} |
|
147 |
result |
|
34485 | 148 |
} |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
149 |
} |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
150 |
|
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
151 |
|
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
152 |
class Document( |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
153 |
val id: Isar_Document.Document_ID, |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
154 |
val commands: Linear_Set[Command], |
34859 | 155 |
former_states: Map[Command, Command]) |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
156 |
{ |
34859 | 157 |
/* command ranges */ |
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
158 |
|
34859 | 159 |
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
|
160 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
161 |
def command_start(cmd: Command): Option[Int] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
162 |
command_starts.find(_._1 == cmd).map(_._2) |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
163 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
164 |
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
|
165 |
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
|
166 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
167 |
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
|
168 |
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
|
169 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
170 |
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
|
171 |
{ |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
172 |
val range = command_range(i) |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
173 |
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
|
174 |
} |
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 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
177 |
/* command state assignment */ |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
178 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
179 |
val assignment = Future.promise[Map[Command, Command]] |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
180 |
def await_assignment { assignment.join } |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
181 |
|
34859 | 182 |
@volatile private var tmp_states = former_states |
34868 | 183 |
private val time0 = System.currentTimeMillis |
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 |
def assign_states(new_states: List[(Command, Command)]) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
186 |
{ |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
187 |
assignment.fulfill(tmp_states ++ new_states) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
188 |
tmp_states = Map() |
34868 | 189 |
System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time") |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
190 |
} |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
191 |
|
34867 | 192 |
def current_state(cmd: Command): Option[State] = |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
193 |
{ |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
194 |
require(assignment.is_finished) |
34867 | 195 |
(assignment.join).get(cmd).map(_.current_state) |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
196 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
197 |
} |