clarified signature: maintan Text.Length within Line.Document;
authorwenzelm
Wed Dec 28 17:26:38 2016 +0100 (2016-12-28)
changeset 64683c0c09b6dfbe0
parent 64682 7e119f32276a
child 64684 fe2c9c215b36
clarified signature: maintan Text.Length within Line.Document;
src/Pure/PIDE/line.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_rendering.scala
     1.1 --- a/src/Pure/PIDE/line.scala	Wed Dec 28 17:10:09 2016 +0100
     1.2 +++ b/src/Pure/PIDE/line.scala	Wed Dec 28 17:26:38 2016 +0100
     1.3 @@ -80,21 +80,14 @@
     1.4  
     1.5    object Document
     1.6    {
     1.7 -    val empty: Document = new Document(Nil)
     1.8 -
     1.9 -    def apply(lines: List[Line]): Document =
    1.10 -      if (lines.isEmpty) empty
    1.11 -      else new Document(lines)
    1.12 -
    1.13 -    def apply(text: String): Document =
    1.14 -      if (text == "") empty
    1.15 -      else if (text.contains('\r'))
    1.16 -        new Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))))
    1.17 +    def apply(text: String, text_length: Text.Length): Document =
    1.18 +      if (text.contains('\r'))
    1.19 +        Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))), text_length)
    1.20        else
    1.21 -        new Document(Library.split_lines(text).map(s => Line(s)))
    1.22 +        Document(Library.split_lines(text).map(s => Line(s)), text_length)
    1.23    }
    1.24  
    1.25 -  final class Document private(val lines: List[Line])
    1.26 +  sealed case class Document(lines: List[Line], text_length: Text.Length)
    1.27    {
    1.28      def make_text: String = lines.mkString("", "\n", "")
    1.29  
    1.30 @@ -107,7 +100,7 @@
    1.31        }
    1.32      override def hashCode(): Int = lines.hashCode
    1.33  
    1.34 -    def position(text_offset: Text.Offset, text_length: Text.Length): Position =
    1.35 +    def position(text_offset: Text.Offset): Position =
    1.36      {
    1.37        @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
    1.38        {
    1.39 @@ -123,12 +116,10 @@
    1.40        move(text_offset, 0, lines)
    1.41      }
    1.42  
    1.43 -    def range(text_range: Text.Range, text_length: Text.Length): Range =
    1.44 -      Range(
    1.45 -        position(text_range.start, text_length),
    1.46 -        position(text_range.stop, text_length))
    1.47 +    def range(text_range: Text.Range): Range =
    1.48 +      Range(position(text_range.start), position(text_range.stop))
    1.49  
    1.50 -    def offset(pos: Position, text_length: Text.Length): Option[Text.Offset] =
    1.51 +    def offset(pos: Position): Option[Text.Offset] =
    1.52      {
    1.53        val l = pos.line
    1.54        val c = pos.column
     2.1 --- a/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:10:09 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/document_model.scala	Wed Dec 28 17:26:38 2016 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  
     2.6  case class Document_Model(
     2.7 -  session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Text.Length,
     2.8 +  session: Session, doc: Line.Document, node_name: Document.Node.Name,
     2.9    changed: Boolean = true,
    2.10    published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    2.11  {
     3.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:10:09 2016 +0100
     3.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:26:38 2016 +0100
     3.3 @@ -111,7 +111,7 @@
     3.4      for {
     3.5        model <- state.value.models.get(node_pos.name)
     3.6        rendering = model.rendering(options)
     3.7 -      offset <- model.doc.offset(node_pos.pos, text_length)
     3.8 +      offset <- model.doc.offset(node_pos.pos)
     3.9      } yield (rendering, offset)
    3.10  
    3.11  
    3.12 @@ -134,7 +134,7 @@
    3.13      state.change(st =>
    3.14        {
    3.15          val node_name = resources.node_name(uri)
    3.16 -        val model = Document_Model(session, Line.Document(text), node_name, text_length)
    3.17 +        val model = Document_Model(session, Line.Document(text, text_length), node_name)
    3.18          st.copy(models = st.models + (uri -> model))
    3.19        })
    3.20      delay_input.invoke()
    3.21 @@ -265,7 +265,7 @@
    3.22          info <- rendering.tooltip(Text.Range(offset, offset + 1))
    3.23        } yield {
    3.24          val doc = rendering.model.doc
    3.25 -        val range = doc.range(info.range, text_length)
    3.26 +        val range = doc.range(info.range)
    3.27          val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
    3.28          (range, List("```\n" + s + "\n```"))  // FIXME proper content format
    3.29        }
     4.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 17:10:09 2016 +0100
     4.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 28 17:26:38 2016 +0100
     4.3 @@ -59,7 +59,7 @@
     4.4    {
     4.5      (for {
     4.6        Text.Info(text_range, res) <- results.iterator
     4.7 -      range = model.doc.range(text_range, model.text_length)
     4.8 +      range = model.doc.range(text_range)
     4.9        (_, XML.Elem(Markup(name, _), body)) <- res.iterator
    4.10      } yield {
    4.11        val message = Pretty.string_of(body, margin = diagnostics_margin)
    4.12 @@ -89,10 +89,8 @@
    4.13          opt_text match {
    4.14            case Some(text) if range.start > 0 =>
    4.15              val chunk = Symbol.Text_Chunk(text)
    4.16 -            val doc = Line.Document(text)
    4.17 -            def position(offset: Symbol.Offset) =
    4.18 -              doc.position(chunk.decode(offset), model.text_length)
    4.19 -            Line.Range(position(range.start), position(range.stop))
    4.20 +            val doc = Line.Document(text, model.doc.text_length)
    4.21 +            doc.range(chunk.decode(range))
    4.22            case _ =>
    4.23              Line.Range(Line.Position((line1 - 1) max 0))
    4.24          })