equal
deleted
inserted
replaced
39 val removed_perspective = |
39 val removed_perspective = |
40 (removed -- models.iterator.map(_.node_name)).toList.map( |
40 (removed -- models.iterator.map(_.node_name)).toList.map( |
41 name => (name, Document.Node.no_perspective_text)) |
41 name => (name, Document.Node.no_perspective_text)) |
42 |
42 |
43 val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective |
43 val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective |
44 if (!edits.isEmpty) session.update(doc_blobs, edits) |
44 if (edits.nonEmpty) session.update(doc_blobs, edits) |
45 } |
45 } |
46 |
46 |
47 private val delay_flush = |
47 private val delay_flush = |
48 GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
48 GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
49 |
49 |