clarified modules;
authorwenzelm
Tue Dec 20 08:57:03 2016 +0100 (2016-12-20)
changeset 64611d72d63d05bdb
parent 64610 1b89608974e9
child 64612 08e4b1aeac50
clarified modules;
src/Pure/PIDE/line.scala
src/Pure/build-jars
src/Tools/VSCode/src/line.scala
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/line.scala	Tue Dec 20 08:57:03 2016 +0100
     1.3 @@ -0,0 +1,149 @@
     1.4 +/*  Title:      Pure/PIDE/line.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Line-oriented text.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import scala.annotation.tailrec
    1.14 +
    1.15 +
    1.16 +object Line
    1.17 +{
    1.18 +  /* position */
    1.19 +
    1.20 +  object Position
    1.21 +  {
    1.22 +    val zero: Position = Position(0, 0)
    1.23 +  }
    1.24 +
    1.25 +  sealed case class Position(line: Int, column: Int)
    1.26 +  {
    1.27 +    def line1: Int = line + 1
    1.28 +    def column1: Int = column + 1
    1.29 +    def print: String = line1.toString + ":" + column1.toString
    1.30 +
    1.31 +    def compare(that: Position): Int =
    1.32 +      line compare that.line match {
    1.33 +        case 0 => column compare that.column
    1.34 +        case i => i
    1.35 +      }
    1.36 +
    1.37 +    private def advance[A](iterator: Iterator[A], is_newline: A => Boolean): Position =
    1.38 +    {
    1.39 +      var l = line
    1.40 +      var c = column
    1.41 +      for (x <- iterator) {
    1.42 +        if (is_newline(x)) { l += 1; c = 0 } else c += 1
    1.43 +      }
    1.44 +      Position(l, c)
    1.45 +    }
    1.46 +
    1.47 +    def advance(text: String): Position =
    1.48 +      if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
    1.49 +
    1.50 +    def advance_symbols(text: String): Position =
    1.51 +      if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
    1.52 +
    1.53 +    def advance_codepoints(text: String): Position =
    1.54 +      if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
    1.55 +  }
    1.56 +
    1.57 +
    1.58 +  /* range (right-open interval) */
    1.59 +
    1.60 +  sealed case class Range(start: Position, stop: Position)
    1.61 +  {
    1.62 +    if (start.compare(stop) > 0)
    1.63 +      error("Bad line range: " + start.print + ".." + stop.print)
    1.64 +
    1.65 +    def print: String = start.print + ".." + stop.print
    1.66 +  }
    1.67 +
    1.68 +
    1.69 +  /* document with newline as separator (not terminator) */
    1.70 +
    1.71 +  object Document
    1.72 +  {
    1.73 +    val empty: Document = new Document("", Nil)
    1.74 +
    1.75 +    def apply(lines: List[Line]): Document =
    1.76 +      if (lines.isEmpty) empty
    1.77 +      else new Document(lines.mkString("", "\n", ""), lines)
    1.78 +
    1.79 +    def apply(text: String): Document =
    1.80 +      if (text.contains('\r'))
    1.81 +        apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
    1.82 +      else if (text == "") Document.empty
    1.83 +      else new Document(text, Library.split_lines(text).map(Line(_)))
    1.84 +  }
    1.85 +
    1.86 +  final class Document private(val text: String, val lines: List[Line])
    1.87 +  {
    1.88 +    override def toString: String = text
    1.89 +
    1.90 +    override def equals(that: Any): Boolean =
    1.91 +      that match {
    1.92 +        case other: Document => lines == other.lines
    1.93 +        case _ => false
    1.94 +      }
    1.95 +    override def hashCode(): Int = lines.hashCode
    1.96 +
    1.97 +    private def position(advance: (Position, String) => Position, offset: Text.Offset): Position =
    1.98 +    {
    1.99 +      @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
   1.100 +      {
   1.101 +        lines_rest match {
   1.102 +          case Nil => require(i == 0); Position(lines_count, 0)
   1.103 +          case line :: ls =>
   1.104 +            val n = line.text.length
   1.105 +            if (ls.isEmpty || i <= n) advance(Position(lines_count, 0), line.text.substring(n - i))
   1.106 +            else move(i - (n + 1), lines_count + 1, ls)
   1.107 +        }
   1.108 +      }
   1.109 +      move(offset, 0, lines)
   1.110 +    }
   1.111 +
   1.112 +    def position(i: Text.Offset): Position = position(_.advance(_), i)
   1.113 +    def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i)
   1.114 +    def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
   1.115 +
   1.116 +    // FIXME symbols, codepoints
   1.117 +    def offset(pos: Position): Option[Text.Offset] =
   1.118 +    {
   1.119 +      val l = pos.line
   1.120 +      val c = pos.column
   1.121 +      if (0 <= l && l < lines.length) {
   1.122 +        val line_offset =
   1.123 +          if (l == 0) 0
   1.124 +          else (0 /: lines.take(l - 1))({ case (n, line) => n + line.text.length + 1 })
   1.125 +        if (c <= lines(l).text.length) Some(line_offset + c) else None
   1.126 +      }
   1.127 +      else None
   1.128 +    }
   1.129 +  }
   1.130 +
   1.131 +
   1.132 +  /* line text */
   1.133 +
   1.134 +  val empty: Line = new Line("")
   1.135 +  def apply(text: String): Line = if (text == "") empty else new Line(text)
   1.136 +}
   1.137 +
   1.138 +final class Line private(val text: String)
   1.139 +{
   1.140 +  require(text.forall(c => c != '\r' && c != '\n'))
   1.141 +
   1.142 +  lazy val length_symbols: Int = Symbol.iterator(text).length
   1.143 +  lazy val length_codepoints: Int = Codepoint.iterator(text).length
   1.144 +
   1.145 +  override def equals(that: Any): Boolean =
   1.146 +    that match {
   1.147 +      case other: Line => text == other.text
   1.148 +      case _ => false
   1.149 +    }
   1.150 +  override def hashCode(): Int = text.hashCode
   1.151 +  override def toString: String = text
   1.152 +}
     2.1 --- a/src/Pure/build-jars	Tue Dec 20 08:53:26 2016 +0100
     2.2 +++ b/src/Pure/build-jars	Tue Dec 20 08:57:03 2016 +0100
     2.3 @@ -86,6 +86,7 @@
     2.4    PIDE/document.scala
     2.5    PIDE/document_id.scala
     2.6    PIDE/editor.scala
     2.7 +  PIDE/line.scala
     2.8    PIDE/markup.scala
     2.9    PIDE/markup_tree.scala
    2.10    PIDE/protocol.scala
    2.11 @@ -157,7 +158,6 @@
    2.12    ../Tools/Graphview/tree_panel.scala
    2.13    ../Tools/VSCode/src/channel.scala
    2.14    ../Tools/VSCode/src/document_model.scala
    2.15 -  ../Tools/VSCode/src/line.scala
    2.16    ../Tools/VSCode/src/protocol.scala
    2.17    ../Tools/VSCode/src/server.scala
    2.18    ../Tools/VSCode/src/uri_resources.scala
     3.1 --- a/src/Tools/VSCode/src/line.scala	Tue Dec 20 08:53:26 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,151 +0,0 @@
     3.4 -/*  Title:      Tools/VSCode/src/line.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Line-oriented text.
     3.8 -*/
     3.9 -
    3.10 -package isabelle.vscode
    3.11 -
    3.12 -
    3.13 -import isabelle._
    3.14 -
    3.15 -import scala.annotation.tailrec
    3.16 -
    3.17 -
    3.18 -object Line
    3.19 -{
    3.20 -  /* position */
    3.21 -
    3.22 -  object Position
    3.23 -  {
    3.24 -    val zero: Position = Position(0, 0)
    3.25 -  }
    3.26 -
    3.27 -  sealed case class Position(line: Int, column: Int)
    3.28 -  {
    3.29 -    def line1: Int = line + 1
    3.30 -    def column1: Int = column + 1
    3.31 -    def print: String = line1.toString + ":" + column1.toString
    3.32 -
    3.33 -    def compare(that: Position): Int =
    3.34 -      line compare that.line match {
    3.35 -        case 0 => column compare that.column
    3.36 -        case i => i
    3.37 -      }
    3.38 -
    3.39 -    private def advance[A](iterator: Iterator[A], is_newline: A => Boolean): Position =
    3.40 -    {
    3.41 -      var l = line
    3.42 -      var c = column
    3.43 -      for (x <- iterator) {
    3.44 -        if (is_newline(x)) { l += 1; c = 0 } else c += 1
    3.45 -      }
    3.46 -      Position(l, c)
    3.47 -    }
    3.48 -
    3.49 -    def advance(text: String): Position =
    3.50 -      if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n')
    3.51 -
    3.52 -    def advance_symbols(text: String): Position =
    3.53 -      if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _)
    3.54 -
    3.55 -    def advance_codepoints(text: String): Position =
    3.56 -      if (text.isEmpty) this else advance[Int](Codepoint.iterator(text), _ == 10)
    3.57 -  }
    3.58 -
    3.59 -
    3.60 -  /* range (right-open interval) */
    3.61 -
    3.62 -  sealed case class Range(start: Position, stop: Position)
    3.63 -  {
    3.64 -    if (start.compare(stop) > 0)
    3.65 -      error("Bad line range: " + start.print + ".." + stop.print)
    3.66 -
    3.67 -    def print: String = start.print + ".." + stop.print
    3.68 -  }
    3.69 -
    3.70 -
    3.71 -  /* document with newline as separator (not terminator) */
    3.72 -
    3.73 -  object Document
    3.74 -  {
    3.75 -    val empty: Document = new Document("", Nil)
    3.76 -
    3.77 -    def apply(lines: List[Line]): Document =
    3.78 -      if (lines.isEmpty) empty
    3.79 -      else new Document(lines.mkString("", "\n", ""), lines)
    3.80 -
    3.81 -    def apply(text: String): Document =
    3.82 -      if (text.contains('\r'))
    3.83 -        apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_))))
    3.84 -      else if (text == "") Document.empty
    3.85 -      else new Document(text, Library.split_lines(text).map(Line(_)))
    3.86 -  }
    3.87 -
    3.88 -  final class Document private(val text: String, val lines: List[Line])
    3.89 -  {
    3.90 -    override def toString: String = text
    3.91 -
    3.92 -    override def equals(that: Any): Boolean =
    3.93 -      that match {
    3.94 -        case other: Document => lines == other.lines
    3.95 -        case _ => false
    3.96 -      }
    3.97 -    override def hashCode(): Int = lines.hashCode
    3.98 -
    3.99 -    private def position(advance: (Position, String) => Position, offset: Text.Offset): Position =
   3.100 -    {
   3.101 -      @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
   3.102 -      {
   3.103 -        lines_rest match {
   3.104 -          case Nil => require(i == 0); Position(lines_count, 0)
   3.105 -          case line :: ls =>
   3.106 -            val n = line.text.length
   3.107 -            if (ls.isEmpty || i <= n) advance(Position(lines_count, 0), line.text.substring(n - i))
   3.108 -            else move(i - (n + 1), lines_count + 1, ls)
   3.109 -        }
   3.110 -      }
   3.111 -      move(offset, 0, lines)
   3.112 -    }
   3.113 -
   3.114 -    def position(i: Text.Offset): Position = position(_.advance(_), i)
   3.115 -    def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i)
   3.116 -    def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i)
   3.117 -
   3.118 -    // FIXME symbols, codepoints
   3.119 -    def offset(pos: Position): Option[Text.Offset] =
   3.120 -    {
   3.121 -      val l = pos.line
   3.122 -      val c = pos.column
   3.123 -      if (0 <= l && l < lines.length) {
   3.124 -        val line_offset =
   3.125 -          if (l == 0) 0
   3.126 -          else (0 /: lines.take(l - 1))({ case (n, line) => n + line.text.length + 1 })
   3.127 -        if (c <= lines(l).text.length) Some(line_offset + c) else None
   3.128 -      }
   3.129 -      else None
   3.130 -    }
   3.131 -  }
   3.132 -
   3.133 -
   3.134 -  /* line text */
   3.135 -
   3.136 -  val empty: Line = new Line("")
   3.137 -  def apply(text: String): Line = if (text == "") empty else new Line(text)
   3.138 -}
   3.139 -
   3.140 -final class Line private(val text: String)
   3.141 -{
   3.142 -  require(text.forall(c => c != '\r' && c != '\n'))
   3.143 -
   3.144 -  lazy val length_symbols: Int = Symbol.iterator(text).length
   3.145 -  lazy val length_codepoints: Int = Codepoint.iterator(text).length
   3.146 -
   3.147 -  override def equals(that: Any): Boolean =
   3.148 -    that match {
   3.149 -      case other: Line => text == other.text
   3.150 -      case _ => false
   3.151 -    }
   3.152 -  override def hashCode(): Int = text.hashCode
   3.153 -  override def toString: String = text
   3.154 -}