# HG changeset patch
# User wenzelm
# Date 1509985292 -3600
# Node ID 57d58c3cf16bd100b6cde7575d6fb6197f1e085b
# Parent  1a9e2a2bf251a5eb2d1c84222fb099af1be79db7
minimal document model for theory files;

diff -r 1a9e2a2bf251 -r 57d58c3cf16b src/Pure/Thy/thy_document_model.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_document_model.scala	Mon Nov 06 17:21:32 2017 +0100
@@ -0,0 +1,61 @@
+/*  Title:      Pure/Thy/thy_document_model.scala
+    Author:     Makarius
+
+Document model for theory files: no edits, no blobs, no overlays.
+*/
+
+package isabelle
+
+
+object Thy_Document_Model
+{
+  def read_file(session: Session, path: Path,
+    qualifier: String = Sessions.DRAFT,
+    node_visible: Boolean = false,
+    node_required: Boolean = false): Thy_Document_Model =
+  {
+    val node_name = session.resources.thy_node_name(qualifier, path.file)
+    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)
+  }
+}
+
+final class Thy_Document_Model private(
+  val session: Session,
+  val node_name: Document.Node.Name,
+  val text: String,
+  val node_visible: Boolean,
+  val node_required: Boolean) 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))
+
+
+  /* perspective */
+
+  def text_perspective: Text.Perspective =
+    if (node_visible) Text.Perspective.full else Text.Perspective.empty
+
+  def node_perspective: Document.Node.Perspective_Text =
+    Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
+
+
+  /* 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 1a9e2a2bf251 -r 57d58c3cf16b src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Nov 06 17:24:09 2017 +0100
+++ b/src/Pure/build-jars	Mon Nov 06 17:21:32 2017 +0100
@@ -128,6 +128,7 @@
   Thy/html.scala
   Thy/present.scala
   Thy/sessions.scala
+  Thy/thy_document_model.scala
   Thy/thy_header.scala
   Thy/thy_syntax.scala
   Tools/bibtex.scala