src/Pure/Thy/thy_document_model.scala
changeset 67056 e35ae3eeec93
parent 67055 383b902fe2b9
child 67057 0d8e4e777973
     1.1 --- a/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 13:22:00 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_document_model.scala	Sun Nov 12 16:38:13 2017 +0100
     1.3 @@ -11,12 +11,11 @@
     1.4  {
     1.5    def read_file(session: Session,
     1.6      node_name: Document.Node.Name,
     1.7 -    node_visible: Boolean = false,
     1.8 -    node_required: Boolean = false): Thy_Document_Model =
     1.9 +    node_visible: Boolean = false): Thy_Document_Model =
    1.10    {
    1.11      val path = node_name.path
    1.12      if (!node_name.is_theory) error("Not a theory file: " + path)
    1.13 -    new Thy_Document_Model(session, node_name, File.read(path), node_visible, node_required)
    1.14 +    new Thy_Document_Model(session, node_name, File.read(path), node_visible)
    1.15    }
    1.16  }
    1.17  
    1.18 @@ -24,8 +23,7 @@
    1.19    val session: Session,
    1.20    val node_name: Document.Node.Name,
    1.21    val text: String,
    1.22 -  val node_visible: Boolean,
    1.23 -  val node_required: Boolean) extends Document.Model
    1.24 +  val node_visible: Boolean) extends Document.Model
    1.25  {
    1.26    /* content */
    1.27  
    1.28 @@ -42,6 +40,8 @@
    1.29    def node_header: Document.Node.Header =
    1.30      resources.check_thy_reader(node_name, Scan.char_reader(text))
    1.31  
    1.32 +  def node_required: Boolean = true
    1.33 +
    1.34  
    1.35    /* perspective */
    1.36  
    1.37 @@ -52,6 +52,19 @@
    1.38      Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
    1.39  
    1.40  
    1.41 +  /* edits */
    1.42 +
    1.43 +  def node_edits(old: Option[Thy_Document_Model]): List[Document.Edit_Text] =
    1.44 +  {
    1.45 +    val text_edits =
    1.46 +      if (old.isEmpty) Text.Edit.inserts(0, text)
    1.47 +      else Text.Edit.replace(0, old.get.text, text)
    1.48 +
    1.49 +    if (text_edits.isEmpty && old.isDefined && old.get.node_perspective == node_perspective) Nil
    1.50 +    else node_edits(node_header, text_edits, node_perspective)
    1.51 +  }
    1.52 +
    1.53 +
    1.54    /* prover session */
    1.55  
    1.56    def resources: Resources = session.resources