# HG changeset patch
# User wenzelm
# Date 1309698617 -7200
# Node ID 42b98a59ec302a1fe7506860c37412ac7dcde6f3
# Parent  598b2c6ce13f51a36fbf20eae3b084d532df73e8
tuned signature;

diff -r 598b2c6ce13f -r 42b98a59ec30 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 02 23:31:07 2011 +0200
+++ b/src/Pure/System/session.scala	Sun Jul 03 15:10:17 2011 +0200
@@ -261,7 +261,8 @@
 
         case Edit_Version(edits) if prover != null =>
           val previous = global_state.peek().history.tip.version
-          val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
+          val syntax = current_syntax()
+          val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
           val change = global_state.change_yield(_.extend_history(previous, edits, result))
 
           val this_actor = self
diff -r 598b2c6ce13f -r 42b98a59ec30 src/Pure/Thy/thy_syntax.scala
--- 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))
     }
   }
 }