540 |
540 |
541 |
541 |
542 /* error navigation */ |
542 /* error navigation */ |
543 |
543 |
544 private def goto_error( |
544 private def goto_error( |
545 view: View, range: Text.Range, which: String = "")(get: List[Text.Markup] => Option[Text.Markup]) |
545 view: View, |
|
546 range: Text.Range, |
|
547 avoid_range: Text.Range = Text.Range.offside, |
|
548 which: String = "")(get: List[Text.Markup] => Option[Text.Markup]) |
546 { |
549 { |
547 GUI_Thread.require {} |
550 GUI_Thread.require {} |
548 |
551 |
549 val text_area = view.getTextArea |
552 val text_area = view.getTextArea |
550 for (doc_view <- Document_View.get(text_area)) { |
553 for (doc_view <- Document_View.get(text_area)) { |
551 val rendering = doc_view.get_rendering() |
554 val rendering = doc_view.get_rendering() |
552 get(rendering.errors(range)) match { |
555 val errs = rendering.errors(range).filterNot(_.range.overlaps(avoid_range)) |
|
556 get(errs) match { |
553 case Some(err) => |
557 case Some(err) => |
554 PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start) |
558 PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start) |
555 case None => |
559 case None => |
556 view.getStatus.setMessageAndClear("No " + which + "error in current document snapshot") |
560 view.getStatus.setMessageAndClear("No " + which + "error in current document snapshot") |
557 } |
561 } |
562 goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.headOption) |
566 goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.headOption) |
563 |
567 |
564 def goto_last_error(view: View): Unit = |
568 def goto_last_error(view: View): Unit = |
565 goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.lastOption) |
569 goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.lastOption) |
566 |
570 |
567 def goto_prev_error(view: View): Unit = |
571 def goto_prev_error(view: View) |
568 goto_error(view, JEdit_Lib.buffer_range_to_caret(view.getTextArea), which = "previous ")( |
572 { |
569 list => |
573 val caret_range = JEdit_Lib.caret_range(view.getTextArea) |
570 list.reverse match { |
574 val range = Text.Range(0, caret_range.stop) |
571 case _ :: err :: _ => Some(err) |
575 goto_error(view, range, avoid_range = caret_range, which = "previous ")(_.lastOption) |
572 case _ => None |
576 } |
573 }) |
577 |
574 |
578 def goto_next_error(view: View) |
575 def goto_next_error(view: View): Unit = |
579 { |
576 goto_error(view, JEdit_Lib.buffer_range_from_caret(view.getTextArea), which = "next ")( |
580 val caret_range = JEdit_Lib.caret_range(view.getTextArea) |
577 { |
581 val range = Text.Range(caret_range.start, view.getBuffer.getLength) |
578 case _ :: err :: _ => Some(err) |
582 goto_error(view, range, avoid_range = caret_range, which = "next ")(_.headOption) |
579 case _ => None |
583 } |
580 }) |
|
581 } |
584 } |