equal
deleted
inserted
replaced
97 |
97 |
98 |
98 |
99 |
99 |
100 /** text edits **/ |
100 /** text edits **/ |
101 |
101 |
102 def text_edits(session: Session, previous: Document.Version, |
102 def text_edits(syntax: Outer_Syntax, new_id: () => Document.ID, previous: Document.Version, |
103 edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) = |
103 edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) = |
104 { |
104 { |
105 /* phase 1: edit individual command source */ |
105 /* phase 1: edit individual command source */ |
106 |
106 |
107 @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]) |
107 @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]) |
145 dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last |
145 dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last |
146 val range = |
146 val range = |
147 commands.iterator(first).takeWhile(_ != last).toList ::: List(last) |
147 commands.iterator(first).takeWhile(_ != last).toList ::: List(last) |
148 |
148 |
149 val sources = range.flatMap(_.span.map(_.source)) |
149 val sources = range.flatMap(_.span.map(_.source)) |
150 val spans0 = parse_spans(session.current_syntax().scan(sources.mkString)) |
150 val spans0 = parse_spans(syntax.scan(sources.mkString)) |
151 |
151 |
152 val (before_edit, spans1) = |
152 val (before_edit, spans1) = |
153 if (!spans0.isEmpty && first.is_command && first.span == spans0.head) |
153 if (!spans0.isEmpty && first.is_command && first.span == spans0.head) |
154 (Some(first), spans0.tail) |
154 (Some(first), spans0.tail) |
155 else (commands.prev(first), spans0) |
155 else (commands.prev(first), spans0) |
157 val (after_edit, spans2) = |
157 val (after_edit, spans2) = |
158 if (!spans1.isEmpty && last.is_command && last.span == spans1.last) |
158 if (!spans1.isEmpty && last.is_command && last.span == spans1.last) |
159 (Some(last), spans1.take(spans1.length - 1)) |
159 (Some(last), spans1.take(spans1.length - 1)) |
160 else (commands.next(last), spans1) |
160 else (commands.next(last), spans1) |
161 |
161 |
162 val inserted = spans2.map(span => new Command(session.new_id(), span)) |
162 val inserted = spans2.map(span => new Command(new_id(), span)) |
163 val new_commands = |
163 val new_commands = |
164 commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) |
164 commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) |
165 recover_spans(new_commands) |
165 recover_spans(new_commands) |
166 |
166 |
167 case None => commands |
167 case None => commands |
193 inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) |
193 inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) |
194 |
194 |
195 doc_edits += (name -> Some(cmd_edits)) |
195 doc_edits += (name -> Some(cmd_edits)) |
196 nodes += (name -> new Document.Node(commands2)) |
196 nodes += (name -> new Document.Node(commands2)) |
197 } |
197 } |
198 (doc_edits.toList, new Document.Version(session.new_id(), nodes)) |
198 (doc_edits.toList, new Document.Version(new_id(), nodes)) |
199 } |
199 } |
200 } |
200 } |
201 } |
201 } |