equal
deleted
inserted
replaced
62 /* pending text edits */ |
62 /* pending text edits */ |
63 |
63 |
64 private val node_name = (master_dir + Path.basic(thy_name)).implode |
64 private val node_name = (master_dir + Path.basic(thy_name)).implode |
65 |
65 |
66 private def node_header(): Document.Node.Header = |
66 private def node_header(): Document.Node.Header = |
67 Document.Node.Header(master_dir, |
67 Document.Node.Header(Path.current, // FIXME master_dir (!?) |
68 Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }) |
68 Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }) |
69 |
69 |
70 private object pending_edits // owned by Swing thread |
70 private object pending_edits // owned by Swing thread |
71 { |
71 { |
72 private val pending = new mutable.ListBuffer[Text.Edit] |
72 private val pending = new mutable.ListBuffer[Text.Edit] |