equal
deleted
inserted
replaced
119 def make_tree( |
119 def make_tree( |
120 parent: DefaultMutableTreeNode, |
120 parent: DefaultMutableTreeNode, |
121 offset: Text.Offset, |
121 offset: Text.Offset, |
122 documents: List[Document_Structure.Document]): Unit = |
122 documents: List[Document_Structure.Document]): Unit = |
123 { |
123 { |
124 (offset /: documents) { case (i, document) => |
124 documents.foldLeft(offset) { case (i, document) => |
125 document match { |
125 document match { |
126 case Document_Structure.Block(name, text, body) => |
126 case Document_Structure.Block(name, text, body) => |
127 val range = Text.Range(i, i + document.length) |
127 val range = Text.Range(i, i + document.length) |
128 val node = |
128 val node = |
129 new DefaultMutableTreeNode( |
129 new DefaultMutableTreeNode( |