tuned signature;
authorwenzelm
Mon Nov 06 16:03:13 2017 +0100 (18 months ago)
changeset 67014e6a695d6a6b2
parent 67013 335a7dce7cb3
child 67015 1a9e2a2bf251
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/line.scala
src/Pure/PIDE/rendering.scala
src/Pure/Tools/bibtex.scala
src/Pure/Tools/spell_checker.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/vscode_spell_checker.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/syntax_style.scala
src/Tools/jEdit/src/text_structure.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sun Nov 05 17:45:17 2017 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Nov 06 16:03:13 2017 +0100
     1.3 @@ -508,7 +508,7 @@
     1.4      def is_theory: Boolean = node_name.is_theory
     1.5      override def toString: String = node_name.toString
     1.6  
     1.7 -    def try_get_text(range: Text.Range): Option[String]
     1.8 +    def get_text(range: Text.Range): Option[String]
     1.9  
    1.10      def node_required: Boolean
    1.11      def get_blob: Option[Blob]
     2.1 --- a/src/Pure/PIDE/line.scala	Sun Nov 05 17:45:17 2017 +0100
     2.2 +++ b/src/Pure/PIDE/line.scala	Mon Nov 06 16:03:13 2017 +0100
     2.3 @@ -128,7 +128,7 @@
     2.4  
     2.5      lazy val text: String = Document.text(lines)
     2.6  
     2.7 -    def try_get_text(range: Text.Range): Option[String] =
     2.8 +    def get_text(range: Text.Range): Option[String] =
     2.9        if (text_range.contains(range)) Some(range.substring(text)) else None
    2.10  
    2.11      override def toString: String = text
     3.1 --- a/src/Pure/PIDE/rendering.scala	Sun Nov 05 17:45:17 2017 +0100
     3.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Nov 06 16:03:13 2017 +0100
     3.3 @@ -251,7 +251,7 @@
     3.4      semantic_completion(completed_range, caret_range) match {
     3.5        case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
     3.6        case Some(Text.Info(range, names: Completion.Names)) =>
     3.7 -        model.try_get_text(range) match {
     3.8 +        model.get_text(range) match {
     3.9            case Some(original) => (false, names.complete(range, history, unicode, original))
    3.10            case None => (false, None)
    3.11          }
    3.12 @@ -334,7 +334,7 @@
    3.13  
    3.14      for {
    3.15        r1 <- language_path(before_caret_range(caret))
    3.16 -      s1 <- model.try_get_text(r1)
    3.17 +      s1 <- model.get_text(r1)
    3.18        if is_wrapped(s1)
    3.19        r2 = Text.Range(r1.start + 1, r1.stop - 1)
    3.20        s2 = s1.substring(1, s1.length - 1)
     4.1 --- a/src/Pure/Tools/bibtex.scala	Sun Nov 05 17:45:17 2017 +0100
     4.2 +++ b/src/Pure/Tools/bibtex.scala	Mon Nov 06 16:03:13 2017 +0100
     4.3 @@ -52,7 +52,7 @@
     4.4        Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
     4.5        name1 <- Completion.clean_name(name)
     4.6  
     4.7 -      original <- rendering.model.try_get_text(r)
     4.8 +      original <- rendering.model.get_text(r)
     4.9        original1 <- Completion.clean_name(Library.perhaps_unquote(original))
    4.10  
    4.11        entries =
     5.1 --- a/src/Pure/Tools/spell_checker.scala	Sun Nov 05 17:45:17 2017 +0100
     5.2 +++ b/src/Pure/Tools/spell_checker.scala	Mon Nov 06 16:03:13 2017 +0100
     5.3 @@ -56,7 +56,7 @@
     5.4    {
     5.5      for {
     5.6        spell_range <- rendering.spell_checker_point(range)
     5.7 -      text <- rendering.model.try_get_text(spell_range)
     5.8 +      text <- rendering.model.get_text(spell_range)
     5.9        info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
    5.10      } yield info
    5.11    }
     6.1 --- a/src/Tools/VSCode/src/document_model.scala	Sun Nov 05 17:45:17 2017 +0100
     6.2 +++ b/src/Tools/VSCode/src/document_model.scala	Mon Nov 06 16:03:13 2017 +0100
     6.3 @@ -79,7 +79,7 @@
     6.4  
     6.5    /* content */
     6.6  
     6.7 -  def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
     6.8 +  def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
     6.9  
    6.10    def set_version(new_version: Long): Document_Model = copy(version = Some(new_version))
    6.11  
     7.1 --- a/src/Tools/VSCode/src/vscode_spell_checker.scala	Sun Nov 05 17:45:17 2017 +0100
     7.2 +++ b/src/Tools/VSCode/src/vscode_spell_checker.scala	Mon Nov 06 16:03:13 2017 +0100
     7.3 @@ -19,7 +19,7 @@
     7.4        (for {
     7.5          spell_checker <- rendering.resources.spell_checker.get.iterator
     7.6          spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator
     7.7 -        text <- model.try_get_text(spell_range).iterator
     7.8 +        text <- model.get_text(spell_range).iterator
     7.9          info <- spell_checker.marked_words(spell_range.start, text).iterator
    7.10        } yield info.range).toList
    7.11      Document_Model.Decoration.ranges("spell_checker", ranges)
     8.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sun Nov 05 17:45:17 2017 +0100
     8.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Nov 06 16:03:13 2017 +0100
     8.3 @@ -171,7 +171,7 @@
     8.4            val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine)
     8.5            val line_start = line_range.start
     8.6            for {
     8.7 -            line_text <- JEdit_Lib.try_get_text(buffer, line_range)
     8.8 +            line_text <- JEdit_Lib.get_text(buffer, line_range)
     8.9              result <-
    8.10                syntax.complete(
    8.11                  history, unicode, explicit, line_start, line_text, caret - line_start, context)
    8.12 @@ -192,7 +192,7 @@
    8.13        val range = item.range
    8.14        if (buffer.isEditable) {
    8.15          JEdit_Lib.buffer_edit(buffer) {
    8.16 -          JEdit_Lib.try_get_text(buffer, range) match {
    8.17 +          JEdit_Lib.get_text(buffer, range) match {
    8.18              case Some(text) if text == item.original =>
    8.19                text_area.getSelectionAtOffset(text_area.getCaretPosition) match {
    8.20  
     9.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 05 17:45:17 2017 +0100
     9.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Nov 06 16:03:13 2017 +0100
     9.3 @@ -406,7 +406,7 @@
     9.4  {
     9.5    /* text */
     9.6  
     9.7 -  def try_get_text(range: Text.Range): Option[String] =
     9.8 +  def get_text(range: Text.Range): Option[String] =
     9.9      range.try_substring(content.text)
    9.10  
    9.11  
    9.12 @@ -473,8 +473,8 @@
    9.13  {
    9.14    /* text */
    9.15  
    9.16 -  def try_get_text(range: Text.Range): Option[String] =
    9.17 -    JEdit_Lib.try_get_text(buffer, range)
    9.18 +  def get_text(range: Text.Range): Option[String] =
    9.19 +    JEdit_Lib.get_text(buffer, range)
    9.20  
    9.21  
    9.22    /* header */
    10.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sun Nov 05 17:45:17 2017 +0100
    10.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Nov 06 16:03:13 2017 +0100
    10.3 @@ -309,7 +309,7 @@
    10.4        val text1 =
    10.5          if (text_area.getSelectionCount == 0) {
    10.6            def pad(range: Text.Range): String =
    10.7 -            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
    10.8 +            if (JEdit_Lib.get_text(buffer, range) == Some("\n")) "" else "\n"
    10.9  
   10.10            val caret = JEdit_Lib.caret_range(text_area)
   10.11            val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
    11.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Nov 05 17:45:17 2017 +0100
    11.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 06 16:03:13 2017 +0100
    11.3 @@ -171,7 +171,7 @@
    11.4  
    11.5    /* get text */
    11.6  
    11.7 -  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
    11.8 +  def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
    11.9      try { Some(buffer.getText(range.start, range.length)) }
   11.10      catch { case _: ArrayIndexOutOfBoundsException => None }
   11.11  
   11.12 @@ -262,7 +262,7 @@
   11.13        try {
   11.14          val p = text_area.offsetToXY(range.start)
   11.15          val (q, r) =
   11.16 -          if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
   11.17 +          if (get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
   11.18              (text_area.offsetToXY(stop - 1), char_width)
   11.19            else if (stop >= end)
   11.20              (text_area.offsetToXY(end), char_width * (stop - end))
    12.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Nov 05 17:45:17 2017 +0100
    12.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 06 16:03:13 2017 +0100
    12.3 @@ -345,7 +345,7 @@
    12.4              for {
    12.5                spell_checker <- PIDE.plugin.spell_checker.get
    12.6                spell_range <- rendering.spell_checker_ranges(line_range)
    12.7 -              text <- JEdit_Lib.try_get_text(buffer, spell_range)
    12.8 +              text <- JEdit_Lib.get_text(buffer, spell_range)
    12.9                info <- spell_checker.marked_words(spell_range.start, text)
   12.10                r <- JEdit_Lib.gfx_range(text_area, info.range)
   12.11              } {
   12.12 @@ -544,7 +544,7 @@
   12.13              // search pattern
   12.14              for {
   12.15                regex <- search_pattern
   12.16 -              text <- JEdit_Lib.try_get_text(buffer, line_range)
   12.17 +              text <- JEdit_Lib.get_text(buffer, line_range)
   12.18                m <- regex.findAllMatchIn(text)
   12.19                range = Text.Range(m.start, m.end) + line_range.start
   12.20                r <- JEdit_Lib.gfx_range(text_area, range)
    13.1 --- a/src/Tools/jEdit/src/syntax_style.scala	Sun Nov 05 17:45:17 2017 +0100
    13.2 +++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Nov 06 16:03:13 2017 +0100
    13.3 @@ -147,7 +147,7 @@
    13.4  
    13.5      text_area.getSelection.foreach(sel => {
    13.6        val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
    13.7 -      JEdit_Lib.try_get_text(buffer, before) match {
    13.8 +      JEdit_Lib.get_text(buffer, before) match {
    13.9          case Some(s) if HTML.is_control(s) =>
   13.10            text_area.extendSelection(before.start, before.stop)
   13.11          case _ =>
    14.1 --- a/src/Tools/jEdit/src/text_structure.scala	Sun Nov 05 17:45:17 2017 +0100
    14.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Mon Nov 06 16:03:13 2017 +0100
    14.3 @@ -192,7 +192,7 @@
    14.4    def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords,
    14.5      range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) =
    14.6    {
    14.7 -    val text = JEdit_Lib.try_get_text(buffer, range).getOrElse("")
    14.8 +    val text = JEdit_Lib.get_text(buffer, range).getOrElse("")
    14.9      val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt)
   14.10      val toks1 = toks.filterNot(_.is_space)
   14.11      (toks1, ctxt1)
    15.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Nov 05 17:45:17 2017 +0100
    15.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Mon Nov 06 16:03:13 2017 +0100
    15.3 @@ -74,7 +74,7 @@
    15.4      val line_context = Line_Context.before(buffer, line)
    15.5      for {
    15.6        ctxt <- line_context.context
    15.7 -      text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line))
    15.8 +      text <- JEdit_Lib.get_text(buffer, JEdit_Lib.line_range(buffer, line))
    15.9      } yield Token.explode_line(syntax.keywords, text, ctxt)._1
   15.10    }
   15.11  
   15.12 @@ -175,7 +175,7 @@
   15.13            case None => buffer.getLength
   15.14          }
   15.15  
   15.16 -      val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("")
   15.17 +      val text = JEdit_Lib.get_text(buffer, Text.Range(start, stop)).getOrElse("")
   15.18        val spans = syntax.parse_spans(text)
   15.19  
   15.20        (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator).