tuned signature;
authorwenzelm
Sat Apr 26 13:34:10 2014 +0200 (2014-04-26 ago)
changeset 56746d37a5d09a277
parent 56745 5e3db9209bcf
child 56747 f87e3be0de9a
tuned signature;
src/Pure/General/position.scala
src/Pure/General/symbol.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/General/position.scala	Sat Apr 26 13:32:28 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Sat Apr 26 13:34:10 2014 +0200
     1.3 @@ -83,13 +83,13 @@
     1.4  
     1.5    object Reported
     1.6    {
     1.7 -    def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] =
     1.8 +    def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name, Symbol.Range)] =
     1.9        (pos, pos) match {
    1.10          case (Id(id), Range(range)) =>
    1.11            val chunk_name =
    1.12              pos match {
    1.13 -              case File(name) => Text.Chunk.File(name)
    1.14 -              case _ => Text.Chunk.Default
    1.15 +              case File(name) => Symbol.Text_Chunk.File(name)
    1.16 +              case _ => Symbol.Text_Chunk.Default
    1.17              }
    1.18            Some((id, chunk_name, range))
    1.19          case _ => None
     2.1 --- a/src/Pure/General/symbol.scala	Sat Apr 26 13:32:28 2014 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Sat Apr 26 13:34:10 2014 +0200
     2.3 @@ -179,6 +179,44 @@
     2.4    }
     2.5  
     2.6  
     2.7 +  /* text chunks */
     2.8 +
     2.9 +  object Text_Chunk
    2.10 +  {
    2.11 +    sealed abstract class Name
    2.12 +    case object Default extends Name
    2.13 +    case class Id(id: Document_ID.Generic) extends Name
    2.14 +    case class File(name: String) extends Name
    2.15 +
    2.16 +    def apply(text: CharSequence): Text_Chunk =
    2.17 +      new Text_Chunk(Text.Range(0, text.length), Index(text))
    2.18 +  }
    2.19 +
    2.20 +  final class Text_Chunk private(val range: Text.Range, private val index: Index)
    2.21 +  {
    2.22 +    override def hashCode: Int = (range, index).hashCode
    2.23 +    override def equals(that: Any): Boolean =
    2.24 +      that match {
    2.25 +        case other: Text_Chunk =>
    2.26 +          range == other.range &&
    2.27 +          index == other.index
    2.28 +        case _ => false
    2.29 +      }
    2.30 +
    2.31 +    def decode(symbol_offset: Offset): Text.Offset = index.decode(symbol_offset)
    2.32 +    def decode(symbol_range: Range): Text.Range = index.decode(symbol_range)
    2.33 +    def incorporate(symbol_range: Range): Option[Text.Range] =
    2.34 +    {
    2.35 +      def in(r: Range): Option[Text.Range] =
    2.36 +        range.try_restrict(decode(r)) match {
    2.37 +          case Some(r1) if !r1.is_singularity => Some(r1)
    2.38 +          case _ => None
    2.39 +        }
    2.40 +     in(symbol_range) orElse in(symbol_range - 1)
    2.41 +    }
    2.42 +  }
    2.43 +
    2.44 +
    2.45    /* recoding text */
    2.46  
    2.47    private class Recoder(list: List[(String, String)])
     3.1 --- a/src/Pure/PIDE/command.scala	Sat Apr 26 13:32:28 2014 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Sat Apr 26 13:34:10 2014 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4  object Command
     3.5  {
     3.6    type Edit = (Option[Command], Option[Command])
     3.7 -  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
     3.8 +  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])]
     3.9  
    3.10  
    3.11  
    3.12 @@ -60,10 +60,10 @@
    3.13  
    3.14    object Markup_Index
    3.15    {
    3.16 -    val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default)
    3.17 +    val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
    3.18    }
    3.19  
    3.20 -  sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name)
    3.21 +  sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)
    3.22  
    3.23    object Markups
    3.24    {
    3.25 @@ -84,16 +84,16 @@
    3.26        new Markups(rep + (index -> (this(index) + markup)))
    3.27  
    3.28      def redirection_iterator: Iterator[Document_ID.Generic] =
    3.29 -      for (Markup_Index(_, Text.Chunk.Id(id)) <- rep.keysIterator)
    3.30 +      for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
    3.31          yield id
    3.32  
    3.33      def redirect(other_id: Document_ID.Generic): Markups =
    3.34      {
    3.35        val rep1 =
    3.36          (for {
    3.37 -          (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
    3.38 +          (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
    3.39            if other_id == id
    3.40 -        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap
    3.41 +        } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap
    3.42        if (rep1.isEmpty) Markups.empty else new Markups(rep1)
    3.43      }
    3.44  
    3.45 @@ -156,7 +156,8 @@
    3.46      private def add_status(st: Markup): State =
    3.47        copy(status = st :: status)
    3.48  
    3.49 -    private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State =
    3.50 +    private def add_markup(
    3.51 +      status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
    3.52      {
    3.53        val markups1 =
    3.54          if (status || Protocol.liberal_status_elements(m.info.name))
    3.55 @@ -167,7 +168,7 @@
    3.56  
    3.57      def accumulate(
    3.58          self_id: Document_ID.Generic => Boolean,
    3.59 -        other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
    3.60 +        other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
    3.61          message: XML.Elem): State =
    3.62        message match {
    3.63          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    3.64 @@ -176,7 +177,7 @@
    3.65                case elem @ XML.Elem(markup, Nil) =>
    3.66                  state.
    3.67                    add_status(markup).
    3.68 -                  add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem))
    3.69 +                  add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
    3.70                case _ =>
    3.71                  System.err.println("Ignored status message: " + msg)
    3.72                  state
    3.73 @@ -194,7 +195,7 @@
    3.74                    val target =
    3.75                      if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
    3.76                        Some((chunk_name, command.chunks(chunk_name)))
    3.77 -                    else if (chunk_name == Text.Chunk.Default) other_id(id)
    3.78 +                    else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
    3.79                      else None
    3.80  
    3.81                    target match {
    3.82 @@ -216,7 +217,7 @@
    3.83                    val range = command.proper_range
    3.84                    val props = Position.purge(atts)
    3.85                    val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
    3.86 -                  state.add_markup(false, Text.Chunk.Default, info)
    3.87 +                  state.add_markup(false, Symbol.Text_Chunk.Default, info)
    3.88  
    3.89                  case _ => bad(); state
    3.90                }
    3.91 @@ -365,12 +366,12 @@
    3.92  
    3.93    /* source chunks */
    3.94  
    3.95 -  val chunk: Text.Chunk = Text.Chunk(source)
    3.96 +  val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source)
    3.97  
    3.98 -  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
    3.99 -    ((Text.Chunk.Default -> chunk) ::
   3.100 +  val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
   3.101 +    ((Symbol.Text_Chunk.Default -> chunk) ::
   3.102        (for (Exn.Res((name, Some((_, file)))) <- blobs)
   3.103 -        yield (Text.Chunk.File(name.node) -> file))).toMap
   3.104 +        yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap
   3.105  
   3.106    def length: Int = source.length
   3.107    def range: Text.Range = chunk.range
     4.1 --- a/src/Pure/PIDE/document.scala	Sat Apr 26 13:32:28 2014 +0200
     4.2 +++ b/src/Pure/PIDE/document.scala	Sat Apr 26 13:34:10 2014 +0200
     4.3 @@ -45,7 +45,7 @@
     4.4  
     4.5    /* document blobs: auxiliary files */
     4.6  
     4.7 -  sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
     4.8 +  sealed case class Blob(bytes: Bytes, chunk: Symbol.Text_Chunk, changed: Boolean)
     4.9    {
    4.10      def unchanged: Blob = copy(changed = false)
    4.11    }
    4.12 @@ -511,10 +511,11 @@
    4.13        id == st.command.id ||
    4.14        (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
    4.15  
    4.16 -    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] = None
    4.17 +    private def other_id(id: Document_ID.Generic)
    4.18 +      : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = None
    4.19      /* FIXME
    4.20        (execs.get(id) orElse commands.get(id)).map(st =>
    4.21 -        ((Text.Chunk.Id(st.command.id), st.command.chunk)))
    4.22 +        ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
    4.23      */
    4.24  
    4.25      private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
    4.26 @@ -751,8 +752,8 @@
    4.27            val former_range = revert(range).inflate_singularity
    4.28            val (chunk_name, command_iterator) =
    4.29              load_commands match {
    4.30 -              case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
    4.31 -              case _ => (Text.Chunk.Default, node.command_iterator(former_range))
    4.32 +              case command :: _ => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
    4.33 +              case _ => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
    4.34              }
    4.35            val markup_index = Command.Markup_Index(status, chunk_name)
    4.36            (for {
     5.1 --- a/src/Pure/PIDE/protocol.scala	Sat Apr 26 13:32:28 2014 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Apr 26 13:34:10 2014 +0200
     5.3 @@ -312,8 +312,8 @@
     5.4  
     5.5    def message_positions(
     5.6      self_id: Document_ID.Generic => Boolean,
     5.7 -    chunk_name: Text.Chunk.Name,
     5.8 -    chunk: Text.Chunk,
     5.9 +    chunk_name: Symbol.Text_Chunk.Name,
    5.10 +    chunk: Symbol.Text_Chunk,
    5.11      message: XML.Elem): Set[Text.Range] =
    5.12    {
    5.13      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
     6.1 --- a/src/Pure/PIDE/text.scala	Sat Apr 26 13:32:28 2014 +0200
     6.2 +++ b/src/Pure/PIDE/text.scala	Sat Apr 26 13:34:10 2014 +0200
     6.3 @@ -72,44 +72,6 @@
     6.4    }
     6.5  
     6.6  
     6.7 -  /* named chunks with sparse symbol index */
     6.8 -
     6.9 -  object Chunk
    6.10 -  {
    6.11 -    sealed abstract class Name
    6.12 -    case object Default extends Name
    6.13 -    case class Id(id: Document_ID.Generic) extends Name
    6.14 -    case class File(name: String) extends Name
    6.15 -
    6.16 -    def apply(text: CharSequence): Chunk =
    6.17 -      new Chunk(Range(0, text.length), Symbol.Index(text))
    6.18 -  }
    6.19 -
    6.20 -  final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
    6.21 -  {
    6.22 -    override def hashCode: Int = (range, symbol_index).hashCode
    6.23 -    override def equals(that: Any): Boolean =
    6.24 -      that match {
    6.25 -        case other: Chunk =>
    6.26 -          range == other.range &&
    6.27 -          symbol_index == other.symbol_index
    6.28 -        case _ => false
    6.29 -      }
    6.30 -
    6.31 -    def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
    6.32 -    def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
    6.33 -    def incorporate(symbol_range: Symbol.Range): Option[Range] =
    6.34 -    {
    6.35 -      def in(r: Symbol.Range): Option[Range] =
    6.36 -        range.try_restrict(decode(r)) match {
    6.37 -          case Some(r1) if !r1.is_singularity => Some(r1)
    6.38 -          case _ => None
    6.39 -        }
    6.40 -     in(symbol_range) orElse in(symbol_range - 1)
    6.41 -    }
    6.42 -  }
    6.43 -
    6.44 -
    6.45    /* perspective */
    6.46  
    6.47    object Perspective
     7.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Apr 26 13:32:28 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Apr 26 13:34:10 2014 +0200
     7.3 @@ -138,7 +138,7 @@
     7.4  
     7.5    /* blob */
     7.6  
     7.7 -  private var _blob: Option[(Bytes, Text.Chunk)] = None  // owned by Swing thread
     7.8 +  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by Swing thread
     7.9  
    7.10    private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
    7.11  
    7.12 @@ -151,7 +151,7 @@
    7.13              case Some(x) => x
    7.14              case None =>
    7.15                val bytes = PIDE.resources.file_content(buffer)
    7.16 -              val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
    7.17 +              val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
    7.18                _blob = Some((bytes, chunk))
    7.19                (bytes, chunk)
    7.20            }