--- a/src/Pure/Thy/thy_syntax.scala Thu Nov 11 16:48:46 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Thu Nov 11 17:07:05 2010 +0100
@@ -100,7 +100,7 @@
/** text edits **/
def text_edits(session: Session, previous: Document.Version,
- edits: List[Document.Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
+ edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
{
/* phase 1: edit individual command source */
@@ -172,7 +172,7 @@
/* resulting document edits */
{
- val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
+ val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
var nodes = previous.nodes
edits foreach {