--- 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 }
}
--- 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 =