80 |
80 |
81 /* phase 2: recover command spans */ |
81 /* phase 2: recover command spans */ |
82 |
82 |
83 def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = |
83 def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = |
84 { |
84 { |
85 // FIXME relative search! |
|
86 commands.iterator.find(is_unparsed) match { |
85 commands.iterator.find(is_unparsed) match { |
87 case Some(first_unparsed) => |
86 case Some(first_unparsed) => |
88 val prefix = commands.prev(first_unparsed) |
87 val first = |
89 val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList |
88 commands.rev_iterator(first_unparsed).find(_.is_command) getOrElse commands.head |
90 val suffix = commands.next(body.last) |
89 val last = |
|
90 commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last |
|
91 val range = |
|
92 commands.iterator(first).takeWhile(_ != last).toList ::: List(last) |
91 |
93 |
92 val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) |
94 val sources = range.flatMap(_.span.map(_.source)) |
93 val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) |
95 val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) |
94 |
96 |
95 val (before_edit, spans1) = |
97 val (before_edit, spans1) = |
96 if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span)) |
98 if (!spans0.isEmpty && first.is_command && first.span == spans0.head) |
97 (prefix, spans0.tail) |
99 (Some(first), spans0.tail) |
98 else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) |
100 else (commands.prev(first), spans0) |
99 |
101 |
100 val (after_edit, spans2) = |
102 val (after_edit, spans2) = |
101 if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) |
103 if (!spans1.isEmpty && last.is_command && last.span == spans1.last) |
102 (suffix, spans1.take(spans1.length - 1)) |
104 (Some(last), spans1.take(spans1.length - 1)) |
103 else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) |
105 else (commands.next(last), spans1) |
104 |
106 |
105 val inserted = spans2.map(span => new Command(session.create_id(), span)) |
107 val inserted = spans2.map(span => new Command(session.create_id(), span)) |
106 val new_commands = |
108 val new_commands = |
107 commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) |
109 commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) |
108 parse_spans(new_commands) |
110 parse_spans(new_commands) |