# HG changeset patch
# User wenzelm
# Date 1607523264 -3600
# Node ID 3a27e6f83ce160d625c1a26aea8761dcb6373956
# Parent  e0f6fa6ff3d0e4ba49459df56c7d48f1f6284c86
clarified signature;

diff -r e0f6fa6ff3d0 -r 3a27e6f83ce1 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Dec 09 14:29:30 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 09 15:14:24 2020 +0100
@@ -230,14 +230,14 @@
       Markup.Markdown_Bullet.name)
 }
 
-abstract class Rendering(
+class Rendering(
   val snapshot: Document.Snapshot,
   val options: Options,
   val session: Session)
 {
   override def toString: String = "Rendering(" + snapshot.toString + ")"
 
-  def model: Document.Model
+  def get_text(range: Text.Range): Option[String] = None
 
 
   /* caret */
@@ -275,7 +275,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.get_text(range) match {
+        get_text(range) match {
           case Some(original) => (false, names.complete(range, history, unicode, original))
           case None => (false, None)
         }
@@ -358,7 +358,7 @@
 
     for {
       Text.Info(r1, delimited) <- language_path(before_caret_range(caret))
-      s1 <- model.get_text(r1)
+      s1 <- get_text(r1)
       (r2, s2) <-
         if (is_wrapped(s1)) {
           Some((Text.Range(r1.start + 1, r1.stop - 1), s1.substring(1, s1.length - 1)))
diff -r e0f6fa6ff3d0 -r 3a27e6f83ce1 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Wed Dec 09 14:29:30 2020 +0100
+++ b/src/Pure/Thy/bibtex.scala	Wed Dec 09 15:14:24 2020 +0100
@@ -196,7 +196,7 @@
       Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
       name1 <- Completion.clean_name(name)
 
-      original <- rendering.model.get_text(r)
+      original <- rendering.get_text(r)
       original1 <- Completion.clean_name(Library.perhaps_unquote(original))
 
       entries =
diff -r e0f6fa6ff3d0 -r 3a27e6f83ce1 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Dec 09 14:29:30 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Dec 09 15:14:24 2020 +0100
@@ -118,10 +118,6 @@
             }
           }
         }
-      def make_rendering(snapshot: Document.Snapshot): Rendering =
-        new Rendering(snapshot, options, session) {
-          override def model: Document.Model = ???
-        }
 
       object Build_Session_Errors
       {
@@ -231,7 +227,7 @@
       session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories")
         {
           case snapshot =>
-            val rendering = make_rendering(snapshot)
+            val rendering = new Rendering(snapshot, options, session)
 
             def export(name: String, xml: XML.Body, compress: Boolean = true)
             {
diff -r e0f6fa6ff3d0 -r 3a27e6f83ce1 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Wed Dec 09 14:29:30 2020 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Wed Dec 09 15:14:24 2020 +0100
@@ -56,7 +56,7 @@
   {
     for {
       spell_range <- rendering.spell_checker_point(range)
-      text <- rendering.model.get_text(spell_range)
+      text <- rendering.get_text(spell_range)
       info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
     } yield info
   }
diff -r e0f6fa6ff3d0 -r 3a27e6f83ce1 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 09 14:29:30 2020 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 09 15:14:24 2020 +0100
@@ -65,14 +65,15 @@
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
 }
 
-class VSCode_Rendering(snapshot: Document.Snapshot, _model: VSCode_Model)
-  extends Rendering(snapshot, _model.resources.options, _model.session)
+class VSCode_Rendering(snapshot: Document.Snapshot, val model: VSCode_Model)
+  extends Rendering(snapshot, model.resources.options, model.session)
 {
   rendering =>
 
-  def model: VSCode_Model = _model
   def resources: VSCode_Resources = model.resources
 
+  override def get_text(range: Text.Range): Option[String] = model.get_text(range)
+
 
   /* bibtex */
 
diff -r e0f6fa6ff3d0 -r 3a27e6f83ce1 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 09 14:29:30 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 09 15:14:24 2020 +0100
@@ -161,10 +161,10 @@
 }
 
 
-class JEdit_Rendering(snapshot: Document.Snapshot, _model: Document_Model, options: Options)
+class JEdit_Rendering(snapshot: Document.Snapshot, model: Document_Model, options: Options)
   extends Rendering(snapshot, options, PIDE.session)
 {
-  def model: Document_Model = _model
+  override def get_text(range: Text.Range): Option[String] = model.get_text(range)
 
 
   /* colors */