wenzelm@34410
|
1 |
/*
|
wenzelm@34865
|
2 |
* Document as editable list of commands
|
wenzelm@34410
|
3 |
*
|
wenzelm@34488
|
4 |
* @author Makarius
|
wenzelm@34410
|
5 |
*/
|
wenzelm@34410
|
6 |
|
wenzelm@34321
|
7 |
package isabelle.proofdocument
|
wenzelm@34321
|
8 |
|
wenzelm@34763
|
9 |
|
wenzelm@34826
|
10 |
object Document
|
wenzelm@34486
|
11 |
{
|
wenzelm@34862
|
12 |
/* command start positions */
|
wenzelm@34821
|
13 |
|
wenzelm@34862
|
14 |
def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
|
wenzelm@34862
|
15 |
{
|
wenzelm@34862
|
16 |
var offset = 0
|
wenzelm@34862
|
17 |
for (cmd <- commands.elements) yield {
|
wenzelm@34862
|
18 |
val start = offset
|
wenzelm@34862
|
19 |
offset += cmd.length
|
wenzelm@34862
|
20 |
(cmd, start)
|
wenzelm@34862
|
21 |
}
|
wenzelm@34862
|
22 |
}
|
wenzelm@34862
|
23 |
|
wenzelm@34862
|
24 |
|
wenzelm@34862
|
25 |
/* empty document */
|
wenzelm@34488
|
26 |
|
wenzelm@34826
|
27 |
def empty(id: Isar_Document.Document_ID): Document =
|
wenzelm@34838
|
28 |
{
|
wenzelm@34862
|
29 |
val doc = new Document(id, Linear_Set(), Map())
|
wenzelm@34838
|
30 |
doc.assign_states(Nil)
|
wenzelm@34838
|
31 |
doc
|
wenzelm@34838
|
32 |
}
|
immler@34663
|
33 |
|
wenzelm@34862
|
34 |
|
wenzelm@34862
|
35 |
// FIXME
|
wenzelm@34862
|
36 |
var phase0: List[Text_Edit] = null
|
wenzelm@34862
|
37 |
var phase1: Linear_Set[Command] = null
|
wenzelm@34862
|
38 |
var phase2: Linear_Set[Command] = null
|
wenzelm@34862
|
39 |
var phase3: List[Edit] = null
|
wenzelm@34862
|
40 |
|
wenzelm@34862
|
41 |
|
wenzelm@34862
|
42 |
|
wenzelm@34862
|
43 |
/** document edits **/
|
wenzelm@34862
|
44 |
|
wenzelm@34856
|
45 |
type Edit = (Option[Command], Option[Command])
|
wenzelm@34827
|
46 |
|
wenzelm@34827
|
47 |
def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
|
wenzelm@34856
|
48 |
edits: List[Text_Edit]): (List[Edit], Document) =
|
wenzelm@34827
|
49 |
{
|
wenzelm@34843
|
50 |
require(old_doc.assignment.is_finished)
|
wenzelm@34843
|
51 |
|
wenzelm@34862
|
52 |
|
wenzelm@34862
|
53 |
/* unparsed dummy commands */
|
wenzelm@34862
|
54 |
|
wenzelm@34862
|
55 |
def unparsed(source: String) =
|
wenzelm@34863
|
56 |
new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
|
wenzelm@34862
|
57 |
|
wenzelm@34863
|
58 |
def is_unparsed(command: Command) = command.id == null
|
wenzelm@34862
|
59 |
|
wenzelm@34866
|
60 |
assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
|
wenzelm@34862
|
61 |
|
wenzelm@34862
|
62 |
|
wenzelm@34862
|
63 |
/* phase 1: edit individual command source */
|
wenzelm@34862
|
64 |
|
wenzelm@34866
|
65 |
def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
|
wenzelm@34862
|
66 |
{
|
wenzelm@34862
|
67 |
eds match {
|
wenzelm@34862
|
68 |
case e :: es =>
|
wenzelm@34862
|
69 |
command_starts(commands).find { // FIXME relative search!
|
wenzelm@34862
|
70 |
case (cmd, cmd_start) => e.can_edit(cmd.length, cmd_start)
|
wenzelm@34866
|
71 |
} match {
|
wenzelm@34866
|
72 |
// FIXME try to append after command
|
wenzelm@34862
|
73 |
case Some((cmd, cmd_start)) =>
|
wenzelm@34862
|
74 |
val (rest, source) = e.edit(cmd.source, cmd_start)
|
wenzelm@34866
|
75 |
val new_commands = commands.insert_after(Some(cmd), unparsed(source)) - cmd
|
wenzelm@34866
|
76 |
edit_text(rest.toList ::: es, new_commands)
|
wenzelm@34862
|
77 |
|
wenzelm@34862
|
78 |
case None =>
|
wenzelm@34862
|
79 |
require(e.isInstanceOf[Text_Edit.Insert] && e.start == 0)
|
wenzelm@34866
|
80 |
edit_text(es, commands.insert_after(None, unparsed(e.text)))
|
wenzelm@34862
|
81 |
}
|
wenzelm@34866
|
82 |
case Nil => commands
|
wenzelm@34862
|
83 |
}
|
wenzelm@34862
|
84 |
}
|
wenzelm@34862
|
85 |
|
wenzelm@34862
|
86 |
|
wenzelm@34862
|
87 |
/* phase 2: command range edits */
|
wenzelm@34862
|
88 |
|
wenzelm@34866
|
89 |
def edit_commands(commands: Linear_Set[Command]): Linear_Set[Command] =
|
wenzelm@34862
|
90 |
{
|
wenzelm@34862
|
91 |
// FIXME relative search!
|
wenzelm@34862
|
92 |
commands.elements.find(is_unparsed) match {
|
wenzelm@34862
|
93 |
case Some(first_unparsed) =>
|
wenzelm@34862
|
94 |
val prefix = commands.prev(first_unparsed)
|
wenzelm@34862
|
95 |
val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
|
wenzelm@34862
|
96 |
val suffix = commands.next(body.last)
|
wenzelm@34862
|
97 |
|
wenzelm@34866
|
98 |
val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
|
wenzelm@34866
|
99 |
val span = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
|
wenzelm@34862
|
100 |
|
wenzelm@34862
|
101 |
val (before_edit, spans1) =
|
wenzelm@34866
|
102 |
if (!span.isEmpty && Some(span.first) == prefix.map(_.span))
|
wenzelm@34866
|
103 |
(prefix, span.tail)
|
wenzelm@34866
|
104 |
else (if (prefix.isDefined) commands.prev(prefix.get) else None, span)
|
wenzelm@34862
|
105 |
|
wenzelm@34862
|
106 |
val (after_edit, spans2) =
|
wenzelm@34862
|
107 |
if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
|
wenzelm@34862
|
108 |
(suffix, spans1.take(spans1.length - 1))
|
wenzelm@34862
|
109 |
else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
|
wenzelm@34862
|
110 |
|
wenzelm@34866
|
111 |
val inserted = spans2.map(span => new Command(session.create_id(), span))
|
wenzelm@34866
|
112 |
val new_commands =
|
wenzelm@34866
|
113 |
commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
|
wenzelm@34866
|
114 |
edit_commands(new_commands)
|
wenzelm@34862
|
115 |
|
wenzelm@34866
|
116 |
case None => commands
|
wenzelm@34862
|
117 |
}
|
wenzelm@34862
|
118 |
}
|
wenzelm@34862
|
119 |
|
wenzelm@34862
|
120 |
|
wenzelm@34862
|
121 |
/* phase 3: resulting document edits */
|
wenzelm@34862
|
122 |
|
wenzelm@34866
|
123 |
val commands0 = old_doc.commands
|
wenzelm@34866
|
124 |
val commands1 = edit_text(edits, commands0)
|
wenzelm@34866
|
125 |
val commands2 = edit_commands(commands1)
|
wenzelm@34862
|
126 |
|
wenzelm@34866
|
127 |
val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
|
wenzelm@34866
|
128 |
val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
|
wenzelm@34866
|
129 |
|
wenzelm@34866
|
130 |
// FIXME tune
|
wenzelm@34862
|
131 |
val doc_edits =
|
wenzelm@34866
|
132 |
removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
|
wenzelm@34866
|
133 |
inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
|
wenzelm@34862
|
134 |
|
wenzelm@34862
|
135 |
val former_states = old_doc.assignment.join -- removed_commands
|
wenzelm@34862
|
136 |
|
wenzelm@34866
|
137 |
phase0 = edits
|
wenzelm@34866
|
138 |
phase1 = commands1
|
wenzelm@34866
|
139 |
phase2 = commands2
|
wenzelm@34862
|
140 |
phase3 = doc_edits
|
wenzelm@34866
|
141 |
|
wenzelm@34866
|
142 |
(doc_edits, new Document(new_id, commands2, former_states))
|
wenzelm@34827
|
143 |
}
|
wenzelm@34781
|
144 |
}
|
immler@34541
|
145 |
|
wenzelm@34858
|
146 |
|
wenzelm@34843
|
147 |
class Document(
|
wenzelm@34843
|
148 |
val id: Isar_Document.Document_ID,
|
wenzelm@34843
|
149 |
val commands: Linear_Set[Command],
|
wenzelm@34862
|
150 |
former_states: Map[Command, Command])
|
wenzelm@34843
|
151 |
{
|
wenzelm@34862
|
152 |
/* command ranges */
|
wenzelm@34843
|
153 |
|
wenzelm@34862
|
154 |
def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
|
wenzelm@34858
|
155 |
|
wenzelm@34858
|
156 |
def command_start(cmd: Command): Option[Int] =
|
wenzelm@34858
|
157 |
command_starts.find(_._1 == cmd).map(_._2)
|
wenzelm@34858
|
158 |
|
wenzelm@34858
|
159 |
def command_range(i: Int): Iterator[(Command, Int)] =
|
wenzelm@34858
|
160 |
command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
|
wenzelm@34858
|
161 |
|
wenzelm@34858
|
162 |
def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
|
wenzelm@34858
|
163 |
command_range(i) takeWhile { case (_, start) => start < j }
|
wenzelm@34858
|
164 |
|
wenzelm@34858
|
165 |
def command_at(i: Int): Option[(Command, Int)] =
|
wenzelm@34858
|
166 |
{
|
wenzelm@34858
|
167 |
val range = command_range(i)
|
wenzelm@34858
|
168 |
if (range.hasNext) Some(range.next) else None
|
wenzelm@34858
|
169 |
}
|
wenzelm@34858
|
170 |
|
wenzelm@34858
|
171 |
|
wenzelm@34858
|
172 |
/* command state assignment */
|
wenzelm@34843
|
173 |
|
wenzelm@34843
|
174 |
val assignment = Future.promise[Map[Command, Command]]
|
wenzelm@34856
|
175 |
def await_assignment { assignment.join }
|
wenzelm@34843
|
176 |
|
wenzelm@34862
|
177 |
@volatile private var tmp_states = former_states
|
wenzelm@34843
|
178 |
|
wenzelm@34843
|
179 |
def assign_states(new_states: List[(Command, Command)])
|
wenzelm@34843
|
180 |
{
|
wenzelm@34843
|
181 |
assignment.fulfill(tmp_states ++ new_states)
|
wenzelm@34843
|
182 |
tmp_states = Map()
|
wenzelm@34843
|
183 |
}
|
wenzelm@34843
|
184 |
|
wenzelm@34843
|
185 |
def current_state(cmd: Command): State =
|
wenzelm@34843
|
186 |
{
|
wenzelm@34843
|
187 |
require(assignment.is_finished)
|
wenzelm@34843
|
188 |
(assignment.join)(cmd).current_state
|
wenzelm@34843
|
189 |
}
|
wenzelm@34321
|
190 |
}
|