src/Pure/Thy/thy_document_model.scala
changeset 67016 57d58c3cf16b
child 67055 383b902fe2b9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/thy_document_model.scala	Mon Nov 06 17:21:32 2017 +0100
     1.3 @@ -0,0 +1,61 @@
     1.4 +/*  Title:      Pure/Thy/thy_document_model.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Document model for theory files: no edits, no blobs, no overlays.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Thy_Document_Model
    1.14 +{
    1.15 +  def read_file(session: Session, path: Path,
    1.16 +    qualifier: String = Sessions.DRAFT,
    1.17 +    node_visible: Boolean = false,
    1.18 +    node_required: Boolean = false): Thy_Document_Model =
    1.19 +  {
    1.20 +    val node_name = session.resources.thy_node_name(qualifier, path.file)
    1.21 +    if (!node_name.is_theory) error("Not a theory file: " + path)
    1.22 +    new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required)
    1.23 +  }
    1.24 +}
    1.25 +
    1.26 +final class Thy_Document_Model private(
    1.27 +  val session: Session,
    1.28 +  val node_name: Document.Node.Name,
    1.29 +  val text: String,
    1.30 +  val node_visible: Boolean,
    1.31 +  val node_required: Boolean) extends Document.Model
    1.32 +{
    1.33 +  /* content */
    1.34 +
    1.35 +  def get_text(range: Text.Range): Option[String] =
    1.36 +    if (0 <= range.start && range.stop <= text.length) Some(range.substring(text)) else None
    1.37 +
    1.38 +  def get_blob: Option[Document.Blob] = None
    1.39 +
    1.40 +  def bibtex_entries: List[Text.Info[String]] = Nil
    1.41 +
    1.42 +
    1.43 +  /* header */
    1.44 +
    1.45 +  def node_header: Document.Node.Header =
    1.46 +    resources.check_thy_reader(node_name, Scan.char_reader(text))
    1.47 +
    1.48 +
    1.49 +  /* perspective */
    1.50 +
    1.51 +  def text_perspective: Text.Perspective =
    1.52 +    if (node_visible) Text.Perspective.full else Text.Perspective.empty
    1.53 +
    1.54 +  def node_perspective: Document.Node.Perspective_Text =
    1.55 +    Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
    1.56 +
    1.57 +
    1.58 +  /* prover session */
    1.59 +
    1.60 +  def resources: Resources = session.resources
    1.61 +
    1.62 +  def is_stable: Boolean = true
    1.63 +  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits = Nil)
    1.64 +}