simplified Text.Chunk -- eliminated ooddities;
authorwenzelm
Tue Apr 08 20:03:00 2014 +0200 (2014-04-08)
changeset 564735b5c750e9763
parent 56472 f4abde849190
child 56474 4df2727a0b5f
simplified Text.Chunk -- eliminated ooddities;
afford strict symbol_index, which is usually empty anyway;
src/Pure/General/position.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/text.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/General/position.scala	Tue Apr 08 20:00:53 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Tue Apr 08 20:03:00 2014 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4          case (Id(id), Range(range)) =>
     1.5            val chunk_name =
     1.6              pos match {
     1.7 -              case File(name) => Text.Chunk.File_Name(name)
     1.8 +              case File(name) => Text.Chunk.File(name)
     1.9                case _ => Text.Chunk.Default
    1.10              }
    1.11            Some((id, chunk_name, range))
     2.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 08 20:00:53 2014 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 08 20:03:00 2014 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  object Command
     2.5  {
     2.6    type Edit = (Option[Command], Option[Command])
     2.7 -  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk.File)])]
     2.8 +  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
     2.9  
    2.10  
    2.11  
    2.12 @@ -355,25 +355,21 @@
    2.13  
    2.14    /* source chunks */
    2.15  
    2.16 +  val chunk: Text.Chunk = Text.Chunk(source)
    2.17 +
    2.18 +  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
    2.19 +    ((Text.Chunk.Default -> chunk) ::
    2.20 +      (for (Exn.Res((name, Some((_, file)))) <- blobs)
    2.21 +        yield (Text.Chunk.File(name.node) -> file))).toMap
    2.22 +
    2.23    def length: Int = source.length
    2.24 -  val range: Text.Range = Text.Range(0, length)
    2.25 +  def range: Text.Range = chunk.range
    2.26  
    2.27    val proper_range: Text.Range =
    2.28      Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
    2.29  
    2.30    def source(range: Text.Range): String = source.substring(range.start, range.stop)
    2.31  
    2.32 -  val chunk: Text.Chunk =
    2.33 -    new Text.Chunk {
    2.34 -      def range: Text.Range = Command.this.range
    2.35 -      lazy val symbol_index = Symbol.Index(source)
    2.36 -    }
    2.37 -
    2.38 -  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
    2.39 -    ((Text.Chunk.Default -> chunk) ::
    2.40 -      (for (Exn.Res((name, Some((_, file)))) <- blobs)
    2.41 -        yield (Text.Chunk.File_Name(name.node) -> file))).toMap
    2.42 -
    2.43  
    2.44    /* accumulated results */
    2.45  
     3.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 08 20:00:53 2014 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 08 20:03:00 2014 +0200
     3.3 @@ -45,7 +45,7 @@
     3.4  
     3.5    /* document blobs: auxiliary files */
     3.6  
     3.7 -  sealed case class Blob(bytes: Bytes, file: Text.Chunk.File, changed: Boolean)
     3.8 +  sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
     3.9    {
    3.10      def unchanged: Blob = copy(changed = false)
    3.11    }
    3.12 @@ -774,7 +774,7 @@
    3.13            val former_range = revert(range)
    3.14            val (chunk_name, command_iterator) =
    3.15              load_commands match {
    3.16 -              case command :: _ => (Text.Chunk.File_Name(node_name.node), Iterator((command, 0)))
    3.17 +              case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
    3.18                case _ => (Text.Chunk.Default, node.command_iterator(former_range))
    3.19              }
    3.20            val markup_index = Command.Markup_Index(status, chunk_name)
     4.1 --- a/src/Pure/PIDE/text.scala	Tue Apr 08 20:00:53 2014 +0200
     4.2 +++ b/src/Pure/PIDE/text.scala	Tue Apr 08 20:03:00 2014 +0200
     4.3 @@ -71,19 +71,25 @@
     4.4    }
     4.5  
     4.6  
     4.7 -  /* chunks with symbol index */
     4.8 +  /* named chunks with sparse symbol index */
     4.9  
    4.10 -  abstract class Chunk
    4.11 +  object Chunk
    4.12    {
    4.13 -    def range: Range
    4.14 -    def symbol_index: Symbol.Index
    4.15 +    sealed abstract class Name
    4.16 +    case object Default extends Name
    4.17 +    case class Id(id: Document_ID.Generic) extends Name
    4.18 +    case class File(name: String) extends Name
    4.19  
    4.20 -    private lazy val hash: Int = (range, symbol_index).hashCode
    4.21 -    override def hashCode: Int = hash
    4.22 +    def apply(text: CharSequence): Chunk =
    4.23 +      new Chunk(Range(0, text.length), Symbol.Index(text))
    4.24 +  }
    4.25 +
    4.26 +  final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
    4.27 +  {
    4.28 +    override def hashCode: Int = (range, symbol_index).hashCode
    4.29      override def equals(that: Any): Boolean =
    4.30        that match {
    4.31          case other: Chunk =>
    4.32 -          hash == other.hash &&
    4.33            range == other.range &&
    4.34            symbol_index == other.symbol_index
    4.35          case _ => false
    4.36 @@ -102,20 +108,6 @@
    4.37      }
    4.38    }
    4.39  
    4.40 -  object Chunk
    4.41 -  {
    4.42 -    sealed abstract class Name
    4.43 -    case object Default extends Name
    4.44 -    case class Id(id: Document_ID.Generic) extends Name
    4.45 -    case class File_Name(file_name: String) extends Name
    4.46 -
    4.47 -    class File(text: CharSequence) extends Chunk
    4.48 -    {
    4.49 -      val range = Range(0, text.length)
    4.50 -      val symbol_index = Symbol.Index(text)
    4.51 -    }
    4.52 -  }
    4.53 -
    4.54  
    4.55    /* perspective */
    4.56  
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Apr 08 20:00:53 2014 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Apr 08 20:03:00 2014 +0200
     5.3 @@ -271,7 +271,7 @@
     5.4        Exn.capture {
     5.5          val name =
     5.6            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
     5.7 -        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
     5.8 +        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
     5.9          (name, blob)
    5.10        })
    5.11    }
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 20:00:53 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 20:03:00 2014 +0200
     6.3 @@ -138,7 +138,7 @@
     6.4  
     6.5    /* blob */
     6.6  
     6.7 -  private var _blob: Option[(Bytes, Text.Chunk.File)] = None  // owned by Swing thread
     6.8 +  private var _blob: Option[(Bytes, Text.Chunk)] = None  // owned by Swing thread
     6.9  
    6.10    private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
    6.11  
    6.12 @@ -146,17 +146,17 @@
    6.13      Swing_Thread.require {
    6.14        if (is_theory) None
    6.15        else {
    6.16 -        val (bytes, file) =
    6.17 +        val (bytes, chunk) =
    6.18            _blob match {
    6.19              case Some(x) => x
    6.20              case None =>
    6.21                val bytes = PIDE.resources.file_content(buffer)
    6.22 -              val file = new Text.Chunk.File(buffer.getSegment(0, buffer.getLength))
    6.23 -              _blob = Some((bytes, file))
    6.24 -              (bytes, file)
    6.25 +              val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
    6.26 +              _blob = Some((bytes, chunk))
    6.27 +              (bytes, chunk)
    6.28            }
    6.29          val changed = pending_edits.is_pending()
    6.30 -        Some(Document.Blob(bytes, file, changed))
    6.31 +        Some(Document.Blob(bytes, chunk, changed))
    6.32        }
    6.33      }
    6.34