# HG changeset patch
# User wenzelm
# Date 1483194774 -3600
# Node ID c534a2ac537d4256250eaeed5778f3b00ef1b65f
# Parent  38305f56c769afd3a717529f57690d3eb67fef9d
clarified;

diff -r 38305f56c769 -r c534a2ac537d src/Tools/VSCode/src/document_model.scala
--- 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 }
     }
diff -r 38305f56c769 -r c534a2ac537d src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 15:31:56 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 15:32:54 2016 +0100
@@ -74,7 +74,7 @@
     state.change(st =>
       {
         val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
-        val model1 = (model.update_text(text) getOrElse model).copy(external = false)
+        val model1 = (model.update_text(text) getOrElse model).copy(external_file = false)
         st.copy(
           models = st.models + (uri -> model1),
           pending_input = st.pending_input + uri)
@@ -86,7 +86,7 @@
       st.models.get(uri) match {
         case None => (None, st)
         case Some(model) =>
-          (Some(model), st.copy(models = st.models + (uri -> model.copy(external = true))))
+          (Some(model), st.copy(models = st.models + (uri -> model.copy(external_file = true))))
       })
 
   def sync_models(changed_files: Set[JFile]): Boolean =