# 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