# HG changeset patch
# User wenzelm
# Date 1510512142 -3600
# Node ID 03d4954c68bbaff41e15eb15717058f410ef39a0
# Parent  0d8e4e777973a5a90e58fdc6e6b0edee9018595b
simplified: eliminated pointless Thy_Document_Model;

diff -r 0d8e4e777973 -r 03d4954c68bb src/Pure/Thy/thy_document_model.scala
--- a/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 16:56:39 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-/*  Title:      Pure/Thy/thy_document_model.scala
-    Author:     Makarius
-
-Document model for theory files: no blobs, no edits, no overlays.
-*/
-
-package isabelle
-
-
-object Thy_Document_Model
-{
-  def read_file(session: Session, node_name: Document.Node.Name): 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))
-  }
-}
-
-final class Thy_Document_Model private(
-  val session: Session,
-  val node_name: Document.Node.Name,
-  val text: String) extends Document.Model
-{
-  /* content */
-
-  def get_text(range: Text.Range): Option[String] =
-    if (0 <= range.start && range.stop <= text.length) Some(range.substring(text)) else None
-
-  def get_blob: Option[Document.Blob] = None
-
-  def bibtex_entries: List[Text.Info[String]] = Nil
-
-
-  /* header */
-
-  def node_header: Document.Node.Header =
-    resources.check_thy_reader(node_name, Scan.char_reader(text))
-
-  def node_required: Boolean = true
-
-
-  /* perspective */
-
-  def node_perspective: Document.Node.Perspective_Text =
-    Document.Node.Perspective(node_required, Text.Perspective.full, 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) Nil
-    else node_edits(node_header, text_edits, node_perspective)
-  }
-
-
-  /* prover session */
-
-  def resources: Resources = session.resources
-
-  def is_stable: Boolean = true
-  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits = Nil)
-}
diff -r 0d8e4e777973 -r 03d4954c68bb src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sun Nov 12 16:56:39 2017 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sun Nov 12 19:42:22 2017 +0100
@@ -11,11 +11,30 @@
 {
   /* internal state */
 
-  sealed case class State(
-    models: Map[Document.Node.Name, Thy_Document_Model] = Map.empty)
+  sealed case class State(theories: Map[Document.Node.Name, Theory] = Map.empty)
+
+  final class Theory private[Thy_Resources](
+    val node_name: Document.Node.Name,
+    val node_header: Document.Node.Header,
+    val text: String)
   {
-    def update_models(changed: List[Thy_Document_Model]): State =
-      copy(models = models ++ changed.iterator.map(model => (model.node_name, model)))
+    override def toString: String = node_name.toString
+
+    def node_perspective: Document.Node.Perspective_Text =
+      Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)
+
+    def node_edits(old: Option[Theory]): 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) Nil
+      else
+        List(node_name -> Document.Node.Deps(node_header),
+          node_name -> Document.Node.Edits(text_edits),
+          node_name -> node_perspective)
+    }
   }
 }
 
@@ -26,6 +45,16 @@
 
   private val state = Synchronized(Thy_Resources.State())
 
+  def read_thy(node_name: Document.Node.Name): Thy_Resources.Theory =
+  {
+    val path = node_name.path
+    if (!node_name.is_theory) error("Not a theory file: " + path)
+
+    val text = File.read(path)
+    val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
+    new Thy_Resources.Theory(node_name, node_header, text)
+  }
+
   def load_theories(
     session: Session,
     theories: List[(String, Position.T)],
@@ -37,20 +66,21 @@
       yield (import_name(qualifier, master_dir, thy), pos)
 
     val dependencies = resources.dependencies(import_names).check_errors
-    val loaded_models = dependencies.names.map(Thy_Document_Model.read_file(session, _))
+    val loaded_theories = dependencies.names.map(read_thy(_))
 
     val edits =
       state.change_result(st =>
       {
-        val model_edits =
+        val theory_edits =
           for {
-            model <- loaded_models
-            edits = model.node_edits(st.models.get(model.node_name))
+            theory <- loaded_theories
+            node_name = theory.node_name
+            edits = theory.node_edits(st.theories.get(node_name))
             if edits.nonEmpty
-          } yield model -> edits
+          } yield ((node_name, theory), edits)
 
-        val st1 = st.update_models(model_edits.map(_._1))
-        (model_edits.flatMap(_._2), st1)
+        val st1 = st.copy(theories = st.theories ++ theory_edits.map(_._1))
+        (theory_edits.flatMap(_._2), st1)
       })
     session.update(Document.Blobs.empty, edits)
 
diff -r 0d8e4e777973 -r 03d4954c68bb src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Nov 12 16:56:39 2017 +0100
+++ b/src/Pure/build-jars	Sun Nov 12 19:42:22 2017 +0100
@@ -128,7 +128,6 @@
   Thy/html.scala
   Thy/present.scala
   Thy/sessions.scala
-  Thy/thy_document_model.scala
   Thy/thy_header.scala
   Thy/thy_resources.scala
   Thy/thy_syntax.scala