# HG changeset patch
# User wenzelm
# Date 1489055664 -3600
# Node ID cd977a5bd9281b2e6b7954b55ca7edaf51e58ef3
# Parent  35fefc2493110f9f910cfd03eaad97aa5679739f
clarified Document.offset: including final position;
support Document.change according to VSCode;

diff -r 35fefc249311 -r cd977a5bd928 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Wed Mar 08 21:41:14 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Thu Mar 09 11:34:24 2017 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/PIDE/line.scala
     Author:     Makarius
 
-Line-oriented text.
+Line-oriented text documents, with some bias towards VSCode.
 */
 
 package isabelle
@@ -91,18 +91,27 @@
   {
     def apply(text: String, text_length: Text.Length): Document =
       Document(logical_lines(text).map(s => Line(Library.trim_substring(s))), text_length)
+
+    def lines(text: String): List[Line] = apply(text, Text.Length).lines
+
+    private def chop(lines: List[Line]): (String, List[Line]) =
+      lines match {
+        case Nil => ("", Nil)
+        case List(line) => (line.text, Nil)
+        case line :: rest => (line.text + "\n", rest)
+      }
+
+    private def length(lines: List[Line]): Int =
+      if (lines.isEmpty) 0
+      else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
+
+    def text(lines: List[Line]): String = lines.mkString("", "\n", "")
   }
 
   sealed case class Document(lines: List[Line], text_length: Text.Length)
   {
-    lazy val text_range: Text.Range =
-    {
-      val length =
-        if (lines.isEmpty) 0
-        else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
-      Text.Range(0, length)
-    }
-    lazy val text: String = lines.mkString("", "\n", "")
+    lazy val text_range: Text.Range = Text.Range(0, Document.length(lines))
+    lazy val text: String = Document.text(lines)
 
     def try_get_text(range: Text.Range): Option[String] =
       if (text_range.contains(range)) Some(text.substring(range.start, range.stop))
@@ -140,13 +149,65 @@
     {
       val l = pos.line
       val c = pos.column
-      if (0 <= l && l < lines.length) {
+      val n = lines.length
+      if (0 <= l && l < n) {
         val line_offset =
-          (0 /: lines.iterator.take(l)) { case (n, line) => n + text_length(line.text) + 1 }
+          (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 }
         text_length.offset(lines(l).text, c).map(line_offset + _)
       }
+      else if (l == n && c == 0) Some(text_range.length)
       else None
     }
+
+    def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] =
+    {
+      for {
+        edit_start <- offset(remove.start)
+        if remove.stop == remove.start || offset(remove.stop).isDefined
+        l1 = remove.start.line
+        l2 = remove.stop.line
+        if l1 <= l2
+        (removed_text, changed_lines) <-
+        {
+          val (prefix, lines1) = lines.splitAt(l1)
+          val (s1, rest1) = Document.chop(lines1)
+
+          if (l1 == l2) {
+            for {
+              c1 <- text_length.offset(s1, remove.start.column)
+              c2 <- text_length.offset(s1, remove.stop.column)
+              if c1 <= c2
+            }
+            yield {
+              val removed_text = s1.substring(c1, c2)
+              val changed_text = s1.substring(0, c1) + insert + Library.trim_line(s1.substring(c2))
+              (removed_text, prefix ::: Document.lines(changed_text) ::: rest1)
+            }
+          }
+          else {
+            val (middle, lines2) = rest1.splitAt(l2 - l1 - 1)
+            val (s2, rest2) = Document.chop(lines2)
+            for {
+              c1 <- text_length.offset(s1, remove.start.column)
+              c2 <- text_length.offset(s2, remove.stop.column)
+            }
+            yield {
+              val r1 = Library.trim_line(s1.substring(c1))
+              val r2 = s2.substring(0, c2)
+              val removed_text =
+                if (lines1.isEmpty) ""
+                else if (lines2.isEmpty) Document.text(Line(r1) :: middle)
+                else Document.text(Line(r1) :: middle ::: List(Line(r2)))
+              val changed_text = s1.substring(0, c1) + insert + Library.trim_line(s2.substring(c2))
+              (removed_text, prefix ::: Document.lines(changed_text) ::: rest2)
+            }
+          }
+        }
+      }
+      yield
+        (Text.Edit.removes(edit_start, removed_text) ::: Text.Edit.inserts(edit_start, insert),
+          Document(changed_lines, text_length))
+    }
   }