|
1 /* |
|
2 * Document as editable list of commands |
|
3 * |
|
4 * @author Makarius |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Document |
|
11 { |
|
12 /* command start positions */ |
|
13 |
|
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 */ |
|
26 |
|
27 def empty(id: Isar_Document.Document_ID): Document = |
|
28 { |
|
29 val doc = new Document(id, Linear_Set(), Map()) |
|
30 doc.assign_states(Nil) |
|
31 doc |
|
32 } |
|
33 |
|
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 |
|
45 type Edit = (Option[Command], Option[Command]) |
|
46 |
|
47 def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, |
|
48 edits: List[Text_Edit]): (List[Edit], Document) = |
|
49 { |
|
50 require(old_doc.assignment.is_finished) |
|
51 |
|
52 |
|
53 /* unparsed dummy commands */ |
|
54 |
|
55 def unparsed(source: String) = |
|
56 new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) |
|
57 |
|
58 def is_unparsed(command: Command) = command.id == null |
|
59 |
|
60 assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove |
|
61 |
|
62 |
|
63 /* phase 1: edit individual command source */ |
|
64 |
|
65 def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] = |
|
66 { |
|
67 eds match { |
|
68 case e :: es => |
|
69 command_starts(commands).find { // FIXME relative search! |
|
70 case (cmd, cmd_start) => |
|
71 e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length |
|
72 } match { |
|
73 case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => |
|
74 val (rest, text) = e.edit(cmd.source, cmd_start) |
|
75 val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd |
|
76 edit_text(rest.toList ::: es, new_commands) |
|
77 |
|
78 case Some((cmd, cmd_start)) => |
|
79 edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) |
|
80 |
|
81 case None => |
|
82 require(e.is_insert && e.start == 0) |
|
83 edit_text(es, commands.insert_after(None, unparsed(e.text))) |
|
84 } |
|
85 case Nil => commands |
|
86 } |
|
87 } |
|
88 |
|
89 |
|
90 /* phase 2: recover command spans */ |
|
91 |
|
92 def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = |
|
93 { |
|
94 // FIXME relative search! |
|
95 commands.elements.find(is_unparsed) match { |
|
96 case Some(first_unparsed) => |
|
97 val prefix = commands.prev(first_unparsed) |
|
98 val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList |
|
99 val suffix = commands.next(body.last) |
|
100 |
|
101 val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) |
|
102 val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) |
|
103 |
|
104 val (before_edit, spans1) = |
|
105 if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span)) |
|
106 (prefix, spans0.tail) |
|
107 else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) |
|
108 |
|
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 |
|
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) |
|
117 parse_spans(new_commands) |
|
118 |
|
119 case None => commands |
|
120 } |
|
121 } |
|
122 |
|
123 |
|
124 /* phase 3: resulting document edits */ |
|
125 |
|
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) } |
|
130 |
|
131 val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList |
|
132 val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList |
|
133 |
|
134 val doc_edits = |
|
135 removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: |
|
136 inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) |
|
137 |
|
138 val former_states = old_doc.assignment.join -- removed_commands |
|
139 |
|
140 phase0 = edits |
|
141 phase1 = commands1 |
|
142 phase2 = commands2 |
|
143 phase3 = doc_edits |
|
144 |
|
145 (doc_edits, new Document(new_id, commands2, former_states)) |
|
146 } |
|
147 result |
|
148 } |
|
149 } |
|
150 |
|
151 |
|
152 class Document( |
|
153 val id: Isar_Document.Document_ID, |
|
154 val commands: Linear_Set[Command], |
|
155 former_states: Map[Command, Command]) |
|
156 { |
|
157 /* command ranges */ |
|
158 |
|
159 def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands) |
|
160 |
|
161 def command_start(cmd: Command): Option[Int] = |
|
162 command_starts.find(_._1 == cmd).map(_._2) |
|
163 |
|
164 def command_range(i: Int): Iterator[(Command, Int)] = |
|
165 command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } |
|
166 |
|
167 def command_range(i: Int, j: Int): Iterator[(Command, Int)] = |
|
168 command_range(i) takeWhile { case (_, start) => start < j } |
|
169 |
|
170 def command_at(i: Int): Option[(Command, Int)] = |
|
171 { |
|
172 val range = command_range(i) |
|
173 if (range.hasNext) Some(range.next) else None |
|
174 } |
|
175 |
|
176 |
|
177 /* command state assignment */ |
|
178 |
|
179 val assignment = Future.promise[Map[Command, Command]] |
|
180 def await_assignment { assignment.join } |
|
181 |
|
182 @volatile private var tmp_states = former_states |
|
183 private val time0 = System.currentTimeMillis |
|
184 |
|
185 def assign_states(new_states: List[(Command, Command)]) |
|
186 { |
|
187 assignment.fulfill(tmp_states ++ new_states) |
|
188 tmp_states = Map() |
|
189 System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time") |
|
190 } |
|
191 |
|
192 def current_state(cmd: Command): Option[State] = |
|
193 { |
|
194 require(assignment.is_finished) |
|
195 (assignment.join).get(cmd).map(_.current_state) |
|
196 } |
|
197 } |