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