--- 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)
-}
--- 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)
--- 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