--- a/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 04 20:52:06 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Jan 04 21:20:37 2017 +0100
@@ -106,9 +106,8 @@
(for {
(file, model) <- st.models.iterator
if changed_files(file) && model.external_file
- model1 <-
- (try { model.update_text(File.read(file)) }
- catch { case ERROR(_) => None })
+ text <- try_read(file)
+ model1 <- model.update_text(text)
} yield (file, model1)).toList
if (changed_models.isEmpty) (false, st)
else (true,
@@ -118,6 +117,19 @@
})
+ /* file content */
+
+ def try_read(file: JFile): Option[String] =
+ try { Some(File.read(file)) }
+ catch { case ERROR(_) => None }
+
+ def get_file_content(file: JFile): Option[String] =
+ get_model(file) match {
+ case Some(model) => Some(model.doc.make_text)
+ case None => try_read(file)
+ }
+
+
/* resolve dependencies */
val thy_info = new Thy_Info(this)
@@ -135,9 +147,7 @@
dep <- thy_info.dependencies("", thys).deps.iterator
file = node_file(dep.name)
if !st.models.isDefinedAt(file)
- text <-
- try { Some(File.read(file)) }
- catch { case ERROR(_) => None }
+ text <- try_read(file)
}
yield {
val model = Document_Model.init(session, node_name(file))