# HG changeset patch
# User wenzelm
# Date 1483561237 -3600
# Node ID 6cdcc271dbd553545d20f69b10819c1642a8df54
# Parent  7884a19de32505027b4b12d93fbf3a184a9fe9b3
tuned;

diff -r 7884a19de325 -r 6cdcc271dbd5 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jan 04 20:52:06 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jan 04 21:20:37 2017 +0100
@@ -83,17 +83,14 @@
     : Option[Line.Node_Range] =
   {
     for {
-      name <- resources.source_file(source_name)
+      platform_path <- resources.source_file(source_name)
       file <-
-        (try { Some(new JFile(name).getCanonicalFile) }
+        (try { Some(new JFile(platform_path).getCanonicalFile) }
          catch { case ERROR(_) => None })
     }
     yield {
-      val opt_text =
-        try { Some(File.read(file)) } // FIXME content from resources/models
-        catch { case ERROR(_) => None }
       Line.Node_Range(file.getPath,
-        opt_text match {
+        resources.get_file_content(file) match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)
             val doc = Line.Document(text, resources.text_length)
diff -r 7884a19de325 -r 6cdcc271dbd5 src/Tools/VSCode/src/vscode_resources.scala
--- 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))