# HG changeset patch # User wenzelm # Date 1396962774 -7200 # Node ID 30128d1acfbc2be2818db05054b76836e4661eff # Parent 8d7d6f17c6a78fc950a1dbc31100074143836ade tuned signature -- moved Command.Chunk to Text.Chunk; diff -r 8d7d6f17c6a7 -r 30128d1acfbc src/Pure/General/position.scala --- a/src/Pure/General/position.scala Tue Apr 08 14:59:36 2014 +0200 +++ b/src/Pure/General/position.scala Tue Apr 08 15:12:54 2014 +0200 @@ -83,13 +83,13 @@ object Reported { - def unapply(pos: T): Option[(Long, Command.Chunk.Name, Symbol.Range)] = + def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] = (pos, pos) match { case (Id(id), Range(range)) => val chunk_name = pos match { - case File(name) => Command.Chunk.File_Name(name) - case _ => Command.Chunk.Self + case File(name) => Text.Chunk.File_Name(name) + case _ => Text.Chunk.Default } Some((id, chunk_name, range)) case _ => None diff -r 8d7d6f17c6a7 -r 30128d1acfbc src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Apr 08 14:59:36 2014 +0200 +++ b/src/Pure/PIDE/command.scala Tue Apr 08 15:12:54 2014 +0200 @@ -15,7 +15,7 @@ object Command { type Edit = (Option[Command], Option[Command]) - type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Chunk.File)])] + type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk.File)])] @@ -56,63 +56,14 @@ } - /* source chunks */ - - abstract class Chunk - { - def name: Chunk.Name - def range: Text.Range - def symbol_index: Symbol.Index - - private lazy val hash: Int = (name, range, symbol_index).hashCode - override def hashCode: Int = hash - override def equals(that: Any): Boolean = - that match { - case other: Chunk => - hash == other.hash && - name == other.name && - range == other.range && - symbol_index == other.symbol_index - case _ => false - } - override def toString: String = "Command.Chunk(" + name + ")" - - def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset) - def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range) - def incorporate(symbol_range: Symbol.Range): Option[Text.Range] = - { - def in(r: Symbol.Range): Option[Text.Range] = - range.try_restrict(decode(r)) match { - case Some(r1) if !r1.is_singularity => Some(r1) - case _ => None - } - in(symbol_range) orElse in(symbol_range - 1) - } - } - - object Chunk - { - sealed abstract class Name - case object Self extends Name - case class File_Name(file_name: String) extends Name - - class File(file_name: String, text: CharSequence) extends Chunk - { - val name = Chunk.File_Name(file_name) - val range = Text.Range(0, text.length) - val symbol_index = Symbol.Index(text) - } - } - - /* markup */ object Markup_Index { - val markup: Markup_Index = Markup_Index(false, Chunk.Self) + val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default) } - sealed case class Markup_Index(status: Boolean, chunk_name: Chunk.Name) + sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name) object Markups { @@ -183,7 +134,7 @@ private def add_status(st: Markup): State = copy(status = st :: status) - private def add_markup(status: Boolean, chunk_name: Command.Chunk.Name, m: Text.Markup): State = + private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Protocol.liberal_status_elements(m.info.name)) @@ -200,7 +151,7 @@ case elem @ XML.Elem(markup, Nil) => state. add_status(markup). - add_markup(true, Command.Chunk.Self, Text.Info(command.proper_range, elem)) + add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem)) case _ => System.err.println("Ignored status message: " + msg) state @@ -232,7 +183,7 @@ val range = command.proper_range val props = Position.purge(atts) val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) - state.add_markup(false, Command.Chunk.Self, info) + state.add_markup(false, Text.Chunk.Default, info) case _ => /* FIXME bad(); */ state } @@ -389,17 +340,17 @@ def source(range: Text.Range): String = source.substring(range.start, range.stop) - val chunk: Command.Chunk = - new Command.Chunk { - def name: Command.Chunk.Name = Command.Chunk.Self + val chunk: Text.Chunk = + new Text.Chunk { + def name: Text.Chunk.Name = Text.Chunk.Default def range: Text.Range = Command.this.range lazy val symbol_index = Symbol.Index(source) } - val chunks: Map[Command.Chunk.Name, Command.Chunk] = - ((Command.Chunk.Self -> chunk) :: + val chunks: Map[Text.Chunk.Name, Text.Chunk] = + ((Text.Chunk.Default -> chunk) :: (for (Exn.Res((name, Some((_, file)))) <- blobs) - yield (Command.Chunk.File_Name(name.node) -> file))).toMap + yield (Text.Chunk.File_Name(name.node) -> file))).toMap /* accumulated results */ diff -r 8d7d6f17c6a7 -r 30128d1acfbc src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Apr 08 14:59:36 2014 +0200 +++ b/src/Pure/PIDE/document.scala Tue Apr 08 15:12:54 2014 +0200 @@ -45,7 +45,7 @@ /* document blobs: auxiliary files */ - sealed case class Blob(bytes: Bytes, file: Command.Chunk.File, changed: Boolean) + sealed case class Blob(bytes: Bytes, file: Text.Chunk.File, changed: Boolean) { def unchanged: Blob = copy(changed = false) } @@ -733,8 +733,8 @@ val former_range = revert(range) val (chunk_name, command_iterator) = load_commands match { - case command :: _ => (Command.Chunk.File_Name(node_name.node), Iterator((command, 0))) - case _ => (Command.Chunk.Self, node.command_iterator(former_range)) + case command :: _ => (Text.Chunk.File_Name(node_name.node), Iterator((command, 0))) + case _ => (Text.Chunk.Default, node.command_iterator(former_range)) } val markup_index = Command.Markup_Index(status, chunk_name) (for { diff -r 8d7d6f17c6a7 -r 30128d1acfbc src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Apr 08 14:59:36 2014 +0200 +++ b/src/Pure/PIDE/protocol.scala Tue Apr 08 15:12:54 2014 +0200 @@ -302,7 +302,7 @@ def message_positions( valid_id: Document_ID.Generic => Boolean, - chunk: Command.Chunk, + chunk: Text.Chunk, message: XML.Elem): Set[Text.Range] = { def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = diff -r 8d7d6f17c6a7 -r 30128d1acfbc src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Tue Apr 08 14:59:36 2014 +0200 +++ b/src/Pure/PIDE/text.scala Tue Apr 08 15:12:54 2014 +0200 @@ -71,6 +71,55 @@ } + /* named chunks */ + + abstract class Chunk + { + def name: Chunk.Name + def range: Range + def symbol_index: Symbol.Index + + private lazy val hash: Int = (name, range, symbol_index).hashCode + override def hashCode: Int = hash + override def equals(that: Any): Boolean = + that match { + case other: Chunk => + hash == other.hash && + name == other.name && + range == other.range && + symbol_index == other.symbol_index + case _ => false + } + override def toString: String = "Text.Chunk(" + name + ")" + + def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset) + def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range) + def incorporate(symbol_range: Symbol.Range): Option[Range] = + { + def in(r: Symbol.Range): Option[Range] = + range.try_restrict(decode(r)) match { + case Some(r1) if !r1.is_singularity => Some(r1) + case _ => None + } + in(symbol_range) orElse in(symbol_range - 1) + } + } + + object Chunk + { + sealed abstract class Name + case object Default extends Name + case class File_Name(file_name: String) extends Name + + class File(file_name: String, text: CharSequence) extends Chunk + { + val name = File_Name(file_name) + val range = Range(0, text.length) + val symbol_index = Symbol.Index(text) + } + } + + /* perspective */ object Perspective diff -r 8d7d6f17c6a7 -r 30128d1acfbc src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Apr 08 14:59:36 2014 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Tue Apr 08 15:12:54 2014 +0200 @@ -138,7 +138,7 @@ /* blob */ - private var _blob: Option[(Bytes, Command.Chunk.File)] = None // owned by Swing thread + private var _blob: Option[(Bytes, Text.Chunk.File)] = None // owned by Swing thread private def reset_blob(): Unit = Swing_Thread.require { _blob = None } @@ -151,8 +151,7 @@ case Some(x) => x case None => val bytes = PIDE.resources.file_content(buffer) - val file = - new Command.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength)) + val file = new Text.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength)) _blob = Some((bytes, file)) (bytes, file) }