load theories via PIDE document update;
authorwenzelm
Sun Nov 12 16:38:13 2017 +0100 (18 months ago)
changeset 67056e35ae3eeec93
parent 67055 383b902fe2b9
child 67057 0d8e4e777973
load theories via PIDE document update;
theory nodes are always required;
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_document_model.scala
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Nov 12 13:22:00 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Nov 12 16:38:13 2017 +0100
     1.3 @@ -253,6 +253,12 @@
     1.4  
     1.5      def errors: List[String] = entries.flatMap(_.header.errors)
     1.6  
     1.7 +    def check_errors: Dependencies =
     1.8 +      errors match {
     1.9 +        case Nil => this
    1.10 +        case errs => error(cat_lines(errs))
    1.11 +      }
    1.12 +
    1.13      lazy val loaded_theories: Graph[String, Outer_Syntax] =
    1.14        (session_base.loaded_theories /: entries)({ case (graph, entry) =>
    1.15          val name = entry.name.theory
     2.1 --- a/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 13:22:00 2017 +0100
     2.2 +++ b/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 16:38:13 2017 +0100
     2.3 @@ -11,12 +11,11 @@
     2.4  {
     2.5    def read_file(session: Session,
     2.6      node_name: Document.Node.Name,
     2.7 -    node_visible: Boolean = false,
     2.8 -    node_required: Boolean = false): Thy_Document_Model =
     2.9 +    node_visible: Boolean = false): Thy_Document_Model =
    2.10    {
    2.11      val path = node_name.path
    2.12      if (!node_name.is_theory) error("Not a theory file: " + path)
    2.13 -    new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required)
    2.14 +    new Thy_Document_Model(session, node_name, File.read(path), node_visible)
    2.15    }
    2.16  }
    2.17  
    2.18 @@ -24,8 +23,7 @@
    2.19    val session: Session,
    2.20    val node_name: Document.Node.Name,
    2.21    val text: String,
    2.22 -  val node_visible: Boolean,
    2.23 -  val node_required: Boolean) extends Document.Model
    2.24 +  val node_visible: Boolean) extends Document.Model
    2.25  {
    2.26    /* content */
    2.27  
    2.28 @@ -42,6 +40,8 @@
    2.29    def node_header: Document.Node.Header =
    2.30      resources.check_thy_reader(node_name, Scan.char_reader(text))
    2.31  
    2.32 +  def node_required: Boolean = true
    2.33 +
    2.34  
    2.35    /* perspective */
    2.36  
    2.37 @@ -52,6 +52,19 @@
    2.38      Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
    2.39  
    2.40  
    2.41 +  /* edits */
    2.42 +
    2.43 +  def node_edits(old: Option[Thy_Document_Model]): List[Document.Edit_Text] =
    2.44 +  {
    2.45 +    val text_edits =
    2.46 +      if (old.isEmpty) Text.Edit.inserts(0, text)
    2.47 +      else Text.Edit.replace(0, old.get.text, text)
    2.48 +
    2.49 +    if (text_edits.isEmpty && old.isDefined && old.get.node_perspective == node_perspective) Nil
    2.50 +    else node_edits(node_header, text_edits, node_perspective)
    2.51 +  }
    2.52 +
    2.53 +
    2.54    /* prover session */
    2.55  
    2.56    def resources: Resources = session.resources
     3.1 --- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 13:22:00 2017 +0100
     3.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 16:38:13 2017 +0100
     3.3 @@ -13,13 +13,52 @@
     3.4  
     3.5    sealed case class State(
     3.6      models: Map[Document.Node.Name, Thy_Document_Model] = Map.empty)
     3.7 +  {
     3.8 +    def update_models(changed: List[Thy_Document_Model]): State =
     3.9 +      copy(models = models ++ changed.iterator.map(model => (model.node_name, model)))
    3.10 +  }
    3.11  }
    3.12  
    3.13 -class Thy_Resources(
    3.14 -    val options: Options,
    3.15 -    session_base: Sessions.Base,
    3.16 -    log: Logger = No_Logger)
    3.17 +class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
    3.18    extends Resources(session_base, log = log)
    3.19  {
    3.20 +  resources =>
    3.21 +
    3.22    private val state = Synchronized(Thy_Resources.State())
    3.23 +
    3.24 +  def load_theories(
    3.25 +    session: Session,
    3.26 +    theories: List[(String, Position.T)],
    3.27 +    visible: Boolean = false,
    3.28 +    qualifier: String = Sessions.DRAFT,
    3.29 +    master_dir: String = ""): List[Document.Node.Name] =
    3.30 +  {
    3.31 +    val import_names =
    3.32 +      for ((thy, pos) <- theories)
    3.33 +      yield (import_name(qualifier, master_dir, thy), pos)
    3.34 +
    3.35 +    val dependencies = resources.dependencies(import_names).check_errors
    3.36 +
    3.37 +    val loaded_models =
    3.38 +      dependencies.names.map(name =>
    3.39 +        Thy_Document_Model.read_file(session, name, visible && import_names.contains(name)))
    3.40 +
    3.41 +    val edits =
    3.42 +      state.change_result(st =>
    3.43 +      {
    3.44 +        val model_edits =
    3.45 +          for {
    3.46 +            model <- loaded_models
    3.47 +            edits = model.node_edits(st.models.get(model.node_name))
    3.48 +            if edits.nonEmpty
    3.49 +          } yield model -> edits
    3.50 +
    3.51 +        val st1 = st.update_models(model_edits.map(_._1))
    3.52 +        (model_edits.flatMap(_._2), st1)
    3.53 +      })
    3.54 +
    3.55 +    session.update(Document.Blobs.empty, edits)
    3.56 +
    3.57 +    dependencies.names
    3.58 +  }
    3.59  }