changeset 81407 | 3796346f5bac |
parent 76904 | e27d097d7d15 |
--- a/src/Pure/Thy/thy_syntax.scala Fri Nov 08 18:34:33 2024 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Fri Nov 08 18:39:35 2024 +0100 @@ -126,7 +126,7 @@ 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.text(text)) + if (text == "") commands else commands.insert_after(cmd, Command.unparsed(text)) Document.Node.Commands.starts(commands.iterator).find { case (cmd, cmd_start) =>