improved performance of remove, e.g. relevant for Theories_Dockable.purge;
authorwenzelm
Wed Mar 01 15:16:06 2017 +0100 (2017-03-01)
changeset 65074df14a0e872e6
parent 65073 b5bf76cf2b4e
child 65075 03e6aa683c4d
improved performance of remove, e.g. relevant for Theories_Dockable.purge;
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Mar 01 11:26:19 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Mar 01 15:16:06 2017 +0100
     1.3 @@ -120,6 +120,9 @@
     1.4    {
     1.5      eds match {
     1.6        case e :: es =>
     1.7 +        def insert_text(cmd: Option[Command], text: String): Linear_Set[Command] =
     1.8 +          if (text == "") commands else commands.insert_after(cmd, Command.unparsed(text))
     1.9 +
    1.10          Document.Node.Commands.starts(commands.iterator).find {
    1.11            case (cmd, cmd_start) =>
    1.12              e.can_edit(cmd.source, cmd_start) ||
    1.13 @@ -127,15 +130,15 @@
    1.14          } match {
    1.15            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
    1.16              val (rest, text) = e.edit(cmd.source, cmd_start)
    1.17 -            val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
    1.18 +            val new_commands = insert_text(Some(cmd), text) - cmd
    1.19              edit_text(rest.toList ::: es, new_commands)
    1.20  
    1.21            case Some((cmd, cmd_start)) =>
    1.22 -            edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
    1.23 +            edit_text(es, insert_text(Some(cmd), e.text))
    1.24  
    1.25            case None =>
    1.26              require(e.is_insert && e.start == 0)
    1.27 -            edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
    1.28 +            edit_text(es, insert_text(None, e.text))
    1.29          }
    1.30        case Nil => commands
    1.31      }