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