equal
deleted
inserted
replaced
308 text: String, |
308 text: String, |
309 node_required: Boolean = false, |
309 node_required: Boolean = false, |
310 last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
310 last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
311 pending_edits: List[Text.Edit] = Nil): File_Model = |
311 pending_edits: List[Text.Edit] = Nil): File_Model = |
312 { |
312 { |
313 val file = PIDE.resources.node_name_file(node_name) |
313 val file = JEdit_Lib.check_file(node_name.node) |
314 file.foreach(PIDE.plugin.file_watcher.register_parent(_)) |
314 file.foreach(PIDE.plugin.file_watcher.register_parent(_)) |
315 |
315 |
316 val content = Document_Model.File_Content(text) |
316 val content = Document_Model.File_Content(text) |
317 File_Model(session, node_name, file, content, node_required, last_perspective, pending_edits) |
317 File_Model(session, node_name, file, content, node_required, last_perspective, pending_edits) |
318 } |
318 } |