# HG changeset patch # User wenzelm # Date 1398512050 -7200 # Node ID d37a5d09a27752d1974b635c524afa60b4107399 # Parent 5e3db9209bcf6b36ce47334604f780d32bc3bf17 tuned signature; diff -r 5e3db9209bcf -r d37a5d09a277 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Sat Apr 26 13:32:28 2014 +0200 +++ b/src/Pure/General/position.scala Sat Apr 26 13:34:10 2014 +0200 @@ -83,13 +83,13 @@ object Reported { - def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] = + def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name, Symbol.Range)] = (pos, pos) match { case (Id(id), Range(range)) => val chunk_name = pos match { - case File(name) => Text.Chunk.File(name) - case _ => Text.Chunk.Default + case File(name) => Symbol.Text_Chunk.File(name) + case _ => Symbol.Text_Chunk.Default } Some((id, chunk_name, range)) case _ => None diff -r 5e3db9209bcf -r d37a5d09a277 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Sat Apr 26 13:32:28 2014 +0200 +++ b/src/Pure/General/symbol.scala Sat Apr 26 13:34:10 2014 +0200 @@ -179,6 +179,44 @@ } + /* text chunks */ + + object Text_Chunk + { + 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 + + def apply(text: CharSequence): Text_Chunk = + new Text_Chunk(Text.Range(0, text.length), Index(text)) + } + + final class Text_Chunk private(val range: Text.Range, private val index: Index) + { + override def hashCode: Int = (range, index).hashCode + override def equals(that: Any): Boolean = + that match { + case other: Text_Chunk => + range == other.range && + index == other.index + case _ => false + } + + def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset) + def decode(symbol_range: Range): Text.Range = index.decode(symbol_range) + def incorporate(symbol_range: Range): Option[Text.Range] = + { + def in(r: 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) + } + } + + /* recoding text */ private class Recoder(list: List[(String, String)]) diff -r 5e3db9209bcf -r d37a5d09a277 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Apr 26 13:32:28 2014 +0200 +++ b/src/Pure/PIDE/command.scala Sat Apr 26 13:34:10 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)])] + type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])] @@ -60,10 +60,10 @@ object Markup_Index { - val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default) + val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) } - sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name) + sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) object Markups { @@ -84,16 +84,16 @@ new Markups(rep + (index -> (this(index) + markup))) def redirection_iterator: Iterator[Document_ID.Generic] = - for (Markup_Index(_, Text.Chunk.Id(id)) <- rep.keysIterator) + for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) yield id def redirect(other_id: Document_ID.Generic): Markups = { val rep1 = (for { - (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator + (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator if other_id == id - } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap + } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap if (rep1.isEmpty) Markups.empty else new Markups(rep1) } @@ -156,7 +156,8 @@ private def add_status(st: Markup): State = copy(status = st :: status) - private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State = + private def add_markup( + status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Protocol.liberal_status_elements(m.info.name)) @@ -167,7 +168,7 @@ def accumulate( self_id: Document_ID.Generic => Boolean, - other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)], + other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], message: XML.Elem): State = message match { case XML.Elem(Markup(Markup.STATUS, _), msgs) => @@ -176,7 +177,7 @@ case elem @ XML.Elem(markup, Nil) => state. add_status(markup). - add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem)) + add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem)) case _ => System.err.println("Ignored status message: " + msg) state @@ -194,7 +195,7 @@ val target = if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) Some((chunk_name, command.chunks(chunk_name))) - else if (chunk_name == Text.Chunk.Default) other_id(id) + else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) else None target match { @@ -216,7 +217,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, Text.Chunk.Default, info) + state.add_markup(false, Symbol.Text_Chunk.Default, info) case _ => bad(); state } @@ -365,12 +366,12 @@ /* source chunks */ - val chunk: Text.Chunk = Text.Chunk(source) + val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) - val chunks: Map[Text.Chunk.Name, Text.Chunk] = - ((Text.Chunk.Default -> chunk) :: + val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = + ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res((name, Some((_, file)))) <- blobs) - yield (Text.Chunk.File(name.node) -> file))).toMap + yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap def length: Int = source.length def range: Text.Range = chunk.range diff -r 5e3db9209bcf -r d37a5d09a277 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Apr 26 13:32:28 2014 +0200 +++ b/src/Pure/PIDE/document.scala Sat Apr 26 13:34:10 2014 +0200 @@ -45,7 +45,7 @@ /* document blobs: auxiliary files */ - sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean) + sealed case class Blob(bytes: Bytes, chunk: Symbol.Text_Chunk, changed: Boolean) { def unchanged: Blob = copy(changed = false) } @@ -511,10 +511,11 @@ id == st.command.id || (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false }) - private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] = None + private def other_id(id: Document_ID.Generic) + : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = None /* FIXME (execs.get(id) orElse commands.get(id)).map(st => - ((Text.Chunk.Id(st.command.id), st.command.chunk))) + ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk))) */ private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] = @@ -751,8 +752,8 @@ val former_range = revert(range).inflate_singularity val (chunk_name, command_iterator) = load_commands match { - case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0))) - case _ => (Text.Chunk.Default, node.command_iterator(former_range)) + case command :: _ => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0))) + case _ => (Symbol.Text_Chunk.Default, node.command_iterator(former_range)) } val markup_index = Command.Markup_Index(status, chunk_name) (for { diff -r 5e3db9209bcf -r d37a5d09a277 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sat Apr 26 13:32:28 2014 +0200 +++ b/src/Pure/PIDE/protocol.scala Sat Apr 26 13:34:10 2014 +0200 @@ -312,8 +312,8 @@ def message_positions( self_id: Document_ID.Generic => Boolean, - chunk_name: Text.Chunk.Name, - chunk: Text.Chunk, + chunk_name: Symbol.Text_Chunk.Name, + chunk: Symbol.Text_Chunk, message: XML.Elem): Set[Text.Range] = { def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = diff -r 5e3db9209bcf -r d37a5d09a277 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Sat Apr 26 13:32:28 2014 +0200 +++ b/src/Pure/PIDE/text.scala Sat Apr 26 13:34:10 2014 +0200 @@ -72,44 +72,6 @@ } - /* named chunks with sparse symbol index */ - - object Chunk - { - 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 - - 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 => - range == other.range && - symbol_index == other.symbol_index - case _ => false - } - - 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) - } - } - - /* perspective */ object Perspective diff -r 5e3db9209bcf -r d37a5d09a277 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sat Apr 26 13:32:28 2014 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Sat Apr 26 13:34:10 2014 +0200 @@ -138,7 +138,7 @@ /* blob */ - private var _blob: Option[(Bytes, Text.Chunk)] = None // owned by Swing thread + private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None // owned by Swing thread private def reset_blob(): Unit = Swing_Thread.require { _blob = None } @@ -151,7 +151,7 @@ case Some(x) => x case None => val bytes = PIDE.resources.file_content(buffer) - val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength)) + val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength)) _blob = Some((bytes, chunk)) (bytes, chunk) }