src/Pure/Thy/thy_document_model.scala
author wenzelm
Sun Nov 12 13:22:00 2017 +0100 (19 months ago)
changeset 67055 383b902fe2b9
parent 67016 57d58c3cf16b
child 67056 e35ae3eeec93
permissions -rw-r--r--
tuned signature;
wenzelm@67016
     1
/*  Title:      Pure/Thy/thy_document_model.scala
wenzelm@67016
     2
    Author:     Makarius
wenzelm@67016
     3
wenzelm@67055
     4
Document model for theory files: no blobs, no edits, no overlays.
wenzelm@67016
     5
*/
wenzelm@67016
     6
wenzelm@67016
     7
package isabelle
wenzelm@67016
     8
wenzelm@67016
     9
wenzelm@67016
    10
object Thy_Document_Model
wenzelm@67016
    11
{
wenzelm@67055
    12
  def read_file(session: Session,
wenzelm@67055
    13
    node_name: Document.Node.Name,
wenzelm@67016
    14
    node_visible: Boolean = false,
wenzelm@67016
    15
    node_required: Boolean = false): Thy_Document_Model =
wenzelm@67016
    16
  {
wenzelm@67055
    17
    val path = node_name.path
wenzelm@67016
    18
    if (!node_name.is_theory) error("Not a theory file: " + path)
wenzelm@67016
    19
    new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required)
wenzelm@67016
    20
  }
wenzelm@67016
    21
}
wenzelm@67016
    22
wenzelm@67016
    23
final class Thy_Document_Model private(
wenzelm@67016
    24
  val session: Session,
wenzelm@67016
    25
  val node_name: Document.Node.Name,
wenzelm@67016
    26
  val text: String,
wenzelm@67016
    27
  val node_visible: Boolean,
wenzelm@67016
    28
  val node_required: Boolean) extends Document.Model
wenzelm@67016
    29
{
wenzelm@67016
    30
  /* content */
wenzelm@67016
    31
wenzelm@67016
    32
  def get_text(range: Text.Range): Option[String] =
wenzelm@67016
    33
    if (0 <= range.start && range.stop <= text.length) Some(range.substring(text)) else None
wenzelm@67016
    34
wenzelm@67016
    35
  def get_blob: Option[Document.Blob] = None
wenzelm@67016
    36
wenzelm@67016
    37
  def bibtex_entries: List[Text.Info[String]] = Nil
wenzelm@67016
    38
wenzelm@67016
    39
wenzelm@67016
    40
  /* header */
wenzelm@67016
    41
wenzelm@67016
    42
  def node_header: Document.Node.Header =
wenzelm@67016
    43
    resources.check_thy_reader(node_name, Scan.char_reader(text))
wenzelm@67016
    44
wenzelm@67016
    45
wenzelm@67016
    46
  /* perspective */
wenzelm@67016
    47
wenzelm@67016
    48
  def text_perspective: Text.Perspective =
wenzelm@67016
    49
    if (node_visible) Text.Perspective.full else Text.Perspective.empty
wenzelm@67016
    50
wenzelm@67016
    51
  def node_perspective: Document.Node.Perspective_Text =
wenzelm@67016
    52
    Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
wenzelm@67016
    53
wenzelm@67016
    54
wenzelm@67016
    55
  /* prover session */
wenzelm@67016
    56
wenzelm@67016
    57
  def resources: Resources = session.resources
wenzelm@67016
    58
wenzelm@67016
    59
  def is_stable: Boolean = true
wenzelm@67016
    60
  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits = Nil)
wenzelm@67016
    61
}