# HG changeset patch
# User wenzelm
# Date 1510501093 -3600
# Node ID e35ae3eeec9360ccaaddbce54ed4475bc81636fd
# Parent  383b902fe2b9a7b8e19472d943eac3ba947a12ba
load theories via PIDE document update;
theory nodes are always required;

diff -r 383b902fe2b9 -r e35ae3eeec93 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Nov 12 13:22:00 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Nov 12 16:38:13 2017 +0100
@@ -253,6 +253,12 @@
 
     def errors: List[String] = entries.flatMap(_.header.errors)
 
+    def check_errors: Dependencies =
+      errors match {
+        case Nil => this
+        case errs => error(cat_lines(errs))
+      }
+
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
       (session_base.loaded_theories /: entries)({ case (graph, entry) =>
         val name = entry.name.theory
diff -r 383b902fe2b9 -r e35ae3eeec93 src/Pure/Thy/thy_document_model.scala
--- a/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 13:22:00 2017 +0100
+++ b/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 16:38:13 2017 +0100
@@ -11,12 +11,11 @@
 {
   def read_file(session: Session,
     node_name: Document.Node.Name,
-    node_visible: Boolean = false,
-    node_required: Boolean = false): Thy_Document_Model =
+    node_visible: Boolean = false): Thy_Document_Model =
   {
     val path = node_name.path
     if (!node_name.is_theory) error("Not a theory file: " + path)
-    new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required)
+    new Thy_Document_Model(session, node_name, File.read(path), node_visible)
   }
 }
 
@@ -24,8 +23,7 @@
   val session: Session,
   val node_name: Document.Node.Name,
   val text: String,
-  val node_visible: Boolean,
-  val node_required: Boolean) extends Document.Model
+  val node_visible: Boolean) extends Document.Model
 {
   /* content */
 
@@ -42,6 +40,8 @@
   def node_header: Document.Node.Header =
     resources.check_thy_reader(node_name, Scan.char_reader(text))
 
+  def node_required: Boolean = true
+
 
   /* perspective */
 
@@ -52,6 +52,19 @@
     Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
 
 
+  /* edits */
+
+  def node_edits(old: Option[Thy_Document_Model]): List[Document.Edit_Text] =
+  {
+    val text_edits =
+      if (old.isEmpty) Text.Edit.inserts(0, text)
+      else Text.Edit.replace(0, old.get.text, text)
+
+    if (text_edits.isEmpty && old.isDefined && old.get.node_perspective == node_perspective) Nil
+    else node_edits(node_header, text_edits, node_perspective)
+  }
+
+
   /* prover session */
 
   def resources: Resources = session.resources
diff -r 383b902fe2b9 -r e35ae3eeec93 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 13:22:00 2017 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 16:38:13 2017 +0100
@@ -13,13 +13,52 @@
 
   sealed case class State(
     models: Map[Document.Node.Name, Thy_Document_Model] = Map.empty)
+  {
+    def update_models(changed: List[Thy_Document_Model]): State =
+      copy(models = models ++ changed.iterator.map(model => (model.node_name, model)))
+  }
 }
 
-class Thy_Resources(
-    val options: Options,
-    session_base: Sessions.Base,
-    log: Logger = No_Logger)
+class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger)
   extends Resources(session_base, log = log)
 {
+  resources =>
+
   private val state = Synchronized(Thy_Resources.State())
+
+  def load_theories(
+    session: Session,
+    theories: List[(String, Position.T)],
+    visible: Boolean = false,
+    qualifier: String = Sessions.DRAFT,
+    master_dir: String = ""): List[Document.Node.Name] =
+  {
+    val import_names =
+      for ((thy, pos) <- theories)
+      yield (import_name(qualifier, master_dir, thy), pos)
+
+    val dependencies = resources.dependencies(import_names).check_errors
+
+    val loaded_models =
+      dependencies.names.map(name =>
+        Thy_Document_Model.read_file(session, name, visible && import_names.contains(name)))
+
+    val edits =
+      state.change_result(st =>
+      {
+        val model_edits =
+          for {
+            model <- loaded_models
+            edits = model.node_edits(st.models.get(model.node_name))
+            if edits.nonEmpty
+          } yield model -> edits
+
+        val st1 = st.update_models(model_edits.map(_._1))
+        (model_edits.flatMap(_._2), st1)
+      })
+
+    session.update(Document.Blobs.empty, edits)
+
+    dependencies.names
+  }
 }