1.1 --- a/src/Pure/System/session.scala	Sat Jul 02 23:31:07 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sun Jul 03 15:10:17 2011 +0200
     1.3 @@ -261,7 +261,8 @@
     1.4  
     1.5          case Edit_Version(edits) if prover != null =>
     1.6            val previous = global_state.peek().history.tip.version
     1.7 -          val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
     1.8 +          val syntax = current_syntax()
     1.9 +          val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
    1.10            val change = global_state.change_yield(_.extend_history(previous, edits, result))
    1.11  
    1.12            val this_actor = self

     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Jul 02 23:31:07 2011 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Jul 03 15:10:17 2011 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4  
     2.5    /** text edits **/
     2.6  
     2.7 -  def text_edits(session: Session, previous: Document.Version,
     2.8 +  def text_edits(syntax: Outer_Syntax, new_id: () => Document.ID, previous: Document.Version,
     2.9        edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
    2.10    {
    2.11      /* phase 1: edit individual command source */
    2.12 @@ -147,7 +147,7 @@
    2.13              commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
    2.14  
    2.15            val sources = range.flatMap(_.span.map(_.source))
    2.16 -          val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
    2.17 +          val spans0 = parse_spans(syntax.scan(sources.mkString))
    2.18  
    2.19            val (before_edit, spans1) =
    2.20              if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
    2.21 @@ -159,7 +159,7 @@
    2.22                (Some(last), spans1.take(spans1.length - 1))
    2.23              else (commands.next(last), spans1)
    2.24  
    2.25 -          val inserted = spans2.map(span => new Command(session.new_id(), span))
    2.26 +          val inserted = spans2.map(span => new Command(new_id(), span))
    2.27            val new_commands =
    2.28              commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    2.29            recover_spans(new_commands)
    2.30 @@ -195,7 +195,7 @@
    2.31            doc_edits += (name -> Some(cmd_edits))
    2.32            nodes += (name -> new Document.Node(commands2))
    2.33        }
    2.34 -      (doc_edits.toList, new Document.Version(session.new_id(), nodes))
    2.35 +      (doc_edits.toList, new Document.Version(new_id(), nodes))
    2.36      }
    2.37    }
    2.38  }