--- a/src/Pure/System/session.scala Wed Dec 05 11:34:04 2012 +0100
+++ b/src/Pure/System/session.scala Wed Dec 05 12:22:55 2012 +0100
@@ -465,14 +465,6 @@
def cancel_execution() { session_actor ! Cancel_Execution }
- def edit(edits: List[Document.Edit_Text])
+ def update(edits: List[Document.Edit_Text])
{ session_actor !? Session.Raw_Edits(edits) }
-
- def edit_node(name: Document.Node.Name,
- header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
- {
- edit(List(header_edit(name, header),
- name -> Document.Node.Edits(text_edits),
- name -> Document.Node.Perspective(perspective)))
- }
}