src/Tools/jEdit/src/document_model.scala
changeset 65469 78ace4a14975
parent 65359 9ca34f0407a9
child 66019 69b5ef78fb07
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Apr 12 17:48:19 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 12 19:56:47 2017 +0200
     1.3 @@ -310,7 +310,7 @@
     1.4      last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
     1.5      pending_edits: List[Text.Edit] = Nil): File_Model =
     1.6    {
     1.7 -    val file = PIDE.resources.node_name_file(node_name)
     1.8 +    val file = JEdit_Lib.check_file(node_name.node)
     1.9      file.foreach(PIDE.plugin.file_watcher.register_parent(_))
    1.10  
    1.11      val content = Document_Model.File_Content(text)