src/Tools/VSCode/src/server.scala
changeset 65184 0f555ce33970
parent 65162 df1052d0708d
child 65189 41d2452845fc
equal deleted inserted replaced
65183:37f1effd6683 65184:0f555ce33970
   143     delay_output.invoke()
   143     delay_output.invoke()
   144   }
   144   }
   145 
   145 
   146   private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
   146   private def change_document(file: JFile, changes: List[Protocol.TextDocumentChange])
   147   {
   147   {
   148     changes.foreach(change => resources.change_model(session, file, change.text, change.range))
   148     changes.reverse.foreach(change =>
       
   149       resources.change_model(session, file, change.text, change.range))
   149     delay_input.invoke()
   150     delay_input.invoke()
   150     delay_output.invoke()
   151     delay_output.invoke()
   151   }
   152   }
   152 
   153 
   153 
   154