# HG changeset patch
# User wenzelm
# Date 1497886128 -7200
# Node ID c137a9f038a644b264aee01aff5943c49eeb15be
# Parent  20304512a33b8b298ae1129c410d834456e652e4
clarified signature;

diff -r 20304512a33b -r c137a9f038a6 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -498,6 +498,8 @@
     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 node_required: Boolean
     def get_blob: Option[Blob]
 
diff -r 20304512a33b -r c137a9f038a6 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -209,6 +209,8 @@
 {
   override def toString: String = "Rendering(" + snapshot.toString + ")"
 
+  def model: Document.Model
+
 
   /* completion */
 
@@ -231,13 +233,12 @@
     history: Completion.History,
     unicode: Boolean,
     completed_range: Option[Text.Range],
-    caret_range: Text.Range,
-    try_get_text: Text.Range => Option[String]): (Boolean, Option[Completion.Result]) =
+    caret_range: Text.Range): (Boolean, Option[Completion.Result]) =
   {
     semantic_completion(completed_range, caret_range) match {
       case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
       case Some(Text.Info(range, names: Completion.Names)) =>
-        try_get_text(range) match {
+        model.try_get_text(range) match {
           case Some(original) => (false, names.complete(range, history, unicode, original))
           case None => (false, None)
         }
diff -r 20304512a33b -r c137a9f038a6 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Pure/PIDE/text.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -73,6 +73,10 @@
       else Some(Range(this.start min that.start, this.stop max that.stop))
 
     def substring(text: String): String = text.substring(start, stop)
+
+    def try_substring(text: String): Option[String] =
+      try { Some(substring(text)) }
+      catch { case _: IndexOutOfBoundsException => None }
   }
 
 
diff -r 20304512a33b -r c137a9f038a6 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -39,7 +39,6 @@
     def text_length: Text.Offset = doc.text_length
     def text_range: Text.Range = doc.text_range
     def text: String = doc.text
-    def try_get_text(range: Text.Range): Option[String] = doc.try_get_text(range)
 
     lazy val bytes: Bytes = Bytes(text)
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
@@ -64,6 +63,14 @@
   published_diagnostics: List[Text.Info[Command.Results]] = Nil,
   published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model
 {
+  model =>
+
+
+  /* text */
+
+  def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
+
+
   /* external file */
 
   def external(b: Boolean): Document_Model = copy(external_file = b)
@@ -84,7 +91,7 @@
     : (Boolean, Document.Node.Perspective_Text) =
   {
     if (is_theory) {
-      val snapshot = this.snapshot()
+      val snapshot = model.snapshot()
 
       val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
       val caret_range =
@@ -192,7 +199,7 @@
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 
   def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
-    new VSCode_Rendering(this, snapshot)
+    new VSCode_Rendering(snapshot, model)
   def rendering(): VSCode_Rendering = rendering(snapshot())
 
 
diff -r 20304512a33b -r c137a9f038a6 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -65,11 +65,13 @@
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
 }
 
-class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot)
-  extends Rendering(snapshot, model.resources.options, model.session)
+class VSCode_Rendering(snapshot: Document.Snapshot, _model: Document_Model)
+  extends Rendering(snapshot, _model.resources.options, _model.session)
 {
   rendering =>
 
+  def model: Document_Model = _model
+
 
   /* completion */
 
@@ -97,7 +99,7 @@
 
         val (no_completion, semantic_completion) =
           rendering.semantic_completion_result(
-            history, false, syntax_completion.map(_.range), caret_range, doc.try_get_text(_))
+            history, false, syntax_completion.map(_.range), caret_range)
 
         if (no_completion) Nil
         else {
@@ -199,7 +201,7 @@
       (for {
         spell_checker <- model.resources.spell_checker.get.iterator
         spell_range <- spell_checker_ranges(model.content.text_range).iterator
-        text <- model.content.try_get_text(spell_range).iterator
+        text <- model.try_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 20304512a33b -r c137a9f038a6 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -356,8 +356,7 @@
           opt_rendering match {
             case Some(rendering) =>
               rendering.semantic_completion_result(history, unicode, result0.map(_.range),
-                JEdit_Lib.before_caret_range(text_area, rendering),
-                JEdit_Lib.try_get_text(buffer, _))
+                JEdit_Lib.before_caret_range(text_area, rendering))
             case None => (false, None)
           }
         }
@@ -509,7 +508,7 @@
       val range = item.range
       if (text_field.isEditable) {
         val content = text_field.getText
-        JEdit_Lib.try_get_text(content, range) match {
+        range.try_substring(content) match {
           case Some(text) if text == item.original =>
             text_field.setText(
               content.substring(0, range.start) +
diff -r 20304512a33b -r c137a9f038a6 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -372,6 +372,10 @@
 
 object File_Model
 {
+  def empty(session: Session): File_Model =
+    File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
+      false, Document.Node.no_perspective_text, Nil)
+
   def init(session: Session,
     node_name: Document.Node.Name,
     text: String,
@@ -396,6 +400,12 @@
   last_perspective: Document.Node.Perspective_Text,
   pending_edits: List[Text.Edit]) extends Document_Model
 {
+  /* text */
+
+  def try_get_text(range: Text.Range): Option[String] =
+    range.try_substring(content.text)
+
+
   /* header */
 
   def node_header: Document.Node.Header =
@@ -457,6 +467,12 @@
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
   extends Document_Model
 {
+  /* text */
+
+  def try_get_text(range: Text.Range): Option[String] =
+    JEdit_Lib.try_get_text(buffer, range)
+
+
   /* header */
 
   def node_header(): Document.Node.Header =
diff -r 20304512a33b -r c137a9f038a6 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -60,7 +60,8 @@
 {
   private val session = model.session
 
-  def get_rendering(): JEdit_Rendering = JEdit_Rendering(model.snapshot(), PIDE.options.value)
+  def get_rendering(): JEdit_Rendering =
+    JEdit_Rendering(model.snapshot(), model, PIDE.options.value)
 
   val rich_text_area =
     new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
diff -r 20304512a33b -r c137a9f038a6 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -68,7 +68,8 @@
           {
             Pretty_Tooltip.invoke(() =>
               {
-                val rendering = JEdit_Rendering(snapshot, options)
+                val model = File_Model.empty(PIDE.session)
+                val rendering = JEdit_Rendering(snapshot, model, options)
                 val info = Text.Info(Text.Range.offside, body)
                 Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
               })
diff -r 20304512a33b -r c137a9f038a6 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -175,10 +175,6 @@
     try { Some(buffer.getText(range.start, range.length)) }
     catch { case _: ArrayIndexOutOfBoundsException => None }
 
-  def try_get_text(text: String, range: Text.Range): Option[String] =
-    try { Some(range.substring(text)) }
-    catch { case _: IndexOutOfBoundsException => None }
-
 
   /* point range */
 
diff -r 20304512a33b -r c137a9f038a6 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -21,8 +21,8 @@
 
 object JEdit_Rendering
 {
-  def apply(snapshot: Document.Snapshot, options: Options): JEdit_Rendering =
-    new JEdit_Rendering(snapshot, options)
+  def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
+    new JEdit_Rendering(snapshot, model, options)
 
 
   /* popup window bounds */
@@ -148,9 +148,12 @@
 }
 
 
-class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
+class JEdit_Rendering(snapshot: Document.Snapshot, _model: Document_Model, options: Options)
   extends Rendering(snapshot, options, PIDE.session)
 {
+  def model: Document_Model = _model
+
+
   /* colors */
 
   def color(s: String): Color =
diff -r 20304512a33b -r c137a9f038a6 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Jun 19 17:28:48 2017 +0200
@@ -57,7 +57,8 @@
     formatted_body: XML.Body): (String, JEdit_Rendering) =
   {
     val (text, state) = document_state(base_snapshot, base_results, formatted_body)
-    val rendering = JEdit_Rendering(state.snapshot(), PIDE.options.value)
+    val model = File_Model.empty(PIDE.session)
+    val rendering = JEdit_Rendering(state.snapshot(), model, PIDE.options.value)
     (text, rendering)
   }
 }