equal
deleted
inserted
replaced
119 @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]): Linear_Set[Command] = |
119 @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command]): Linear_Set[Command] = |
120 { |
120 { |
121 eds match { |
121 eds match { |
122 case e :: es => |
122 case e :: es => |
123 def insert_text(cmd: Option[Command], text: String): Linear_Set[Command] = |
123 def insert_text(cmd: Option[Command], text: String): Linear_Set[Command] = |
124 if (text == "") commands else commands.insert_after(cmd, Command.unparsed(text)) |
124 if (text == "") commands else commands.insert_after(cmd, Command.text(text)) |
125 |
125 |
126 Document.Node.Commands.starts(commands.iterator).find { |
126 Document.Node.Commands.starts(commands.iterator).find { |
127 case (cmd, cmd_start) => |
127 case (cmd, cmd_start) => |
128 e.can_edit(cmd.source, cmd_start) || |
128 e.can_edit(cmd.source, cmd_start) || |
129 e.is_insert && e.start == cmd_start + cmd.length |
129 e.is_insert && e.start == cmd_start + cmd.length |