# HG changeset patch
# User wenzelm
# Date 1484037626 -3600
# Node ID e5572c1169fd4fa5afa166670a425de7cc19a2c3
# Parent  4d56170d97b3713a869293bbac7b1cdb6ba5a19e
tuned;

diff -r 4d56170d97b3 -r e5572c1169fd src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Jan 09 23:00:11 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Jan 10 09:40:26 2017 +0100
@@ -71,8 +71,7 @@
       if (models.isDefinedAt(node_name)) this
       else {
         val edit = Text.Edit.insert(0, text)
-        val model = File_Model(session, node_name, File_Content(text), pending_edits = List(edit))
-        model.watch
+        val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
         copy(models = models + (node_name -> model))
       }
   }
@@ -285,13 +284,33 @@
   }
 }
 
+object File_Model
+{
+  def init(session: Session,
+    node_name: Document.Node.Name,
+    text: String,
+    node_required: Boolean = false,
+    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)
+
+    for (file <- PIDE.resources.node_name_file(node_name))
+      PIDE.file_watcher.register_parent(file)
+
+    model
+  }
+}
+
 case class File_Model(
   session: Session,
   node_name: Document.Node.Name,
   content: Document_Model.File_Content,
-  node_required: Boolean = false,
-  last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
-  pending_edits: List[Text.Edit] = Nil) extends Document_Model
+  node_required: Boolean,
+  last_perspective: Document.Node.Perspective_Text,
+  pending_edits: List[Text.Edit]) extends Document_Model
 {
   /* header */
 
@@ -341,13 +360,6 @@
 
   def is_stable: Boolean = pending_edits.isEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
-
-
-  /* watch file-system content */
-
-  def watch: Unit =
-    for (file <- PIDE.resources.node_name_file(node_name))
-      PIDE.file_watcher.register_parent(file)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
@@ -556,11 +568,7 @@
     buffer.removeBufferListener(buffer_listener)
     init_token_marker()
 
-    val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer))
-    val model =
-      File_Model(session, node_name, content, node_required,
-        pending_edits.get_last_perspective, pending_edits.get_edits)
-    model.watch
-    model
+    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
+      pending_edits.get_last_perspective, pending_edits.get_edits)
   }
 }