| changeset 64683 | c0c09b6dfbe0 |
| parent 64682 | 7e119f32276a |
| child 64690 | 599873de8b01 |
--- a/src/Tools/VSCode/src/document_model.scala Wed Dec 28 17:10:09 2016 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Wed Dec 28 17:26:38 2016 +0100 @@ -13,7 +13,7 @@ case class Document_Model( - session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Text.Length, + session: Session, doc: Line.Document, node_name: Document.Node.Name, changed: Boolean = true, published_diagnostics: List[Text.Info[Command.Results]] = Nil) {