equal
deleted
inserted
replaced
397 |
397 |
398 |
398 |
399 /* theories */ |
399 /* theories */ |
400 |
400 |
401 lazy val theory_graph: Graph[Document.Node.Name, Unit] = |
401 lazy val theory_graph: Graph[Document.Node.Name, Unit] = |
402 { |
402 Document.theory_graph( |
403 val entries = |
|
404 for ((name, theory) <- theories.toList) |
403 for ((name, theory) <- theories.toList) |
405 yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))) |
404 yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_)))) |
406 Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering) |
|
407 } |
|
408 |
405 |
409 def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) |
406 def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) |
410 |
407 |
411 def insert_required(id: UUID.T, names: List[Document.Node.Name]): State = |
408 def insert_required(id: UUID.T, names: List[Document.Node.Name]): State = |
412 copy(required = (required /: names)(_.insert(_, id))) |
409 copy(required = (required /: names)(_.insert(_, id))) |