--- a/src/Tools/VSCode/src/document_model.scala Sat Dec 31 14:29:16 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Sat Dec 31 14:35:37 2016 +0100
@@ -30,7 +30,6 @@
node_name: Document.Node.Name,
doc: Line.Document,
external: Boolean = false,
- node_visible: Boolean = true,
node_required: Boolean = false,
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
pending_edits: Vector[Text.Edit] = Vector.empty,
@@ -69,6 +68,8 @@
/* perspective */
+ def node_visible: Boolean = !external
+
def text_perspective: Text.Perspective =
if (node_visible) Text.Perspective.full else Text.Perspective.empty