src/Tools/jEdit/src/proofdocument/session.scala
changeset 34853 32b49207ca20
parent 34851 304a86164dd2
child 34859 f986d84dd44b
equal deleted inserted replaced
34852:d21c997104c4 34853:32b49207ca20
    79 
    79 
    80     def handle_change(change: Change)
    80     def handle_change(change: Change)
    81     {
    81     {
    82       require(change.parent.isDefined)
    82       require(change.parent.isDefined)
    83 
    83 
    84       val (doc, changes) = change.result.join
    84       val (changes, doc) = change.result.join
    85       val id_changes = changes map {
    85       val id_changes = changes map {
    86         case (c1, c2) =>
    86         case (c1, c2) =>
    87           (c1.map(_.id).getOrElse(""),
    87           (c1.map(_.id).getOrElse(""),
    88            c2 match {
    88            c2 match {
    89               case None => None
    89               case None => None