src/Tools/jEdit/src/document_model.scala
changeset 64883 e89f5ef32aa2
parent 64868 6212d3c396b0
child 64885 205274ca16ee
equal deleted inserted replaced
64882:c3b42ac0cf81 64883:e89f5ef32aa2
   407   // owned by GUI thread
   407   // owned by GUI thread
   408   private var _node_required = false
   408   private var _node_required = false
   409   def node_required: Boolean = _node_required
   409   def node_required: Boolean = _node_required
   410   def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
   410   def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
   411 
   411 
       
   412   def document_view_iterator: Iterator[Document_View] =
       
   413     for {
       
   414       text_area <- JEdit_Lib.jedit_text_areas(buffer)
       
   415       doc_view <- Document_View.get(text_area)
       
   416     } yield doc_view
       
   417 
   412   override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
   418   override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
   413   {
   419   {
   414     GUI_Thread.require {}
   420     GUI_Thread.require {}
   415 
   421 
   416     (for {
   422     (for {
   417       doc_view <- PIDE.document_views(buffer).iterator
   423       doc_view <- document_view_iterator
   418       range <- doc_view.perspective(snapshot).ranges.iterator
   424       range <- doc_view.perspective(snapshot).ranges.iterator
   419     } yield range).toList
   425     } yield range).toList
   420   }
   426   }
   421 
   427 
   422 
   428 
   501       GUI_Thread.require {}
   507       GUI_Thread.require {}
   502 
   508 
   503       reset_blob()
   509       reset_blob()
   504       reset_bibtex_entries()
   510       reset_bibtex_entries()
   505 
   511 
   506       for (doc_view <- PIDE.document_views(buffer))
   512       for (doc_view <- document_view_iterator)
   507         doc_view.rich_text_area.active_reset()
   513         doc_view.rich_text_area.active_reset()
   508 
   514 
   509       pending ++= edits
   515       pending ++= edits
   510       PIDE.editor.invoke()
   516       PIDE.editor.invoke()
   511     }
   517     }