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