# HG changeset patch
# User wenzelm
# Date 1484038043 -3600
# Node ID eec7ffef0be65d196af6df43d266d4c38cae9dfb
# Parent  e5572c1169fd4fa5afa166670a425de7cc19a2c3
accomodate very big file_models and changed_files;

diff -r e5572c1169fd -r eec7ffef0be6 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Jan 10 09:40:26 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Jan 10 09:47:23 2017 +0100
@@ -98,15 +98,14 @@
         val changed_models =
           (for {
             model <- st.file_models_iterator
-            node_name = model.node_name
-            file <- PIDE.resources.node_name_file(node_name)
-            if changed_files(file)
-            text <- PIDE.resources.read_file_content(node_name)
+            file <- model.file if changed_files(file)
+            text <- PIDE.resources.read_file_content(model.node_name)
             if model.content.text != text
           } yield {
             val content = Document_Model.File_Content(text)
             val edits = Text.Edit.replace(0, model.content.text, text)
-            (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
+            val model1 = model.copy(content = content, pending_edits = model.pending_edits ::: edits)
+            (model.node_name, model1)
           }).toList
         if (changed_models.isEmpty) (false, st)
         else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
@@ -293,20 +292,18 @@
     last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
     pending_edits: List[Text.Edit] = Nil): File_Model =
   {
-    val content = Document_Model.File_Content(text)
-    val model =
-      File_Model(session, node_name, content, node_required, last_perspective, pending_edits)
+    val file = PIDE.resources.node_name_file(node_name)
+    file.foreach(PIDE.file_watcher.register_parent(_))
 
-    for (file <- PIDE.resources.node_name_file(node_name))
-      PIDE.file_watcher.register_parent(file)
-
-    model
+    val content = Document_Model.File_Content(text)
+    File_Model(session, node_name, file, content, node_required, last_perspective, pending_edits)
   }
 }
 
 case class File_Model(
   session: Session,
   node_name: Document.Node.Name,
+  file: Option[JFile],
   content: Document_Model.File_Content,
   node_required: Boolean,
   last_perspective: Document.Node.Perspective_Text,