126 |
126 |
127 def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit]) |
127 def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit]) |
128 : (List[Edit[Command]], Document) = |
128 : (List[Edit[Command]], Document) = |
129 { |
129 { |
130 require(old_doc.assignment.is_finished) |
130 require(old_doc.assignment.is_finished) |
131 |
|
132 |
|
133 /* unparsed dummy commands */ |
|
134 |
|
135 def unparsed(source: String) = |
|
136 new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source))) |
|
137 |
|
138 def is_unparsed(command: Command) = command.id == NO_ID |
|
139 |
131 |
140 |
132 |
141 /* phase 1: edit individual command source */ |
133 /* phase 1: edit individual command source */ |
142 |
134 |
143 @tailrec def edit_text(eds: List[Text_Edit], |
135 @tailrec def edit_text(eds: List[Text_Edit], |
150 e.can_edit(cmd.source, cmd_start) || |
142 e.can_edit(cmd.source, cmd_start) || |
151 e.is_insert && e.start == cmd_start + cmd.length |
143 e.is_insert && e.start == cmd_start + cmd.length |
152 } match { |
144 } match { |
153 case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => |
145 case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => |
154 val (rest, text) = e.edit(cmd.source, cmd_start) |
146 val (rest, text) = e.edit(cmd.source, cmd_start) |
155 val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd |
147 val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd |
156 edit_text(rest.toList ::: es, new_commands) |
148 edit_text(rest.toList ::: es, new_commands) |
157 |
149 |
158 case Some((cmd, cmd_start)) => |
150 case Some((cmd, cmd_start)) => |
159 edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) |
151 edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text))) |
160 |
152 |
161 case None => |
153 case None => |
162 require(e.is_insert && e.start == 0) |
154 require(e.is_insert && e.start == 0) |
163 edit_text(es, commands.insert_after(None, unparsed(e.text))) |
155 edit_text(es, commands.insert_after(None, Command.unparsed(e.text))) |
164 } |
156 } |
165 case Nil => commands |
157 case Nil => commands |
166 } |
158 } |
167 } |
159 } |
168 |
160 |
169 |
161 |
170 /* phase 2: recover command spans */ |
162 /* phase 2: recover command spans */ |
171 |
163 |
172 @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = |
164 @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = |
173 { |
165 { |
174 commands.iterator.find(is_unparsed) match { |
166 commands.iterator.find(_.is_unparsed) match { |
175 case Some(first_unparsed) => |
167 case Some(first_unparsed) => |
176 val first = |
168 val first = |
177 commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head |
169 commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head |
178 val last = |
170 val last = |
179 commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last |
171 commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last |