equal
deleted
inserted
replaced
265 } |
265 } |
266 } |
266 } |
267 } |
267 } |
268 |
268 |
269 |
269 |
270 /* perspective */ |
|
271 |
|
272 def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective) |
|
273 { |
|
274 val previous = global_state().tip_version |
|
275 val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective) |
|
276 |
|
277 val text_edits: List[Document.Edit_Text] = |
|
278 List((name, Document.Node.Perspective(text_perspective))) |
|
279 val change = |
|
280 global_state >>> |
|
281 (_.continue_history(Future.value(previous), text_edits, Future.value(version))) |
|
282 |
|
283 val assignment = global_state().the_assignment(previous).check_finished |
|
284 global_state >> (_.define_version(version, assignment)) |
|
285 global_state >>> (_.assign(version.id)) |
|
286 |
|
287 prover.get.update_perspective(previous.id, version.id, name, perspective) |
|
288 } |
|
289 |
|
290 |
|
291 /* incoming edits */ |
270 /* incoming edits */ |
292 |
271 |
293 def handle_edits(name: Document.Node.Name, |
272 def handle_edits(name: Document.Node.Name, |
294 header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]]) |
273 header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]]) |
295 //{{{ |
274 //{{{ |
463 Document.Node.Edits(List(Text.Edit.insert(0, text))), |
442 Document.Node.Edits(List(Text.Edit.insert(0, text))), |
464 Document.Node.Perspective(perspective))) |
443 Document.Node.Perspective(perspective))) |
465 reply(()) |
444 reply(()) |
466 |
445 |
467 case Edit_Node(name, header, perspective, text_edits) if prover.isDefined => |
446 case Edit_Node(name, header, perspective, text_edits) if prover.isDefined => |
468 if (text_edits.isEmpty && global_state().tip_stable && |
447 handle_edits(name, header, |
469 perspective.range.stop <= global_state().last_exec_offset(name)) |
448 List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective))) |
470 update_perspective(name, perspective) |
|
471 else |
|
472 handle_edits(name, header, |
|
473 List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective))) |
|
474 reply(()) |
449 reply(()) |
475 |
450 |
476 case Messages(msgs) => |
451 case Messages(msgs) => |
477 msgs foreach { |
452 msgs foreach { |
478 case input: Isabelle_Process.Input => |
453 case input: Isabelle_Process.Input => |