support for purge_theories;
authorwenzelm
Fri Mar 23 22:26:50 2018 +0100 (14 months ago)
changeset 67936141a93b93aa6
parent 67935 61888dd27f73
child 67937 91eb307511bb
support for purge_theories;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Fri Mar 23 21:56:22 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:26:50 2018 +0100
     1.3 @@ -86,6 +86,9 @@
     1.4        finally { Isabelle_System.rm_tree(tmp_dir) }
     1.5      }
     1.6  
     1.7 +
     1.8 +    /* theories */
     1.9 +
    1.10      def use_theories(
    1.11        theories: List[(String, Position.T)],
    1.12        qualifier: String = Sessions.DRAFT,
    1.13 @@ -134,6 +137,9 @@
    1.14  
    1.15        result.join
    1.16      }
    1.17 +
    1.18 +    def purge_theories(nodes: List[Document.Node.Name] = Nil, all: Boolean = false)
    1.19 +      : List[Document.Node.Name] = resources.purge_theories(session, if (all) None else Some(nodes))
    1.20    }
    1.21  
    1.22  
    1.23 @@ -159,6 +165,20 @@
    1.24              case _ => thys + (name -> thy)
    1.25            }
    1.26          }))
    1.27 +
    1.28 +    def remove_theories(remove: List[Document.Node.Name]): State =
    1.29 +    {
    1.30 +      require(remove.forall(name => !is_required(name)))
    1.31 +      copy(theories = theories -- remove)
    1.32 +    }
    1.33 +
    1.34 +    lazy val theories_graph: Graph[Document.Node.Name, Unit] =
    1.35 +    {
    1.36 +      val entries =
    1.37 +        for ((name, theory) <- theories.toList)
    1.38 +        yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
    1.39 +      Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering)
    1.40 +    }
    1.41    }
    1.42  
    1.43    final class Theory private[Thy_Resources](
    1.44 @@ -172,6 +192,11 @@
    1.45      def node_perspective: Document.Node.Perspective_Text =
    1.46        Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
    1.47  
    1.48 +    def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
    1.49 +      List(node_name -> Document.Node.Deps(node_header),
    1.50 +        node_name -> Document.Node.Edits(text_edits),
    1.51 +        node_name -> node_perspective)
    1.52 +
    1.53      def node_edits(old: Option[Theory]): List[Document.Edit_Text] =
    1.54      {
    1.55        val (text_edits, old_required) =
    1.56 @@ -179,12 +204,12 @@
    1.57          else (Text.Edit.replace(0, old.get.text, text), old.get.node_required)
    1.58  
    1.59        if (text_edits.isEmpty && node_required == old_required) Nil
    1.60 -      else
    1.61 -        List(node_name -> Document.Node.Deps(node_header),
    1.62 -          node_name -> Document.Node.Edits(text_edits),
    1.63 -          node_name -> node_perspective)
    1.64 +      else make_edits(text_edits)
    1.65      }
    1.66  
    1.67 +    def purge_edits: List[Document.Edit_Text] =
    1.68 +      make_edits(Text.Edit.removes(0, text))
    1.69 +
    1.70      def required(required: Boolean): Theory =
    1.71        if (required == node_required) this
    1.72        else new Theory(node_name, node_header, text, required)
    1.73 @@ -262,4 +287,24 @@
    1.74          st1.update_theories(theory_edits.map(_._2))
    1.75        })
    1.76    }
    1.77 +
    1.78 +  def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
    1.79 +    : List[Document.Node.Name] =
    1.80 +  {
    1.81 +    state.change_result(st =>
    1.82 +      {
    1.83 +        val graph = st.theories_graph
    1.84 +        val all_nodes = graph.topological_order
    1.85 +
    1.86 +        val purge =
    1.87 +          (if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))).
    1.88 +            filterNot(st.is_required(_)).toSet
    1.89 +        val purged = all_nodes.filterNot(graph.all_preds(all_nodes.filterNot(purge)).toSet)
    1.90 +
    1.91 +        val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
    1.92 +        session.update(Document.Blobs.empty, purge_edits)
    1.93 +
    1.94 +        (purged, st.remove_theories(purged))
    1.95 +      })
    1.96 +  }
    1.97  }