# HG changeset patch
# User wenzelm
# Date 1488377766 -3600
# Node ID df14a0e872e631b1c51dd396638eef001ce1b41f
# Parent  b5bf76cf2b4e1bbd8f56d2ba2182218029d77252
improved performance of remove, e.g. relevant for Theories_Dockable.purge;

diff -r b5bf76cf2b4e -r df14a0e872e6 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Mar 01 11:26:19 2017 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Mar 01 15:16:06 2017 +0100
@@ -120,6 +120,9 @@
   {
     eds match {
       case e :: es =>
+        def insert_text(cmd: Option[Command], text: String): Linear_Set[Command] =
+          if (text == "") commands else commands.insert_after(cmd, Command.unparsed(text))
+
         Document.Node.Commands.starts(commands.iterator).find {
           case (cmd, cmd_start) =>
             e.can_edit(cmd.source, cmd_start) ||
@@ -127,15 +130,15 @@
         } match {
           case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
             val (rest, text) = e.edit(cmd.source, cmd_start)
-            val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
+            val new_commands = insert_text(Some(cmd), text) - cmd
             edit_text(rest.toList ::: es, new_commands)
 
           case Some((cmd, cmd_start)) =>
-            edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
+            edit_text(es, insert_text(Some(cmd), e.text))
 
           case None =>
             require(e.is_insert && e.start == 0)
-            edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
+            edit_text(es, insert_text(None, e.text))
         }
       case Nil => commands
     }