src/Pure/Thy/thy_resources.scala
changeset 67056 e35ae3eeec93
parent 67054 9498b7522a99
child 67057 0d8e4e777973
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 13:22:00 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 16:38:13 2017 +0100
     1.3 @@ -13,13 +13,52 @@
     1.4  
     1.5    sealed case class State(
     1.6      models: Map[Document.Node.Name, Thy_Document_Model] = Map.empty)
     1.7 +  {
     1.8 +    def update_models(changed: List[Thy_Document_Model]): State =
     1.9 +      copy(models = models ++ changed.iterator.map(model => (model.node_name, model)))
    1.10 +  }
    1.11  }
    1.12  
    1.13 -class Thy_Resources(
    1.14 -    val options: Options,
    1.15 -    session_base: Sessions.Base,
    1.16 -    log: Logger = No_Logger)
    1.17 +class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
    1.18    extends Resources(session_base, log = log)
    1.19  {
    1.20 +  resources =>
    1.21 +
    1.22    private val state = Synchronized(Thy_Resources.State())
    1.23 +
    1.24 +  def load_theories(
    1.25 +    session: Session,
    1.26 +    theories: List[(String, Position.T)],
    1.27 +    visible: Boolean = false,
    1.28 +    qualifier: String = Sessions.DRAFT,
    1.29 +    master_dir: String = ""): List[Document.Node.Name] =
    1.30 +  {
    1.31 +    val import_names =
    1.32 +      for ((thy, pos) <- theories)
    1.33 +      yield (import_name(qualifier, master_dir, thy), pos)
    1.34 +
    1.35 +    val dependencies = resources.dependencies(import_names).check_errors
    1.36 +
    1.37 +    val loaded_models =
    1.38 +      dependencies.names.map(name =>
    1.39 +        Thy_Document_Model.read_file(session, name, visible && import_names.contains(name)))
    1.40 +
    1.41 +    val edits =
    1.42 +      state.change_result(st =>
    1.43 +      {
    1.44 +        val model_edits =
    1.45 +          for {
    1.46 +            model <- loaded_models
    1.47 +            edits = model.node_edits(st.models.get(model.node_name))
    1.48 +            if edits.nonEmpty
    1.49 +          } yield model -> edits
    1.50 +
    1.51 +        val st1 = st.update_models(model_edits.map(_._1))
    1.52 +        (model_edits.flatMap(_._2), st1)
    1.53 +      })
    1.54 +
    1.55 +    session.update(Document.Blobs.empty, edits)
    1.56 +
    1.57 +    dependencies.names
    1.58 +  }
    1.59  }