# 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).