--- a/src/Pure/Thy/thy_syntax.scala Sat Jul 02 23:31:07 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Sun Jul 03 15:10:17 2011 +0200
@@ -99,7 +99,7 @@
/** text edits **/
- def text_edits(session: Session, previous: Document.Version,
+ def text_edits(syntax: Outer_Syntax, new_id: () => Document.ID, previous: Document.Version,
edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
{
/* phase 1: edit individual command source */
@@ -147,7 +147,7 @@
commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
val sources = range.flatMap(_.span.map(_.source))
- val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
+ val spans0 = parse_spans(syntax.scan(sources.mkString))
val (before_edit, spans1) =
if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
@@ -159,7 +159,7 @@
(Some(last), spans1.take(spans1.length - 1))
else (commands.next(last), spans1)
- val inserted = spans2.map(span => new Command(session.new_id(), span))
+ val inserted = spans2.map(span => new Command(new_id(), span))
val new_commands =
commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
recover_spans(new_commands)
@@ -195,7 +195,7 @@
doc_edits += (name -> Some(cmd_edits))
nodes += (name -> new Document.Node(commands2))
}
- (doc_edits.toList, new Document.Version(session.new_id(), nodes))
+ (doc_edits.toList, new Document.Version(new_id(), nodes))
}
}
}