--- 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
--- 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)])
--- 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
--- 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 {
--- 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] =
--- 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
--- 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)
}