--- a/src/Tools/VSCode/src/document_model.scala Sat Dec 31 15:31:56 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Sat Dec 31 15:32:54 2016 +0100
@@ -29,7 +29,7 @@
session: Session,
node_name: Document.Node.Name,
doc: Line.Document,
- external: Boolean = false,
+ external_file: Boolean = false,
node_required: Boolean = false,
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
pending_edits: Vector[Text.Edit] = Vector.empty,
@@ -68,7 +68,7 @@
/* perspective */
- def node_visible: Boolean = !external
+ def node_visible: Boolean = !external_file
def text_perspective: Text.Perspective =
if (node_visible) Text.Perspective.full else Text.Perspective.empty
@@ -93,7 +93,7 @@
}
def update_file: Option[Document_Model] =
- if (external) {
+ if (external_file) {
try { update_text(File.read(file)) }
catch { case ERROR(_) => None }
}