223 case Nil => commands |
223 case Nil => commands |
224 } |
224 } |
225 } |
225 } |
226 |
226 |
227 |
227 |
|
228 /* inlined files */ |
|
229 |
|
230 private def find_file(tokens: List[Token]): Option[String] = |
|
231 { |
|
232 def clean(toks: List[Token]): List[Token] = |
|
233 toks match { |
|
234 case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts) |
|
235 case t :: ts => t :: clean(ts) |
|
236 case Nil => Nil |
|
237 } |
|
238 val clean_tokens = clean(tokens.filter(_.is_proper)) |
|
239 clean_tokens.reverse.find(_.is_name).map(_.content) |
|
240 } |
|
241 |
|
242 def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] = |
|
243 syntax.thy_load(span) match { |
|
244 case Some(exts) => |
|
245 find_file(span) match { |
|
246 case Some(file) => |
|
247 if (exts.isEmpty) List(file) |
|
248 else exts.map(ext => file + "." + ext) |
|
249 case None => Nil |
|
250 } |
|
251 case None => Nil |
|
252 } |
|
253 |
|
254 def resolve_files( |
|
255 syntax: Outer_Syntax, |
|
256 all_blobs: Map[Document.Node.Name, Bytes], |
|
257 name: Document.Node.Name, |
|
258 span: List[Token]): Command.Blobs = |
|
259 { |
|
260 val files = span_files(syntax, span) |
|
261 files.map(file => { |
|
262 // FIXME proper thy_load append |
|
263 val file_name = Document.Node.Name(name.dir + file, name.dir, "") |
|
264 (file_name, all_blobs.get(file_name).map(_.sha1_digest)) |
|
265 }) |
|
266 } |
|
267 |
|
268 |
228 /* reparse range of command spans */ |
269 /* reparse range of command spans */ |
229 |
270 |
230 @tailrec private def chop_common( |
271 @tailrec private def chop_common( |
231 cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) = |
272 cmds: List[Command], spans: List[(List[Token], Command.Blobs)]) |
|
273 : (List[Command], List[(List[Token], Command.Blobs)]) = |
232 (cmds, spans) match { |
274 (cmds, spans) match { |
233 case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss) |
275 case (c :: cs, (span, blobs) :: ps) if c.span == span && c.blobs == blobs => |
|
276 chop_common(cs, ps) |
234 case _ => (cmds, spans) |
277 case _ => (cmds, spans) |
235 } |
278 } |
236 |
279 |
237 private def reparse_spans( |
280 private def reparse_spans( |
238 syntax: Outer_Syntax, |
281 syntax: Outer_Syntax, |
|
282 all_blobs: Map[Document.Node.Name, Bytes], |
239 name: Document.Node.Name, |
283 name: Document.Node.Name, |
240 commands: Linear_Set[Command], |
284 commands: Linear_Set[Command], |
241 first: Command, last: Command): Linear_Set[Command] = |
285 first: Command, last: Command): Linear_Set[Command] = |
242 { |
286 { |
243 val cmds0 = commands.iterator(first, last).toList |
287 val cmds0 = commands.iterator(first, last).toList |
244 val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)) |
288 val spans0 = |
|
289 parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)). |
|
290 map(span => (span, resolve_files(syntax, all_blobs, name, span))) |
245 |
291 |
246 val (cmds1, spans1) = chop_common(cmds0, spans0) |
292 val (cmds1, spans1) = chop_common(cmds0, spans0) |
247 |
293 |
248 val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse) |
294 val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse) |
249 val cmds2 = rev_cmds2.reverse |
295 val cmds2 = rev_cmds2.reverse |
254 assert(spans2.isEmpty) |
300 assert(spans2.isEmpty) |
255 commands |
301 commands |
256 case cmd :: _ => |
302 case cmd :: _ => |
257 val hook = commands.prev(cmd) |
303 val hook = commands.prev(cmd) |
258 val inserted = |
304 val inserted = |
259 spans2.map(span => Command(Document_ID.make(), name, span, syntax.thy_load(span))) |
305 spans2.map({ case (span, blobs) => Command(Document_ID.make(), name, span, blobs) }) |
260 (commands /: cmds2)(_ - _).append_after(hook, inserted) |
306 (commands /: cmds2)(_ - _).append_after(hook, inserted) |
261 } |
307 } |
262 } |
308 } |
263 |
309 |
264 |
310 |
265 /* recover command spans after edits */ |
311 /* recover command spans after edits */ |
266 |
312 |
267 // FIXME somewhat slow |
313 // FIXME somewhat slow |
268 private def recover_spans( |
314 private def recover_spans( |
269 syntax: Outer_Syntax, |
315 syntax: Outer_Syntax, |
|
316 all_blobs: Map[Document.Node.Name, Bytes], |
270 name: Document.Node.Name, |
317 name: Document.Node.Name, |
271 perspective: Command.Perspective, |
318 perspective: Command.Perspective, |
272 commands: Linear_Set[Command]): Linear_Set[Command] = |
319 commands: Linear_Set[Command]): Linear_Set[Command] = |
273 { |
320 { |
274 val visible = perspective.commands.toSet |
321 val visible = perspective.commands.toSet |
280 @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] = |
327 @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] = |
281 cmds.find(_.is_unparsed) match { |
328 cmds.find(_.is_unparsed) match { |
282 case Some(first_unparsed) => |
329 case Some(first_unparsed) => |
283 val first = next_invisible_command(cmds.reverse, first_unparsed) |
330 val first = next_invisible_command(cmds.reverse, first_unparsed) |
284 val last = next_invisible_command(cmds, first_unparsed) |
331 val last = next_invisible_command(cmds, first_unparsed) |
285 recover(reparse_spans(syntax, name, cmds, first, last)) |
332 recover(reparse_spans(syntax, all_blobs, name, cmds, first, last)) |
286 case None => cmds |
333 case None => cmds |
287 } |
334 } |
288 recover(commands) |
335 recover(commands) |
289 } |
336 } |
290 |
337 |
291 |
338 |
292 /* consolidate unfinished spans */ |
339 /* consolidate unfinished spans */ |
293 |
340 |
294 private def consolidate_spans( |
341 private def consolidate_spans( |
295 syntax: Outer_Syntax, |
342 syntax: Outer_Syntax, |
|
343 all_blobs: Map[Document.Node.Name, Bytes], |
296 reparse_limit: Int, |
344 reparse_limit: Int, |
297 name: Document.Node.Name, |
345 name: Document.Node.Name, |
298 perspective: Command.Perspective, |
346 perspective: Command.Perspective, |
299 commands: Linear_Set[Command]): Linear_Set[Command] = |
347 commands: Linear_Set[Command]): Linear_Set[Command] = |
300 { |
348 { |
331 |
379 |
332 removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) ::: |
380 removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) ::: |
333 inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd))) |
381 inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd))) |
334 } |
382 } |
335 |
383 |
336 private def text_edit(syntax: Outer_Syntax, reparse_limit: Int, |
384 private def text_edit( |
|
385 syntax: Outer_Syntax, |
|
386 all_blobs: Map[Document.Node.Name, Bytes], |
|
387 reparse_limit: Int, |
337 node: Document.Node, edit: Document.Edit_Text): Document.Node = |
388 node: Document.Node, edit: Document.Edit_Text): Document.Node = |
338 { |
389 { |
339 edit match { |
390 edit match { |
340 case (_, Document.Node.Clear()) => node.clear |
391 case (_, Document.Node.Clear()) => node.clear |
341 |
392 |
342 case (name, Document.Node.Edits(text_edits)) => |
393 case (name, Document.Node.Edits(text_edits)) => |
343 val commands0 = node.commands |
394 val commands0 = node.commands |
344 val commands1 = edit_text(text_edits, commands0) |
395 val commands1 = edit_text(text_edits, commands0) |
345 val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1) |
396 val commands2 = recover_spans(syntax, all_blobs, name, node.perspective.visible, commands1) |
346 node.update_commands(commands2) |
397 node.update_commands(commands2) |
347 |
398 |
348 case (_, Document.Node.Deps(_)) => node |
399 case (_, Document.Node.Deps(_)) => node |
349 |
400 |
350 case (name, Document.Node.Perspective(required, text_perspective, overlays)) => |
401 case (name, Document.Node.Perspective(required, text_perspective, overlays)) => |
352 val perspective: Document.Node.Perspective_Command = |
403 val perspective: Document.Node.Perspective_Command = |
353 Document.Node.Perspective(required, visible_overlay, overlays) |
404 Document.Node.Perspective(required, visible_overlay, overlays) |
354 if (node.same_perspective(perspective)) node |
405 if (node.same_perspective(perspective)) node |
355 else |
406 else |
356 node.update_perspective(perspective).update_commands( |
407 node.update_perspective(perspective).update_commands( |
357 consolidate_spans(syntax, reparse_limit, name, visible, node.commands)) |
408 consolidate_spans(syntax, all_blobs, reparse_limit, name, visible, node.commands)) |
358 |
409 |
359 case (_, Document.Node.Blob(blob)) => node.update_blob(blob) |
410 case (_, Document.Node.Blob(_)) => node |
360 } |
411 } |
361 } |
412 } |
362 |
413 |
363 def text_edits( |
414 def text_edits( |
364 base_syntax: Outer_Syntax, |
415 base_syntax: Outer_Syntax, |
375 |
426 |
376 val node_edits = |
427 val node_edits = |
377 (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) |
428 (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) |
378 .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? |
429 .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? |
379 |
430 |
|
431 val all_blobs: Map[Document.Node.Name, Bytes] = |
|
432 (Map.empty[Document.Node.Name, Bytes] /: node_edits) { |
|
433 case (bs1, (_, es)) => (bs1 /: es) { |
|
434 case (bs, (name, Document.Node.Blob(blob))) => bs + (name -> blob) |
|
435 case (bs, _) => bs |
|
436 } |
|
437 } |
|
438 |
380 node_edits foreach { |
439 node_edits foreach { |
381 case (name, edits) => |
440 case (name, edits) => |
382 val node = nodes(name) |
441 val node = nodes(name) |
383 val commands = node.commands |
442 val commands = node.commands |
384 |
443 |
385 val node1 = |
444 val node1 = |
386 if (reparse_set(name) && !commands.isEmpty) |
445 if (reparse_set(name) && !commands.isEmpty) |
387 node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last)) |
446 node.update_commands( |
|
447 reparse_spans(syntax, all_blobs, name, commands, commands.head, commands.last)) |
388 else node |
448 else node |
389 val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _)) |
449 val node2 = (node1 /: edits)(text_edit(syntax, all_blobs, reparse_limit, _, _)) |
390 |
450 |
391 if (!(node.same_perspective(node2.perspective))) |
451 if (!(node.same_perspective(node2.perspective))) |
392 doc_edits += (name -> node2.perspective) |
452 doc_edits += (name -> node2.perspective) |
393 |
453 |
394 doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) |
454 doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) |