src/Tools/VSCode/src/document_model.scala
changeset 66674 30d5195299e2
parent 66150 c2e19b9e1398
child 66676 39db5bb7eb0a
     1.1 --- a/src/Tools/VSCode/src/document_model.scala	Mon Sep 18 10:28:22 2017 +0200
     1.2 +++ b/src/Tools/VSCode/src/document_model.scala	Mon Sep 18 10:32:09 2017 +0200
     1.3 @@ -56,6 +56,7 @@
     1.4    editor: Server.Editor,
     1.5    node_name: Document.Node.Name,
     1.6    content: Document_Model.Content,
     1.7 +  version: Option[Long] = None,
     1.8    external_file: Boolean = false,
     1.9    node_required: Boolean = false,
    1.10    last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
    1.11 @@ -66,10 +67,12 @@
    1.12    model =>
    1.13  
    1.14  
    1.15 -  /* text */
    1.16 +  /* content */
    1.17  
    1.18    def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
    1.19  
    1.20 +  def set_version(new_version: Long): Document_Model = copy(version = Some(new_version))
    1.21 +
    1.22  
    1.23    /* external file */
    1.24