# HG changeset patch # User wenzelm # Date 1396980180 -7200 # Node ID 5b5c750e9763c4feedbe9896be80b4c90c4d09f1 # Parent f4abde849190e074111edc0ac6d6d60b3097a371 simplified Text.Chunk -- eliminated ooddities; afford strict symbol_index, which is usually empty anyway; diff -r f4abde849190 -r 5b5c750e9763 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Tue Apr 08 20:00:53 2014 +0200 +++ b/src/Pure/General/position.scala Tue Apr 08 20:03:00 2014 +0200 @@ -88,7 +88,7 @@ case (Id(id), Range(range)) => val chunk_name = pos match { - case File(name) => Text.Chunk.File_Name(name) + case File(name) => Text.Chunk.File(name) case _ => Text.Chunk.Default } Some((id, chunk_name, range)) diff -r f4abde849190 -r 5b5c750e9763 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Apr 08 20:00:53 2014 +0200 +++ b/src/Pure/PIDE/command.scala Tue Apr 08 20:03:00 2014 +0200 @@ -15,7 +15,7 @@ object Command { type Edit = (Option[Command], Option[Command]) - type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk.File)])] + type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])] @@ -355,25 +355,21 @@ /* source chunks */ + val chunk: Text.Chunk = Text.Chunk(source) + + val chunks: Map[Text.Chunk.Name, Text.Chunk] = + ((Text.Chunk.Default -> chunk) :: + (for (Exn.Res((name, Some((_, file)))) <- blobs) + yield (Text.Chunk.File(name.node) -> file))).toMap + def length: Int = source.length - val range: Text.Range = Text.Range(0, length) + def range: Text.Range = chunk.range val proper_range: Text.Range = Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length)) def source(range: Text.Range): String = source.substring(range.start, range.stop) - val chunk: Text.Chunk = - new Text.Chunk { - def range: Text.Range = Command.this.range - lazy val symbol_index = Symbol.Index(source) - } - - val chunks: Map[Text.Chunk.Name, Text.Chunk] = - ((Text.Chunk.Default -> chunk) :: - (for (Exn.Res((name, Some((_, file)))) <- blobs) - yield (Text.Chunk.File_Name(name.node) -> file))).toMap - /* accumulated results */ diff -r f4abde849190 -r 5b5c750e9763 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Apr 08 20:00:53 2014 +0200 +++ b/src/Pure/PIDE/document.scala Tue Apr 08 20:03:00 2014 +0200 @@ -45,7 +45,7 @@ /* document blobs: auxiliary files */ - sealed case class Blob(bytes: Bytes, file: Text.Chunk.File, changed: Boolean) + sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean) { def unchanged: Blob = copy(changed = false) } @@ -774,7 +774,7 @@ val former_range = revert(range) val (chunk_name, command_iterator) = load_commands match { - case command :: _ => (Text.Chunk.File_Name(node_name.node), Iterator((command, 0))) + case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0))) case _ => (Text.Chunk.Default, node.command_iterator(former_range)) } val markup_index = Command.Markup_Index(status, chunk_name) diff -r f4abde849190 -r 5b5c750e9763 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Tue Apr 08 20:00:53 2014 +0200 +++ b/src/Pure/PIDE/text.scala Tue Apr 08 20:03:00 2014 +0200 @@ -71,19 +71,25 @@ } - /* chunks with symbol index */ + /* named chunks with sparse symbol index */ - abstract class Chunk + object Chunk { - def range: Range - def symbol_index: Symbol.Index + sealed abstract class Name + case object Default extends Name + case class Id(id: Document_ID.Generic) extends Name + case class File(name: String) extends Name - private lazy val hash: Int = (range, symbol_index).hashCode - override def hashCode: Int = hash + def apply(text: CharSequence): Chunk = + new Chunk(Range(0, text.length), Symbol.Index(text)) + } + + final class Chunk private(val range: Range, private val symbol_index: Symbol.Index) + { + override def hashCode: Int = (range, symbol_index).hashCode override def equals(that: Any): Boolean = that match { case other: Chunk => - hash == other.hash && range == other.range && symbol_index == other.symbol_index case _ => false @@ -102,20 +108,6 @@ } } - object Chunk - { - sealed abstract class Name - case object Default extends Name - case class Id(id: Document_ID.Generic) extends Name - case class File_Name(file_name: String) extends Name - - class File(text: CharSequence) extends Chunk - { - val range = Range(0, text.length) - val symbol_index = Symbol.Index(text) - } - } - /* perspective */ diff -r f4abde849190 -r 5b5c750e9763 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Tue Apr 08 20:00:53 2014 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Tue Apr 08 20:03:00 2014 +0200 @@ -271,7 +271,7 @@ Exn.capture { val name = Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name))) - val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.file))) + val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk))) (name, blob) }) } diff -r f4abde849190 -r 5b5c750e9763 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Apr 08 20:00:53 2014 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Tue Apr 08 20:03:00 2014 +0200 @@ -138,7 +138,7 @@ /* blob */ - private var _blob: Option[(Bytes, Text.Chunk.File)] = None // owned by Swing thread + private var _blob: Option[(Bytes, Text.Chunk)] = None // owned by Swing thread private def reset_blob(): Unit = Swing_Thread.require { _blob = None } @@ -146,17 +146,17 @@ Swing_Thread.require { if (is_theory) None else { - val (bytes, file) = + val (bytes, chunk) = _blob match { case Some(x) => x case None => val bytes = PIDE.resources.file_content(buffer) - val file = new Text.Chunk.File(buffer.getSegment(0, buffer.getLength)) - _blob = Some((bytes, file)) - (bytes, file) + val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength)) + _blob = Some((bytes, chunk)) + (bytes, chunk) } val changed = pending_edits.is_pending() - Some(Document.Blob(bytes, file, changed)) + Some(Document.Blob(bytes, chunk, changed)) } }