clarified signature;
authorwenzelm
Mon Jun 19 17:28:48 2017 +0200 (2017-06-19 ago)
changeset 66114c137a9f038a6
parent 66111 20304512a33b
child 66115 135bf45026ea
clarified signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/rendering.scala
src/Pure/PIDE/text.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_rendering.scala
src/Tools/jEdit/src/pretty_text_area.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Jun 17 20:24:22 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Jun 19 17:28:48 2017 +0200
     1.3 @@ -498,6 +498,8 @@
     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 +
     1.9      def node_required: Boolean
    1.10      def get_blob: Option[Blob]
    1.11  
     2.1 --- a/src/Pure/PIDE/rendering.scala	Sat Jun 17 20:24:22 2017 +0200
     2.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Jun 19 17:28:48 2017 +0200
     2.3 @@ -209,6 +209,8 @@
     2.4  {
     2.5    override def toString: String = "Rendering(" + snapshot.toString + ")"
     2.6  
     2.7 +  def model: Document.Model
     2.8 +
     2.9  
    2.10    /* completion */
    2.11  
    2.12 @@ -231,13 +233,12 @@
    2.13      history: Completion.History,
    2.14      unicode: Boolean,
    2.15      completed_range: Option[Text.Range],
    2.16 -    caret_range: Text.Range,
    2.17 -    try_get_text: Text.Range => Option[String]): (Boolean, Option[Completion.Result]) =
    2.18 +    caret_range: Text.Range): (Boolean, Option[Completion.Result]) =
    2.19    {
    2.20      semantic_completion(completed_range, caret_range) match {
    2.21        case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
    2.22        case Some(Text.Info(range, names: Completion.Names)) =>
    2.23 -        try_get_text(range) match {
    2.24 +        model.try_get_text(range) match {
    2.25            case Some(original) => (false, names.complete(range, history, unicode, original))
    2.26            case None => (false, None)
    2.27          }
     3.1 --- a/src/Pure/PIDE/text.scala	Sat Jun 17 20:24:22 2017 +0200
     3.2 +++ b/src/Pure/PIDE/text.scala	Mon Jun 19 17:28:48 2017 +0200
     3.3 @@ -73,6 +73,10 @@
     3.4        else Some(Range(this.start min that.start, this.stop max that.stop))
     3.5  
     3.6      def substring(text: String): String = text.substring(start, stop)
     3.7 +
     3.8 +    def try_substring(text: String): Option[String] =
     3.9 +      try { Some(substring(text)) }
    3.10 +      catch { case _: IndexOutOfBoundsException => None }
    3.11    }
    3.12  
    3.13  
     4.1 --- a/src/Tools/VSCode/src/document_model.scala	Sat Jun 17 20:24:22 2017 +0200
     4.2 +++ b/src/Tools/VSCode/src/document_model.scala	Mon Jun 19 17:28:48 2017 +0200
     4.3 @@ -39,7 +39,6 @@
     4.4      def text_length: Text.Offset = doc.text_length
     4.5      def text_range: Text.Range = doc.text_range
     4.6      def text: String = doc.text
     4.7 -    def try_get_text(range: Text.Range): Option[String] = doc.try_get_text(range)
     4.8  
     4.9      lazy val bytes: Bytes = Bytes(text)
    4.10      lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
    4.11 @@ -64,6 +63,14 @@
    4.12    published_diagnostics: List[Text.Info[Command.Results]] = Nil,
    4.13    published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model
    4.14  {
    4.15 +  model =>
    4.16 +
    4.17 +
    4.18 +  /* text */
    4.19 +
    4.20 +  def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
    4.21 +
    4.22 +
    4.23    /* external file */
    4.24  
    4.25    def external(b: Boolean): Document_Model = copy(external_file = b)
    4.26 @@ -84,7 +91,7 @@
    4.27      : (Boolean, Document.Node.Perspective_Text) =
    4.28    {
    4.29      if (is_theory) {
    4.30 -      val snapshot = this.snapshot()
    4.31 +      val snapshot = model.snapshot()
    4.32  
    4.33        val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
    4.34        val caret_range =
    4.35 @@ -192,7 +199,7 @@
    4.36    def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
    4.37  
    4.38    def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
    4.39 -    new VSCode_Rendering(this, snapshot)
    4.40 +    new VSCode_Rendering(snapshot, model)
    4.41    def rendering(): VSCode_Rendering = rendering(snapshot())
    4.42  
    4.43  
     5.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Jun 17 20:24:22 2017 +0200
     5.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Jun 19 17:28:48 2017 +0200
     5.3 @@ -65,11 +65,13 @@
     5.4      Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
     5.5  }
     5.6  
     5.7 -class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot)
     5.8 -  extends Rendering(snapshot, model.resources.options, model.session)
     5.9 +class VSCode_Rendering(snapshot: Document.Snapshot, _model: Document_Model)
    5.10 +  extends Rendering(snapshot, _model.resources.options, _model.session)
    5.11  {
    5.12    rendering =>
    5.13  
    5.14 +  def model: Document_Model = _model
    5.15 +
    5.16  
    5.17    /* completion */
    5.18  
    5.19 @@ -97,7 +99,7 @@
    5.20  
    5.21          val (no_completion, semantic_completion) =
    5.22            rendering.semantic_completion_result(
    5.23 -            history, false, syntax_completion.map(_.range), caret_range, doc.try_get_text(_))
    5.24 +            history, false, syntax_completion.map(_.range), caret_range)
    5.25  
    5.26          if (no_completion) Nil
    5.27          else {
    5.28 @@ -199,7 +201,7 @@
    5.29        (for {
    5.30          spell_checker <- model.resources.spell_checker.get.iterator
    5.31          spell_range <- spell_checker_ranges(model.content.text_range).iterator
    5.32 -        text <- model.content.try_get_text(spell_range).iterator
    5.33 +        text <- model.try_get_text(spell_range).iterator
    5.34          info <- spell_checker.marked_words(spell_range.start, text).iterator
    5.35        } yield info.range).toList
    5.36      Document_Model.Decoration.ranges("spell_checker", ranges)
     6.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sat Jun 17 20:24:22 2017 +0200
     6.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Jun 19 17:28:48 2017 +0200
     6.3 @@ -356,8 +356,7 @@
     6.4            opt_rendering match {
     6.5              case Some(rendering) =>
     6.6                rendering.semantic_completion_result(history, unicode, result0.map(_.range),
     6.7 -                JEdit_Lib.before_caret_range(text_area, rendering),
     6.8 -                JEdit_Lib.try_get_text(buffer, _))
     6.9 +                JEdit_Lib.before_caret_range(text_area, rendering))
    6.10              case None => (false, None)
    6.11            }
    6.12          }
    6.13 @@ -509,7 +508,7 @@
    6.14        val range = item.range
    6.15        if (text_field.isEditable) {
    6.16          val content = text_field.getText
    6.17 -        JEdit_Lib.try_get_text(content, range) match {
    6.18 +        range.try_substring(content) match {
    6.19            case Some(text) if text == item.original =>
    6.20              text_field.setText(
    6.21                content.substring(0, range.start) +
     7.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jun 17 20:24:22 2017 +0200
     7.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Jun 19 17:28:48 2017 +0200
     7.3 @@ -372,6 +372,10 @@
     7.4  
     7.5  object File_Model
     7.6  {
     7.7 +  def empty(session: Session): File_Model =
     7.8 +    File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
     7.9 +      false, Document.Node.no_perspective_text, Nil)
    7.10 +
    7.11    def init(session: Session,
    7.12      node_name: Document.Node.Name,
    7.13      text: String,
    7.14 @@ -396,6 +400,12 @@
    7.15    last_perspective: Document.Node.Perspective_Text,
    7.16    pending_edits: List[Text.Edit]) extends Document_Model
    7.17  {
    7.18 +  /* text */
    7.19 +
    7.20 +  def try_get_text(range: Text.Range): Option[String] =
    7.21 +    range.try_substring(content.text)
    7.22 +
    7.23 +
    7.24    /* header */
    7.25  
    7.26    def node_header: Document.Node.Header =
    7.27 @@ -457,6 +467,12 @@
    7.28  case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
    7.29    extends Document_Model
    7.30  {
    7.31 +  /* text */
    7.32 +
    7.33 +  def try_get_text(range: Text.Range): Option[String] =
    7.34 +    JEdit_Lib.try_get_text(buffer, range)
    7.35 +
    7.36 +
    7.37    /* header */
    7.38  
    7.39    def node_header(): Document.Node.Header =
     8.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Jun 17 20:24:22 2017 +0200
     8.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Jun 19 17:28:48 2017 +0200
     8.3 @@ -60,7 +60,8 @@
     8.4  {
     8.5    private val session = model.session
     8.6  
     8.7 -  def get_rendering(): JEdit_Rendering = JEdit_Rendering(model.snapshot(), PIDE.options.value)
     8.8 +  def get_rendering(): JEdit_Rendering =
     8.9 +    JEdit_Rendering(model.snapshot(), model, PIDE.options.value)
    8.10  
    8.11    val rich_text_area =
    8.12      new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
     9.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Jun 17 20:24:22 2017 +0200
     9.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Jun 19 17:28:48 2017 +0200
     9.3 @@ -68,7 +68,8 @@
     9.4            {
     9.5              Pretty_Tooltip.invoke(() =>
     9.6                {
     9.7 -                val rendering = JEdit_Rendering(snapshot, options)
     9.8 +                val model = File_Model.empty(PIDE.session)
     9.9 +                val rendering = JEdit_Rendering(snapshot, model, options)
    9.10                  val info = Text.Info(Text.Range.offside, body)
    9.11                  Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
    9.12                })
    10.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Jun 17 20:24:22 2017 +0200
    10.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Jun 19 17:28:48 2017 +0200
    10.3 @@ -175,10 +175,6 @@
    10.4      try { Some(buffer.getText(range.start, range.length)) }
    10.5      catch { case _: ArrayIndexOutOfBoundsException => None }
    10.6  
    10.7 -  def try_get_text(text: String, range: Text.Range): Option[String] =
    10.8 -    try { Some(range.substring(text)) }
    10.9 -    catch { case _: IndexOutOfBoundsException => None }
   10.10 -
   10.11  
   10.12    /* point range */
   10.13  
    11.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Jun 17 20:24:22 2017 +0200
    11.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Jun 19 17:28:48 2017 +0200
    11.3 @@ -21,8 +21,8 @@
    11.4  
    11.5  object JEdit_Rendering
    11.6  {
    11.7 -  def apply(snapshot: Document.Snapshot, options: Options): JEdit_Rendering =
    11.8 -    new JEdit_Rendering(snapshot, options)
    11.9 +  def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
   11.10 +    new JEdit_Rendering(snapshot, model, options)
   11.11  
   11.12  
   11.13    /* popup window bounds */
   11.14 @@ -148,9 +148,12 @@
   11.15  }
   11.16  
   11.17  
   11.18 -class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
   11.19 +class JEdit_Rendering(snapshot: Document.Snapshot, _model: Document_Model, options: Options)
   11.20    extends Rendering(snapshot, options, PIDE.session)
   11.21  {
   11.22 +  def model: Document_Model = _model
   11.23 +
   11.24 +
   11.25    /* colors */
   11.26  
   11.27    def color(s: String): Color =
    12.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sat Jun 17 20:24:22 2017 +0200
    12.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Jun 19 17:28:48 2017 +0200
    12.3 @@ -57,7 +57,8 @@
    12.4      formatted_body: XML.Body): (String, JEdit_Rendering) =
    12.5    {
    12.6      val (text, state) = document_state(base_snapshot, base_results, formatted_body)
    12.7 -    val rendering = JEdit_Rendering(state.snapshot(), PIDE.options.value)
    12.8 +    val model = File_Model.empty(PIDE.session)
    12.9 +    val rendering = JEdit_Rendering(state.snapshot(), model, PIDE.options.value)
   12.10      (text, rendering)
   12.11    }
   12.12  }