src/Pure/PIDE/line.scala
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 65203 314246c6eeaa
child 65234 1d6e9048cb62
permissions -rw-r--r--
clarified modules;
     1 /*  Title:      Pure/PIDE/line.scala
     2     Author:     Makarius
     3 
     4 Line-oriented text documents, with some bias towards VSCode.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.annotation.tailrec
    11 
    12 
    13 object Line
    14 {
    15   /* logical lines */
    16 
    17   def normalize(text: String): String =
    18     if (text.contains('\r')) text.replace("\r\n", "\n") else text
    19 
    20   def logical_lines(text: String): List[String] =
    21     Library.split_lines(normalize(text))
    22 
    23 
    24   /* position */
    25 
    26   object Position
    27   {
    28     val zero: Position = Position()
    29   }
    30 
    31   sealed case class Position(line: Int = 0, column: Int = 0)
    32   {
    33     def line1: Int = line + 1
    34     def column1: Int = column + 1
    35     def print: String = line1.toString + ":" + column1.toString
    36 
    37     def compare(that: Position): Int =
    38       line compare that.line match {
    39         case 0 => column compare that.column
    40         case i => i
    41       }
    42 
    43     def advance(text: String): Position =
    44       if (text.isEmpty) this
    45       else {
    46         val lines = logical_lines(text)
    47         val l = line + lines.length - 1
    48         val c = (if (l == line) column else 0) + Library.trim_line(lines.last).length
    49         Position(l, c)
    50       }
    51   }
    52 
    53 
    54   /* range (right-open interval) */
    55 
    56   object Range
    57   {
    58     def apply(start: Position): Range = Range(start, start)
    59     val zero: Range = Range(Position.zero)
    60   }
    61 
    62   sealed case class Range(start: Position, stop: Position)
    63   {
    64     if (start.compare(stop) > 0)
    65       error("Bad line range: " + start.print + ".." + stop.print)
    66 
    67     def print: String =
    68       if (start == stop) start.print
    69       else start.print + ".." + stop.print
    70   }
    71 
    72 
    73   /* positions within document node */
    74 
    75   sealed case class Node_Position(name: String, pos: Position = Position.zero)
    76   {
    77     def line: Int = pos.line
    78     def column: Int = pos.column
    79   }
    80 
    81   sealed case class Node_Range(name: String, range: Range = Range.zero)
    82   {
    83     def start: Position = range.start
    84     def stop: Position = range.stop
    85   }
    86 
    87 
    88   /* document with newline as separator (not terminator) */
    89 
    90   object Document
    91   {
    92     def apply(text: String): Document =
    93       Document(logical_lines(text).map(s => Line(Library.trim_substring(s))))
    94 
    95     val empty: Document = apply("")
    96 
    97     private def split(line_text: String): List[Line] =
    98       if (line_text == "") List(Line.empty) else apply(line_text).lines
    99 
   100     private def chop(lines: List[Line]): (String, List[Line]) =
   101       lines match {
   102         case Nil => ("", Nil)
   103         case line :: rest => (line.text, rest)
   104       }
   105 
   106     private def length(lines: List[Line]): Int =
   107       if (lines.isEmpty) 0
   108       else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
   109 
   110     def text(lines: List[Line]): String = lines.mkString("", "\n", "")
   111   }
   112 
   113   sealed case class Document(lines: List[Line])
   114   {
   115     lazy val text_length: Text.Offset = Document.length(lines)
   116     def text_range: Text.Range = Text.Range(0, text_length)
   117 
   118     lazy val text: String = Document.text(lines)
   119 
   120     def try_get_text(range: Text.Range): Option[String] =
   121       if (text_range.contains(range)) Some(text.substring(range.start, range.stop))
   122       else None
   123 
   124     override def toString: String = text
   125 
   126     override def equals(that: Any): Boolean =
   127       that match {
   128         case other: Document => lines == other.lines
   129         case _ => false
   130       }
   131     override def hashCode(): Int = lines.hashCode
   132 
   133     def position(text_offset: Text.Offset): Position =
   134     {
   135       @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
   136       {
   137         lines_rest match {
   138           case Nil => require(i == 0); Position(lines_count)
   139           case line :: ls =>
   140             val n = line.text.length
   141             if (ls.isEmpty || i <= n)
   142               Position(lines_count).advance(line.text.substring(n - i))
   143             else move(i - (n + 1), lines_count + 1, ls)
   144         }
   145       }
   146       move(text_offset, 0, lines)
   147     }
   148 
   149     def range(text_range: Text.Range): Range =
   150       Range(position(text_range.start), position(text_range.stop))
   151 
   152     def offset(pos: Position): Option[Text.Offset] =
   153     {
   154       val l = pos.line
   155       val c = pos.column
   156       val n = lines.length
   157       if (0 <= l && l < n) {
   158         if (0 <= c && c <= lines(l).text.length) {
   159           val line_offset =
   160             (0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 }
   161           Some(line_offset + c)
   162         }
   163         else None
   164       }
   165       else if (l == n && c == 0) Some(text_length)
   166       else None
   167     }
   168 
   169     def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] =
   170     {
   171       for {
   172         edit_start <- offset(remove.start)
   173         if remove.stop == remove.start || offset(remove.stop).isDefined
   174         l1 = remove.start.line
   175         l2 = remove.stop.line
   176         if l1 <= l2
   177         (removed_text, new_lines) <-
   178         {
   179           val c1 = remove.start.column
   180           val c2 = remove.stop.column
   181 
   182           val (prefix, lines1) = lines.splitAt(l1)
   183           val (s1, rest1) = Document.chop(lines1)
   184 
   185           if (l1 == l2) {
   186             if (0 <= c1 && c1 <= c2 && c2 <= s1.length) {
   187               Some(
   188                 if (lines1.isEmpty) ("", prefix ::: Document.split(insert))
   189                 else {
   190                   val removed_text = s1.substring(c1, c2)
   191                   val changed_text = s1.substring(0, c1) + insert + s1.substring(c2)
   192                   (removed_text, prefix ::: Document.split(changed_text) ::: rest1)
   193                 })
   194             }
   195             else None
   196           }
   197           else {
   198             val (middle, lines2) = rest1.splitAt(l2 - l1 - 1)
   199             val (s2, rest2) = Document.chop(lines2)
   200             if (0 <= c1 && c1 <= s1.length && 0 <= c2 && c2 <= s2.length) {
   201               Some(
   202                 if (lines1.isEmpty) ("", prefix ::: Document.split(insert))
   203                 else {
   204                   val r1 = s1.substring(c1)
   205                   val r2 = s2.substring(0, c2)
   206                   val removed_text =
   207                     if (lines2.isEmpty) Document.text(Line(r1) :: middle)
   208                     else Document.text(Line(r1) :: middle ::: List(Line(r2)))
   209                   val changed_text = s1.substring(0, c1) + insert + s2.substring(c2)
   210                   (removed_text, prefix ::: Document.split(changed_text) ::: rest2)
   211                 })
   212             }
   213             else None
   214           }
   215         }
   216       }
   217       yield
   218         (Text.Edit.removes(edit_start, removed_text) ::: Text.Edit.inserts(edit_start, insert),
   219           Document(new_lines))
   220     }
   221   }
   222 
   223 
   224   /* line text */
   225 
   226   val empty: Line = new Line("")
   227   def apply(text: String): Line = if (text == "") empty else new Line(text)
   228 }
   229 
   230 final class Line private(val text: String)
   231 {
   232   require(text.forall(c => c != '\r' && c != '\n'))
   233 
   234   override def equals(that: Any): Boolean =
   235     that match {
   236       case other: Line => text == other.text
   237       case _ => false
   238     }
   239   override def hashCode(): Int = text.hashCode
   240   override def toString: String = text
   241 }