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