src/Pure/PIDE/session.scala
changeset 82786 29d8d6d8a3b1
parent 82784 0751d363fd0e
child 82789 941b6cdf3611
equal deleted inserted replaced
82785:b06207e2215d 82786:29d8d6d8a3b1
   268   private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) {
   268   private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) {
   269     case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
   269     case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
   270       val prev = previous.get_finished
   270       val prev = previous.get_finished
   271       val change =
   271       val change =
   272         Timing.timeit(
   272         Timing.timeit(
   273           Thy_Syntax.parse_change(resources, reparse_limit, prev, doc_blobs, text_edits, consolidate),
   273           Thy_Syntax.parse_change(session, reparse_limit, prev, doc_blobs, text_edits, consolidate),
   274           message = _ => "parse_change",
   274           message = _ => "parse_change",
   275           enabled = timing)
   275           enabled = timing)
   276       version_result.fulfill(change.version)
   276       version_result.fulfill(change.version)
   277       manager.send(change)
   277       manager.send(change)
   278       true
   278       true