561 require(remove.forall(name => !is_required(name))) |
561 require(remove.forall(name => !is_required(name))) |
562 copy(theories = theories -- remove) |
562 copy(theories = theories -- remove) |
563 } |
563 } |
564 |
564 |
565 def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
565 def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
566 : State = |
566 : (List[Document.Edit_Text], State) = |
567 { |
567 { |
568 val st1 = remove_required(id, theories) |
568 val st1 = remove_required(id, theories) |
569 val theory_edits = |
569 val theory_edits = |
570 for { |
570 for { |
571 node_name <- theories |
571 node_name <- theories |
574 yield { |
574 yield { |
575 val theory1 = theory.required(st1.is_required(node_name)) |
575 val theory1 = theory.required(st1.is_required(node_name)) |
576 val edits = theory1.node_edits(Some(theory)) |
576 val edits = theory1.node_edits(Some(theory)) |
577 (edits, (node_name, theory1)) |
577 (edits, (node_name, theory1)) |
578 } |
578 } |
579 session.update(doc_blobs, theory_edits.flatMap(_._1)) |
579 (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2))) |
580 st1.update_theories(theory_edits.map(_._2)) |
|
581 } |
580 } |
582 |
581 |
583 def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) |
582 def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) |
584 : ((List[Document.Node.Name], List[Document.Node.Name]), State) = |
583 : ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) = |
585 { |
584 { |
586 val all_nodes = theory_graph.topological_order |
585 val all_nodes = theory_graph.topological_order |
587 val purge = nodes.getOrElse(all_nodes).filterNot(is_required(_)).toSet |
586 val purge = nodes.getOrElse(all_nodes).filterNot(is_required(_)).toSet |
588 |
587 |
589 val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet |
588 val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet |
590 val (retained, purged) = all_nodes.partition(retain) |
589 val (retained, purged) = all_nodes.partition(retain) |
591 |
|
592 val purge_edits = purged.flatMap(name => theories(name).purge_edits) |
590 val purge_edits = purged.flatMap(name => theories(name).purge_edits) |
593 session.update(doc_blobs, purge_edits) |
591 |
594 |
592 ((purged, retained, purge_edits), remove_theories(purged)) |
595 ((purged, retained), remove_theories(purged)) |
|
596 } |
593 } |
597 } |
594 } |
598 } |
595 } |
599 |
596 |
600 class Resources private[Headless]( |
597 class Resources private[Headless]( |
689 }) |
686 }) |
690 } |
687 } |
691 |
688 |
692 def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
689 def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
693 { |
690 { |
694 state.change(_.unload_theories(session, id, theories)) |
691 state.change(st => |
|
692 { |
|
693 val (edits, st1) = st.unload_theories(session, id, theories) |
|
694 session.update(st.doc_blobs, edits) |
|
695 st1 |
|
696 }) |
695 } |
697 } |
696 |
698 |
697 def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
699 def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
698 { |
700 { |
699 state.change(st => |
701 state.change(st => |
700 st.unload_theories(session, id, theories).purge_theories(session, None)._2) |
702 { |
|
703 val (edits1, st1) = st.unload_theories(session, id, theories) |
|
704 val ((_, _, edits2), st2) = st1.purge_theories(session, None) |
|
705 session.update(st.doc_blobs, edits1 ::: edits2) |
|
706 st2 |
|
707 }) |
701 } |
708 } |
702 |
709 |
703 def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) |
710 def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) |
704 : (List[Document.Node.Name], List[Document.Node.Name]) = |
711 : (List[Document.Node.Name], List[Document.Node.Name]) = |
705 { |
712 { |
706 state.change_result(_.purge_theories(session, nodes)) |
713 state.change_result(st => |
|
714 { |
|
715 val ((purged, retained, _), st1) = st.purge_theories(session, nodes) |
|
716 ((purged, retained), st1) |
|
717 }) |
707 } |
718 } |
708 } |
719 } |
709 } |
720 } |