50 previous: Document.Version, |
50 previous: Document.Version, |
51 syntax_changed: List[Document.Node.Name], |
51 syntax_changed: List[Document.Node.Name], |
52 deps_changed: Boolean, |
52 deps_changed: Boolean, |
53 doc_edits: List[Document.Edit_Command], |
53 doc_edits: List[Document.Edit_Command], |
54 consolidate: List[Document.Node.Name], |
54 consolidate: List[Document.Node.Name], |
|
55 share_common_data: Boolean, |
55 version: Document.Version) |
56 version: Document.Version) |
56 |
57 |
57 case object Change_Flush |
58 case object Change_Flush |
58 |
59 |
59 |
60 |
61 |
62 |
62 //{{{ |
63 //{{{ |
63 case class Statistics(props: Properties.T) |
64 case class Statistics(props: Properties.T) |
64 case class Global_Options(options: Options) |
65 case class Global_Options(options: Options) |
65 case object Caret_Focus |
66 case object Caret_Focus |
66 case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) |
67 case class Raw_Edits( |
|
68 doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], share_common_data: Boolean) |
67 case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) |
69 case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) |
68 case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])]) |
70 case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])]) |
69 case class Commands_Changed( |
71 case class Commands_Changed( |
70 assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) |
72 assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) |
71 |
73 |
233 private case class Text_Edits( |
235 private case class Text_Edits( |
234 previous: Future[Document.Version], |
236 previous: Future[Document.Version], |
235 doc_blobs: Document.Blobs, |
237 doc_blobs: Document.Blobs, |
236 text_edits: List[Document.Edit_Text], |
238 text_edits: List[Document.Edit_Text], |
237 consolidate: List[Document.Node.Name], |
239 consolidate: List[Document.Node.Name], |
|
240 share_common_data: Boolean, |
238 version_result: Promise[Document.Version]) |
241 version_result: Promise[Document.Version]) |
239 |
242 |
240 private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) |
243 private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) |
241 { |
244 { |
242 case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) => |
245 case Text_Edits(previous, doc_blobs, text_edits, consolidate, share_common_data, version_result) => |
243 val prev = previous.get_finished |
246 val prev = previous.get_finished |
244 val change = |
247 val change = |
245 Timing.timeit("parse_change", timing) { |
248 Timing.timeit("parse_change", timing) { |
246 resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate) |
249 resources.parse_change( |
|
250 reparse_limit, prev, doc_blobs, text_edits, consolidate, share_common_data) |
247 } |
251 } |
248 version_result.fulfill(change.version) |
252 version_result.fulfill(change.version) |
249 manager.send(change) |
253 manager.send(change) |
250 true |
254 true |
251 } |
255 } |
388 /* raw edits */ |
392 /* raw edits */ |
389 |
393 |
390 def handle_raw_edits( |
394 def handle_raw_edits( |
391 doc_blobs: Document.Blobs = Document.Blobs.empty, |
395 doc_blobs: Document.Blobs = Document.Blobs.empty, |
392 edits: List[Document.Edit_Text] = Nil, |
396 edits: List[Document.Edit_Text] = Nil, |
393 consolidate: List[Document.Node.Name] = Nil) |
397 consolidate: List[Document.Node.Name] = Nil, |
|
398 share_common_data: Boolean = false) |
394 //{{{ |
399 //{{{ |
395 { |
400 { |
396 require(prover.defined) |
401 require(prover.defined) |
397 |
402 |
398 prover.get.discontinue_execution() |
403 prover.get.discontinue_execution() |
399 |
404 |
400 val previous = global_state.value.history.tip.version |
405 val previous = global_state.value.history.tip.version |
401 val version = Future.promise[Document.Version] |
406 val version = Future.promise[Document.Version] |
402 global_state.change(_.continue_history(previous, edits, version)) |
407 global_state.change(_.continue_history(previous, edits, version)) |
403 |
408 |
404 raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) |
409 raw_edits.post(Session.Raw_Edits(doc_blobs, edits, share_common_data)) |
405 change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version)) |
410 change_parser.send( |
|
411 Text_Edits(previous, doc_blobs, edits, consolidate, share_common_data, version)) |
406 } |
412 } |
407 //}}} |
413 //}}} |
408 |
414 |
409 |
415 |
410 /* resulting changes */ |
416 /* resulting changes */ |
438 edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) |
444 edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) |
439 } |
445 } |
440 |
446 |
441 val assignment = global_state.value.the_assignment(change.previous).check_finished |
447 val assignment = global_state.value.the_assignment(change.previous).check_finished |
442 global_state.change(_.define_version(change.version, assignment)) |
448 global_state.change(_.define_version(change.version, assignment)) |
|
449 |
|
450 if (change.share_common_data) { |
|
451 prover.get.protocol_command("ML_Heap.share_common_data") |
|
452 } |
443 prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) |
453 prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) |
444 resources.commit(change) |
454 resources.commit(change) |
445 } |
455 } |
446 //}}} |
456 //}}} |
447 |
457 |
608 global_options.post(Session.Global_Options(options)) |
618 global_options.post(Session.Global_Options(options)) |
609 |
619 |
610 case Cancel_Exec(exec_id) if prover.defined => |
620 case Cancel_Exec(exec_id) if prover.defined => |
611 prover.get.cancel_exec(exec_id) |
621 prover.get.cancel_exec(exec_id) |
612 |
622 |
613 case Session.Raw_Edits(doc_blobs, edits) if prover.defined => |
623 case Session.Raw_Edits(doc_blobs, edits, share_common_data) if prover.defined => |
614 handle_raw_edits(doc_blobs = doc_blobs, edits = edits) |
624 handle_raw_edits(doc_blobs = doc_blobs, edits = edits, |
|
625 share_common_data = share_common_data) |
615 |
626 |
616 case Session.Dialog_Result(id, serial, result) if prover.defined => |
627 case Session.Dialog_Result(id, serial, result) if prover.defined => |
617 prover.get.dialog_result(serial, result) |
628 prover.get.dialog_result(serial, result) |
618 handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) |
629 handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) |
619 |
630 |
701 { manager.send(Protocol_Command(name, args.toList)) } |
712 { manager.send(Protocol_Command(name, args.toList)) } |
702 |
713 |
703 def cancel_exec(exec_id: Document_ID.Exec) |
714 def cancel_exec(exec_id: Document_ID.Exec) |
704 { manager.send(Cancel_Exec(exec_id)) } |
715 { manager.send(Cancel_Exec(exec_id)) } |
705 |
716 |
706 def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) |
717 def update( |
707 { if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) } |
718 doc_blobs: Document.Blobs, |
|
719 edits: List[Document.Edit_Text], |
|
720 share_common_data: Boolean = false) |
|
721 { |
|
722 if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits, share_common_data)) |
|
723 } |
708 |
724 |
709 def update_options(options: Options) |
725 def update_options(options: Options) |
710 { manager.send_wait(Update_Options(options)) } |
726 { manager.send_wait(Update_Options(options)) } |
711 |
727 |
712 def dialog_result(id: Document_ID.Generic, serial: Long, result: String) |
728 def dialog_result(id: Document_ID.Generic, serial: Long, result: String) |