# HG changeset patch
# User wenzelm
# Date 1483191337 -3600
# Node ID 65bcb1fbaa73d5676d17e371c91d3c272bcfbd60
# Parent  6df73de0d3c70acadbc136ce3e1fb4419deccd2b
clarified node_visible;

diff -r 6df73de0d3c7 -r 65bcb1fbaa73 src/Tools/VSCode/src/document_model.scala
--- 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