clarified Document_Model perspective and edits;
authorwenzelm
Fri Dec 30 11:46:34 2016 +0100 (2016-12-30)
changeset 647077157685b71e3
parent 64706 3ebf9f8299df
child 64708 dd7f1a7e03f4
clarified Document_Model perspective and edits;
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_resources.scala
     1.1 --- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 10:26:10 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 11:46:34 2016 +0100
     1.3 @@ -12,9 +12,26 @@
     1.4  import scala.util.parsing.input.CharSequenceReader
     1.5  
     1.6  
     1.7 -case class Document_Model(
     1.8 -  session: Session, node_name: Document.Node.Name, doc: Line.Document,
     1.9 -  changed: Boolean = true,
    1.10 +object Document_Model
    1.11 +{
    1.12 +  def init(session: Session, node_name: Document.Node.Name, text: String): Document_Model =
    1.13 +  {
    1.14 +    val resources = session.resources.asInstanceOf[VSCode_Resources]
    1.15 +    Document_Model(session, node_name, Line.Document(text, resources.text_length),
    1.16 +      pending_clear = true,
    1.17 +      pending_edits = List(Text.Edit.insert(0, text)))
    1.18 +  }
    1.19 +}
    1.20 +
    1.21 +sealed case class Document_Model private(
    1.22 +  session: Session,
    1.23 +  node_name: Document.Node.Name,
    1.24 +  doc: Line.Document,
    1.25 +  node_visible: Boolean = true,
    1.26 +  node_required: Boolean = false,
    1.27 +  last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
    1.28 +  pending_clear: Boolean = false,
    1.29 +  pending_edits: List[Text.Edit] = Nil,
    1.30    published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    1.31  {
    1.32    /* name */
    1.33 @@ -37,22 +54,39 @@
    1.34      }
    1.35  
    1.36  
    1.37 +  /* perspective */
    1.38 +
    1.39 +  def text_perspective: Text.Perspective =
    1.40 +    if (node_visible) Text.Perspective.full else Text.Perspective.empty
    1.41 +
    1.42 +  def node_perspective: Document.Node.Perspective_Text =
    1.43 +    Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
    1.44 +
    1.45 +
    1.46    /* edits */
    1.47  
    1.48 -  def text_edits: List[Text.Edit] =
    1.49 -    if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
    1.50 +  def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] =
    1.51 +  {
    1.52 +    val perspective = node_perspective
    1.53 +    if (pending_clear || pending_edits.nonEmpty || last_perspective != perspective) {
    1.54 +      val model1 = copy(pending_clear = false, pending_edits = Nil, last_perspective = perspective)
    1.55  
    1.56 -  def node_edits: List[Document.Edit_Text] =
    1.57 -    if (changed) {
    1.58 -      List(session.header_edit(node_name, node_header),
    1.59 -        node_name -> Document.Node.Clear(),
    1.60 -        node_name -> Document.Node.Edits(text_edits),
    1.61 -        node_name ->
    1.62 -          Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty))
    1.63 +      val header_edit = session.header_edit(node_name, node_header)
    1.64 +      val edits: List[Document.Edit_Text] =
    1.65 +        if (pending_clear)
    1.66 +          List(header_edit,
    1.67 +            node_name -> Document.Node.Clear(),
    1.68 +            node_name -> Document.Node.Edits(pending_edits),
    1.69 +            node_name -> perspective)
    1.70 +        else
    1.71 +          List(header_edit,
    1.72 +            node_name -> Document.Node.Edits(pending_edits),
    1.73 +            node_name -> perspective)
    1.74 +
    1.75 +      Some((edits.filterNot(_._2.is_void), model1))
    1.76      }
    1.77 -    else Nil
    1.78 -
    1.79 -  def unchanged: Document_Model = if (changed) copy(changed = false) else this
    1.80 +    else None
    1.81 +  }
    1.82  
    1.83  
    1.84    /* diagnostics */
    1.85 @@ -70,7 +104,7 @@
    1.86  
    1.87    def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
    1.88  
    1.89 -  def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
    1.90 +  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
    1.91  
    1.92    def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
    1.93  }
     2.1 --- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 10:26:10 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 11:46:34 2016 +0100
     2.3 @@ -114,7 +114,7 @@
     2.4  
     2.5    private def update_document(uri: String, text: String)
     2.6    {
     2.7 -    val model = Document_Model(session, resources.node_name(uri), Line.Document(text, text_length))
     2.8 +    val model = Document_Model.init(session, resources.node_name(uri), text)
     2.9      resources.update_model(model)
    2.10      delay_input.invoke()
    2.11    }
     3.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 10:26:10 2016 +0100
     3.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 11:46:34 2016 +0100
     3.3 @@ -79,11 +79,12 @@
     3.4            (for {
     3.5              node_name <- st.pending_input.iterator
     3.6              model <- st.models.get(node_name.node)
     3.7 -            if model.changed } yield model).toList
     3.8 -        val edits = for { model <- changed; edit <- model.node_edits } yield edit
     3.9 -        session.update(Document.Blobs.empty, edits)
    3.10 +            res <- model.flush_edits
    3.11 +          } yield res).toList
    3.12 +
    3.13 +        session.update(Document.Blobs.empty, changed.flatMap(_._1))
    3.14          st.copy(
    3.15 -          models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
    3.16 +          models = (st.models /: changed) { case (ms, (_, m)) => ms + (m.uri -> m) },
    3.17            pending_input = Set.empty)
    3.18        })
    3.19    }