equal
deleted
inserted
replaced
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 } |