# HG changeset patch
# User wenzelm
# Date 1731087575 -3600
# Node ID 3796346f5bacb1b600c35c8c0969747a121a0e79
# Parent  4e9873629bffd1825aea83d7bae30ae8abbca727
clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);

diff -r 4e9873629bff -r 3796346f5bac src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Nov 08 18:34:33 2024 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Nov 08 18:39:35 2024 +0100
@@ -386,8 +386,6 @@
     new Command(id, node_name, blobs_info, span1, source1, results, markups)
   }
 
-  def text(source: String): Command = unparsed(source)
-
   def rich_text(body: XML.Body = Nil, results: Results = Results.empty): Command =
     unparsed(XML.content(body), id = Document_ID.make(), results = results,
       markups = Markups.init(Markup_Tree.from_XML(body)))
diff -r 4e9873629bff -r 3796346f5bac src/Pure/Thy/thy_syntax.scala
--- 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) =>