src/Tools/jEdit/src/document_model.scala
changeset 61538 bf4969660913
parent 61192 98eba31c51f8
child 61728 5f5ff1eab407
equal deleted inserted replaced
61537:f6bd97a587b7 61538:bf4969660913
   253       GUI_Thread.require {}
   253       GUI_Thread.require {}
   254 
   254 
   255       reset_blob()
   255       reset_blob()
   256       reset_bibtex()
   256       reset_bibtex()
   257 
   257 
       
   258       for (doc_view <- PIDE.document_views(buffer))
       
   259         doc_view.rich_text_area.active_reset()
       
   260 
   258       if (clear) {
   261       if (clear) {
   259         pending_clear = true
   262         pending_clear = true
   260         pending.clear
   263         pending.clear
   261       }
   264       }
   262       pending += e
   265       pending += e