# HG changeset patch # User wenzelm # Date 1509980593 -3600 # Node ID e6a695d6a6b24d9e3e7c81a86badcd2e1524e129 # Parent 335a7dce7cb3720d19bfc35e3e014b38f67b6c8b tuned signature; diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Pure/PIDE/document.scala Mon Nov 06 16:03:13 2017 +0100 @@ -508,7 +508,7 @@ def is_theory: Boolean = node_name.is_theory override def toString: String = node_name.toString - def try_get_text(range: Text.Range): Option[String] + def get_text(range: Text.Range): Option[String] def node_required: Boolean def get_blob: Option[Blob] diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Pure/PIDE/line.scala Mon Nov 06 16:03:13 2017 +0100 @@ -128,7 +128,7 @@ lazy val text: String = Document.text(lines) - def try_get_text(range: Text.Range): Option[String] = + def get_text(range: Text.Range): Option[String] = if (text_range.contains(range)) Some(range.substring(text)) else None override def toString: String = text diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Mon Nov 06 16:03:13 2017 +0100 @@ -251,7 +251,7 @@ semantic_completion(completed_range, caret_range) match { case Some(Text.Info(_, Completion.No_Completion)) => (true, None) case Some(Text.Info(range, names: Completion.Names)) => - model.try_get_text(range) match { + model.get_text(range) match { case Some(original) => (false, names.complete(range, history, unicode, original)) case None => (false, None) } @@ -334,7 +334,7 @@ for { r1 <- language_path(before_caret_range(caret)) - s1 <- model.try_get_text(r1) + s1 <- model.get_text(r1) if is_wrapped(s1) r2 = Text.Range(r1.start + 1, r1.stop - 1) s2 = s1.substring(1, s1.length - 1) diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Pure/Tools/bibtex.scala --- a/src/Pure/Tools/bibtex.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Pure/Tools/bibtex.scala Mon Nov 06 16:03:13 2017 +0100 @@ -52,7 +52,7 @@ Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret)) name1 <- Completion.clean_name(name) - original <- rendering.model.try_get_text(r) + original <- rendering.model.get_text(r) original1 <- Completion.clean_name(Library.perhaps_unquote(original)) entries = diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Pure/Tools/spell_checker.scala --- a/src/Pure/Tools/spell_checker.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Pure/Tools/spell_checker.scala Mon Nov 06 16:03:13 2017 +0100 @@ -56,7 +56,7 @@ { for { spell_range <- rendering.spell_checker_point(range) - text <- rendering.model.try_get_text(spell_range) + text <- rendering.model.get_text(spell_range) info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption } yield info } diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Mon Nov 06 16:03:13 2017 +0100 @@ -79,7 +79,7 @@ /* content */ - def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range) + def get_text(range: Text.Range): Option[String] = content.doc.get_text(range) def set_version(new_version: Long): Document_Model = copy(version = Some(new_version)) diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/VSCode/src/vscode_spell_checker.scala --- a/src/Tools/VSCode/src/vscode_spell_checker.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_spell_checker.scala Mon Nov 06 16:03:13 2017 +0100 @@ -19,7 +19,7 @@ (for { spell_checker <- rendering.resources.spell_checker.get.iterator spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator - text <- model.try_get_text(spell_range).iterator + text <- model.get_text(spell_range).iterator info <- spell_checker.marked_words(spell_range.start, text).iterator } yield info.range).toList Document_Model.Decoration.ranges("spell_checker", ranges) diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Mon Nov 06 16:03:13 2017 +0100 @@ -171,7 +171,7 @@ val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine) val line_start = line_range.start for { - line_text <- JEdit_Lib.try_get_text(buffer, line_range) + line_text <- JEdit_Lib.get_text(buffer, line_range) result <- syntax.complete( history, unicode, explicit, line_start, line_text, caret - line_start, context) @@ -192,7 +192,7 @@ val range = item.range if (buffer.isEditable) { JEdit_Lib.buffer_edit(buffer) { - JEdit_Lib.try_get_text(buffer, range) match { + JEdit_Lib.get_text(buffer, range) match { case Some(text) if text == item.original => text_area.getSelectionAtOffset(text_area.getCaretPosition) match { diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Mon Nov 06 16:03:13 2017 +0100 @@ -406,7 +406,7 @@ { /* text */ - def try_get_text(range: Text.Range): Option[String] = + def get_text(range: Text.Range): Option[String] = range.try_substring(content.text) @@ -473,8 +473,8 @@ { /* text */ - def try_get_text(range: Text.Range): Option[String] = - JEdit_Lib.try_get_text(buffer, range) + def get_text(range: Text.Range): Option[String] = + JEdit_Lib.get_text(buffer, range) /* header */ diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Mon Nov 06 16:03:13 2017 +0100 @@ -309,7 +309,7 @@ val text1 = if (text_area.getSelectionCount == 0) { def pad(range: Text.Range): String = - if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n" + if (JEdit_Lib.get_text(buffer, range) == Some("\n")) "" else "\n" val caret = JEdit_Lib.caret_range(text_area) val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1) diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Nov 06 16:03:13 2017 +0100 @@ -171,7 +171,7 @@ /* get text */ - def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = + def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = try { Some(buffer.getText(range.start, range.length)) } catch { case _: ArrayIndexOutOfBoundsException => None } @@ -262,7 +262,7 @@ try { val p = text_area.offsetToXY(range.start) val (q, r) = - if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n")) + if (get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n")) (text_area.offsetToXY(stop - 1), char_width) else if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end)) diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Nov 06 16:03:13 2017 +0100 @@ -345,7 +345,7 @@ for { spell_checker <- PIDE.plugin.spell_checker.get spell_range <- rendering.spell_checker_ranges(line_range) - text <- JEdit_Lib.try_get_text(buffer, spell_range) + text <- JEdit_Lib.get_text(buffer, spell_range) info <- spell_checker.marked_words(spell_range.start, text) r <- JEdit_Lib.gfx_range(text_area, info.range) } { @@ -544,7 +544,7 @@ // search pattern for { regex <- search_pattern - text <- JEdit_Lib.try_get_text(buffer, line_range) + text <- JEdit_Lib.get_text(buffer, line_range) m <- regex.findAllMatchIn(text) range = Text.Range(m.start, m.end) + line_range.start r <- JEdit_Lib.gfx_range(text_area, range) diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/jEdit/src/syntax_style.scala --- a/src/Tools/jEdit/src/syntax_style.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/jEdit/src/syntax_style.scala Mon Nov 06 16:03:13 2017 +0100 @@ -147,7 +147,7 @@ text_area.getSelection.foreach(sel => { val before = JEdit_Lib.point_range(buffer, sel.getStart - 1) - JEdit_Lib.try_get_text(buffer, before) match { + JEdit_Lib.get_text(buffer, before) match { case Some(s) if HTML.is_control(s) => text_area.extendSelection(before.start, before.stop) case _ => diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/jEdit/src/text_structure.scala Mon Nov 06 16:03:13 2017 +0100 @@ -192,7 +192,7 @@ def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) = { - val text = JEdit_Lib.try_get_text(buffer, range).getOrElse("") + val text = JEdit_Lib.get_text(buffer, range).getOrElse("") val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt) val toks1 = toks.filterNot(_.is_space) (toks1, ctxt1) diff -r 335a7dce7cb3 -r e6a695d6a6b2 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Sun Nov 05 17:45:17 2017 +0100 +++ b/src/Tools/jEdit/src/token_markup.scala Mon Nov 06 16:03:13 2017 +0100 @@ -74,7 +74,7 @@ val line_context = Line_Context.before(buffer, line) for { ctxt <- line_context.context - text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line)) + text <- JEdit_Lib.get_text(buffer, JEdit_Lib.line_range(buffer, line)) } yield Token.explode_line(syntax.keywords, text, ctxt)._1 } @@ -175,7 +175,7 @@ case None => buffer.getLength } - val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("") + val text = JEdit_Lib.get_text(buffer, Text.Range(start, stop)).getOrElse("") val spans = syntax.parse_spans(text) (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator).