src/Pure/PIDE/line.scala
changeset 64672 d8e0619abb60
parent 64666 f6c6e25ef782
child 64679 b2bf280b7e13
equal deleted inserted replaced
64671:93e375bd3283 64672:d8e0619abb60
    78 
    78 
    79   /* document with newline as separator (not terminator) */
    79   /* document with newline as separator (not terminator) */
    80 
    80 
    81   object Document
    81   object Document
    82   {
    82   {
    83     val empty: Document = new Document("", Nil)
    83     val empty: Document = new Document(Nil)
    84 
    84 
    85     def apply(lines: List[Line]): Document =
    85     def apply(lines: List[Line]): Document =
    86       if (lines.isEmpty) empty
    86       if (lines.isEmpty) empty
    87       else new Document(lines.mkString("", "\n", ""), lines)
    87       else new Document(lines)
    88 
    88 
    89     def apply(text: String): Document =
    89     def apply(text: String): Document =
    90       if (text.contains('\r'))
    90       if (text == "") empty
    91         apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
    91       else if (text.contains('\r'))
    92       else if (text == "") Document.empty
    92         new Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))))
    93       else new Document(text, Library.split_lines(text).map(Line(_)))
    93       else
       
    94         new Document(Library.split_lines(text).map(s => Line(s)))
    94   }
    95   }
    95 
    96 
    96   final class Document private(val text: String, val lines: List[Line])
    97   final class Document private(val lines: List[Line])
    97   {
    98   {
    98     override def toString: String = text
    99     def make_text: String = lines.mkString("", "\n", "")
       
   100 
       
   101     override def toString: String = make_text
    99 
   102 
   100     override def equals(that: Any): Boolean =
   103     override def equals(that: Any): Boolean =
   101       that match {
   104       that match {
   102         case other: Document => lines == other.lines
   105         case other: Document => lines == other.lines
   103         case _ => false
   106         case _ => false