260 def resolve_files( |
260 def resolve_files( |
261 resources: Resources, |
261 resources: Resources, |
262 syntax: Outer_Syntax, |
262 syntax: Outer_Syntax, |
263 node_name: Document.Node.Name, |
263 node_name: Document.Node.Name, |
264 span: List[Token], |
264 span: List[Token], |
265 doc_blobs_default: Document.Blobs) |
265 get_blob: Document.Node.Name => Option[Document.Blob]) |
266 : List[Command.Blob] = |
266 : List[Command.Blob] = |
267 { |
267 { |
268 span_files(syntax, span).map(file_name => |
268 span_files(syntax, span).map(file_name => |
269 Exn.capture { |
269 Exn.capture { |
270 val name = |
270 val name = |
271 Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name))) |
271 Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name))) |
272 val blob = doc_blobs_default.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file))) |
272 val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.file))) |
273 (name, blob) |
273 (name, blob) |
274 }) |
274 }) |
275 } |
275 } |
276 |
276 |
277 |
277 |
290 } |
290 } |
291 |
291 |
292 private def reparse_spans( |
292 private def reparse_spans( |
293 resources: Resources, |
293 resources: Resources, |
294 syntax: Outer_Syntax, |
294 syntax: Outer_Syntax, |
295 doc_blobs_default: Document.Blobs, |
295 get_blob: Document.Node.Name => Option[Document.Blob], |
296 name: Document.Node.Name, |
296 name: Document.Node.Name, |
297 commands: Linear_Set[Command], |
297 commands: Linear_Set[Command], |
298 first: Command, last: Command): Linear_Set[Command] = |
298 first: Command, last: Command): Linear_Set[Command] = |
299 { |
299 { |
300 val cmds0 = commands.iterator(first, last).toList |
300 val cmds0 = commands.iterator(first, last).toList |
301 val blobs_spans0 = |
301 val blobs_spans0 = |
302 parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)). |
302 parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)). |
303 map(span => (resolve_files(resources, syntax, name, span, doc_blobs_default), span)) |
303 map(span => (resolve_files(resources, syntax, name, span, get_blob), span)) |
304 |
304 |
305 val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0) |
305 val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0) |
306 |
306 |
307 val (rev_cmds2, rev_blobs_spans2) = chop_common(cmds1.reverse, blobs_spans1.reverse) |
307 val (rev_cmds2, rev_blobs_spans2) = chop_common(cmds1.reverse, blobs_spans1.reverse) |
308 val cmds2 = rev_cmds2.reverse |
308 val cmds2 = rev_cmds2.reverse |
325 |
325 |
326 // FIXME somewhat slow |
326 // FIXME somewhat slow |
327 private def recover_spans( |
327 private def recover_spans( |
328 resources: Resources, |
328 resources: Resources, |
329 syntax: Outer_Syntax, |
329 syntax: Outer_Syntax, |
330 doc_blobs_default: Document.Blobs, |
330 get_blob: Document.Node.Name => Option[Document.Blob], |
331 name: Document.Node.Name, |
331 name: Document.Node.Name, |
332 perspective: Command.Perspective, |
332 perspective: Command.Perspective, |
333 commands: Linear_Set[Command]): Linear_Set[Command] = |
333 commands: Linear_Set[Command]): Linear_Set[Command] = |
334 { |
334 { |
335 val visible = perspective.commands.toSet |
335 val visible = perspective.commands.toSet |
341 @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] = |
341 @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] = |
342 cmds.find(_.is_unparsed) match { |
342 cmds.find(_.is_unparsed) match { |
343 case Some(first_unparsed) => |
343 case Some(first_unparsed) => |
344 val first = next_invisible_command(cmds.reverse, first_unparsed) |
344 val first = next_invisible_command(cmds.reverse, first_unparsed) |
345 val last = next_invisible_command(cmds, first_unparsed) |
345 val last = next_invisible_command(cmds, first_unparsed) |
346 recover(reparse_spans(resources, syntax, doc_blobs_default, name, cmds, first, last)) |
346 recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last)) |
347 case None => cmds |
347 case None => cmds |
348 } |
348 } |
349 recover(commands) |
349 recover(commands) |
350 } |
350 } |
351 |
351 |
353 /* consolidate unfinished spans */ |
353 /* consolidate unfinished spans */ |
354 |
354 |
355 private def consolidate_spans( |
355 private def consolidate_spans( |
356 resources: Resources, |
356 resources: Resources, |
357 syntax: Outer_Syntax, |
357 syntax: Outer_Syntax, |
358 doc_blobs_default: Document.Blobs, |
358 get_blob: Document.Node.Name => Option[Document.Blob], |
359 reparse_limit: Int, |
359 reparse_limit: Int, |
360 name: Document.Node.Name, |
360 name: Document.Node.Name, |
361 perspective: Command.Perspective, |
361 perspective: Command.Perspective, |
362 commands: Linear_Set[Command]): Linear_Set[Command] = |
362 commands: Linear_Set[Command]): Linear_Set[Command] = |
363 { |
363 { |
373 var i = 0 |
373 var i = 0 |
374 while (i < reparse_limit && it.hasNext) { |
374 while (i < reparse_limit && it.hasNext) { |
375 last = it.next |
375 last = it.next |
376 i += last.length |
376 i += last.length |
377 } |
377 } |
378 reparse_spans( |
378 reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last) |
379 resources, syntax, doc_blobs_default, name, commands, first_unfinished, last) |
|
380 case None => commands |
379 case None => commands |
381 } |
380 } |
382 case None => commands |
381 case None => commands |
383 } |
382 } |
384 } |
383 } |
398 } |
397 } |
399 |
398 |
400 private def text_edit( |
399 private def text_edit( |
401 resources: Resources, |
400 resources: Resources, |
402 syntax: Outer_Syntax, |
401 syntax: Outer_Syntax, |
403 doc_blobs_default: Document.Blobs, |
402 get_blob: Document.Node.Name => Option[Document.Blob], |
404 reparse_limit: Int, |
403 reparse_limit: Int, |
405 node: Document.Node, edit: Document.Edit_Text): Document.Node = |
404 node: Document.Node, edit: Document.Edit_Text): Document.Node = |
406 { |
405 { |
407 edit match { |
406 edit match { |
408 case (_, Document.Node.Clear()) => node.clear |
407 case (_, Document.Node.Clear()) => node.clear |
412 case (name, Document.Node.Edits(text_edits)) => |
411 case (name, Document.Node.Edits(text_edits)) => |
413 if (name.is_theory) { |
412 if (name.is_theory) { |
414 val commands0 = node.commands |
413 val commands0 = node.commands |
415 val commands1 = edit_text(text_edits, commands0) |
414 val commands1 = edit_text(text_edits, commands0) |
416 val commands2 = |
415 val commands2 = |
417 recover_spans( |
416 recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1) |
418 resources, syntax, doc_blobs_default, name, node.perspective.visible, commands1) |
|
419 node.update_commands(commands2) |
417 node.update_commands(commands2) |
420 } |
418 } |
421 else node |
419 else node |
422 |
420 |
423 case (_, Document.Node.Deps(_)) => node |
421 case (_, Document.Node.Deps(_)) => node |
427 val perspective: Document.Node.Perspective_Command = |
425 val perspective: Document.Node.Perspective_Command = |
428 Document.Node.Perspective(required, visible_overlay, overlays) |
426 Document.Node.Perspective(required, visible_overlay, overlays) |
429 if (node.same_perspective(perspective)) node |
427 if (node.same_perspective(perspective)) node |
430 else |
428 else |
431 node.update_perspective(perspective).update_commands( |
429 node.update_perspective(perspective).update_commands( |
432 consolidate_spans(resources, syntax, doc_blobs_default, reparse_limit, |
430 consolidate_spans(resources, syntax, get_blob, reparse_limit, |
433 name, visible, node.commands)) |
431 name, visible, node.commands)) |
434 } |
432 } |
435 } |
433 } |
436 |
434 |
437 def parse_change( |
435 def parse_change( |
439 reparse_limit: Int, |
437 reparse_limit: Int, |
440 previous: Document.Version, |
438 previous: Document.Version, |
441 doc_blobs: Document.Blobs, |
439 doc_blobs: Document.Blobs, |
442 edits: List[Document.Edit_Text]): Session.Change = |
440 edits: List[Document.Edit_Text]): Session.Change = |
443 { |
441 { |
|
442 def get_blob(name: Document.Node.Name) = |
|
443 doc_blobs.get(name) orElse previous.nodes(name).get_blob |
|
444 |
444 val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) = |
445 val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) = |
445 header_edits(resources.base_syntax, previous, edits) |
446 header_edits(resources.base_syntax, previous, edits) |
446 |
447 |
447 val (doc_edits, version) = |
448 val (doc_edits, version) = |
448 if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes)) |
449 if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes)) |
471 val commands = node.commands |
470 val commands = node.commands |
472 |
471 |
473 val node1 = |
472 val node1 = |
474 if (reparse_set(name) && !commands.isEmpty) |
473 if (reparse_set(name) && !commands.isEmpty) |
475 node.update_commands( |
474 node.update_commands( |
476 reparse_spans(resources, syntax, doc_blobs_default, |
475 reparse_spans(resources, syntax, get_blob, |
477 name, commands, commands.head, commands.last)) |
476 name, commands, commands.head, commands.last)) |
478 else node |
477 else node |
479 val node2 = |
478 val node2 = |
480 (node1 /: edits)(text_edit(resources, syntax, doc_blobs_default, reparse_limit, _, _)) |
479 (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _)) |
481 |
480 |
482 if (!(node.same_perspective(node2.perspective))) |
481 if (!(node.same_perspective(node2.perspective))) |
483 doc_edits += (name -> node2.perspective) |
482 doc_edits += (name -> node2.perspective) |
484 |
483 |
485 doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) |
484 doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) |