# HG changeset patch
# User wenzelm
# Date 1491053732 -7200
# Node ID c82a1620b274c1a96c0b67619e094714167dc14f
# Parent  8ec91f7eca37e1d0675f498dc393a55136ad0dce
tuned signature;

diff -r 8ec91f7eca37 -r c82a1620b274 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Apr 01 08:05:40 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Apr 01 15:35:32 2017 +0200
@@ -355,7 +355,7 @@
     new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup)
   }
 
-  def unparsed(source: String): Command =
+  def text(source: String): Command =
     unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
 
   def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
diff -r 8ec91f7eca37 -r c82a1620b274 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Apr 01 08:05:40 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Apr 01 15:35:32 2017 +0200
@@ -121,7 +121,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.unparsed(text))
+          if (text == "") commands else commands.insert_after(cmd, Command.text(text))
 
         Document.Node.Commands.starts(commands.iterator).find {
           case (cmd, cmd_start) =>