src/Pure/Thy/thy_syntax.scala
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) =>