| changeset 64703 | a115391494ed |
| parent 64702 | d95b9117cb5b |
| child 64704 | 08c2d80428ff |
--- a/src/Tools/VSCode/src/document_model.scala Thu Dec 29 17:25:32 2016 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Thu Dec 29 21:54:04 2016 +0100 @@ -13,7 +13,7 @@ case class Document_Model( - session: Session, doc: Line.Document, node_name: Document.Node.Name, + session: Session, node_name: Document.Node.Name, doc: Line.Document, changed: Boolean = true, published_diagnostics: List[Text.Info[Command.Results]] = Nil) {