tuned signature -- moved Command.Chunk to Text.Chunk;
authorwenzelm
Tue Apr 08 15:12:54 2014 +0200 (2014-04-08)
changeset 5646830128d1acfbc
parent 56467 8d7d6f17c6a7
child 56469 ffc94a271633
tuned signature -- moved Command.Chunk to Text.Chunk;
src/Pure/General/position.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	Tue Apr 08 14:59:36 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Tue Apr 08 15:12:54 2014 +0200
     1.3 @@ -83,13 +83,13 @@
     1.4  
     1.5    object Reported
     1.6    {
     1.7 -    def unapply(pos: T): Option[(Long, Command.Chunk.Name, Symbol.Range)] =
     1.8 +    def unapply(pos: T): Option[(Long, 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) => Command.Chunk.File_Name(name)
    1.14 -              case _ => Command.Chunk.Self
    1.15 +              case File(name) => Text.Chunk.File_Name(name)
    1.16 +              case _ => Text.Chunk.Default
    1.17              }
    1.18            Some((id, chunk_name, range))
    1.19          case _ => None
     2.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 08 14:59:36 2014 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 08 15:12:54 2014 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  object Command
     2.5  {
     2.6    type Edit = (Option[Command], Option[Command])
     2.7 -  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Chunk.File)])]
     2.8 +  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk.File)])]
     2.9  
    2.10  
    2.11  
    2.12 @@ -56,63 +56,14 @@
    2.13    }
    2.14  
    2.15  
    2.16 -  /* source chunks */
    2.17 -
    2.18 -  abstract class Chunk
    2.19 -  {
    2.20 -    def name: Chunk.Name
    2.21 -    def range: Text.Range
    2.22 -    def symbol_index: Symbol.Index
    2.23 -
    2.24 -    private lazy val hash: Int = (name, range, symbol_index).hashCode
    2.25 -    override def hashCode: Int = hash
    2.26 -    override def equals(that: Any): Boolean =
    2.27 -      that match {
    2.28 -        case other: Chunk =>
    2.29 -          hash == other.hash &&
    2.30 -          name == other.name &&
    2.31 -          range == other.range &&
    2.32 -          symbol_index == other.symbol_index
    2.33 -        case _ => false
    2.34 -      }
    2.35 -    override def toString: String = "Command.Chunk(" + name + ")"
    2.36 -
    2.37 -    def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset)
    2.38 -    def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
    2.39 -    def incorporate(symbol_range: Symbol.Range): Option[Text.Range] =
    2.40 -    {
    2.41 -      def in(r: Symbol.Range): Option[Text.Range] =
    2.42 -        range.try_restrict(decode(r)) match {
    2.43 -          case Some(r1) if !r1.is_singularity => Some(r1)
    2.44 -          case _ => None
    2.45 -        }
    2.46 -     in(symbol_range) orElse in(symbol_range - 1)
    2.47 -    }
    2.48 -  }
    2.49 -
    2.50 -  object Chunk
    2.51 -  {
    2.52 -    sealed abstract class Name
    2.53 -    case object Self extends Name
    2.54 -    case class File_Name(file_name: String) extends Name
    2.55 -
    2.56 -    class File(file_name: String, text: CharSequence) extends Chunk
    2.57 -    {
    2.58 -      val name = Chunk.File_Name(file_name)
    2.59 -      val range = Text.Range(0, text.length)
    2.60 -      val symbol_index = Symbol.Index(text)
    2.61 -    }
    2.62 -  }
    2.63 -
    2.64 -
    2.65    /* markup */
    2.66  
    2.67    object Markup_Index
    2.68    {
    2.69 -    val markup: Markup_Index = Markup_Index(false, Chunk.Self)
    2.70 +    val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default)
    2.71    }
    2.72  
    2.73 -  sealed case class Markup_Index(status: Boolean, chunk_name: Chunk.Name)
    2.74 +  sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name)
    2.75  
    2.76    object Markups
    2.77    {
    2.78 @@ -183,7 +134,7 @@
    2.79      private def add_status(st: Markup): State =
    2.80        copy(status = st :: status)
    2.81  
    2.82 -    private def add_markup(status: Boolean, chunk_name: Command.Chunk.Name, m: Text.Markup): State =
    2.83 +    private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State =
    2.84      {
    2.85        val markups1 =
    2.86          if (status || Protocol.liberal_status_elements(m.info.name))
    2.87 @@ -200,7 +151,7 @@
    2.88                case elem @ XML.Elem(markup, Nil) =>
    2.89                  state.
    2.90                    add_status(markup).
    2.91 -                  add_markup(true, Command.Chunk.Self, Text.Info(command.proper_range, elem))
    2.92 +                  add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem))
    2.93                case _ =>
    2.94                  System.err.println("Ignored status message: " + msg)
    2.95                  state
    2.96 @@ -232,7 +183,7 @@
    2.97                    val range = command.proper_range
    2.98                    val props = Position.purge(atts)
    2.99                    val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
   2.100 -                  state.add_markup(false, Command.Chunk.Self, info)
   2.101 +                  state.add_markup(false, Text.Chunk.Default, info)
   2.102  
   2.103                  case _ => /* FIXME bad(); */ state
   2.104                }
   2.105 @@ -389,17 +340,17 @@
   2.106  
   2.107    def source(range: Text.Range): String = source.substring(range.start, range.stop)
   2.108  
   2.109 -  val chunk: Command.Chunk =
   2.110 -    new Command.Chunk {
   2.111 -      def name: Command.Chunk.Name = Command.Chunk.Self
   2.112 +  val chunk: Text.Chunk =
   2.113 +    new Text.Chunk {
   2.114 +      def name: Text.Chunk.Name = Text.Chunk.Default
   2.115        def range: Text.Range = Command.this.range
   2.116        lazy val symbol_index = Symbol.Index(source)
   2.117      }
   2.118  
   2.119 -  val chunks: Map[Command.Chunk.Name, Command.Chunk] =
   2.120 -    ((Command.Chunk.Self -> chunk) ::
   2.121 +  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
   2.122 +    ((Text.Chunk.Default -> chunk) ::
   2.123        (for (Exn.Res((name, Some((_, file)))) <- blobs)
   2.124 -        yield (Command.Chunk.File_Name(name.node) -> file))).toMap
   2.125 +        yield (Text.Chunk.File_Name(name.node) -> file))).toMap
   2.126  
   2.127  
   2.128    /* accumulated results */
     3.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 08 14:59:36 2014 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 08 15:12:54 2014 +0200
     3.3 @@ -45,7 +45,7 @@
     3.4  
     3.5    /* document blobs: auxiliary files */
     3.6  
     3.7 -  sealed case class Blob(bytes: Bytes, file: Command.Chunk.File, changed: Boolean)
     3.8 +  sealed case class Blob(bytes: Bytes, file: Text.Chunk.File, changed: Boolean)
     3.9    {
    3.10      def unchanged: Blob = copy(changed = false)
    3.11    }
    3.12 @@ -733,8 +733,8 @@
    3.13            val former_range = revert(range)
    3.14            val (chunk_name, command_iterator) =
    3.15              load_commands match {
    3.16 -              case command :: _ => (Command.Chunk.File_Name(node_name.node), Iterator((command, 0)))
    3.17 -              case _ => (Command.Chunk.Self, node.command_iterator(former_range))
    3.18 +              case command :: _ => (Text.Chunk.File_Name(node_name.node), Iterator((command, 0)))
    3.19 +              case _ => (Text.Chunk.Default, node.command_iterator(former_range))
    3.20              }
    3.21            val markup_index = Command.Markup_Index(status, chunk_name)
    3.22            (for {
     4.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 14:59:36 2014 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 15:12:54 2014 +0200
     4.3 @@ -302,7 +302,7 @@
     4.4  
     4.5    def message_positions(
     4.6      valid_id: Document_ID.Generic => Boolean,
     4.7 -    chunk: Command.Chunk,
     4.8 +    chunk: Text.Chunk,
     4.9      message: XML.Elem): Set[Text.Range] =
    4.10    {
    4.11      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
     5.1 --- a/src/Pure/PIDE/text.scala	Tue Apr 08 14:59:36 2014 +0200
     5.2 +++ b/src/Pure/PIDE/text.scala	Tue Apr 08 15:12:54 2014 +0200
     5.3 @@ -71,6 +71,55 @@
     5.4    }
     5.5  
     5.6  
     5.7 +  /* named chunks */
     5.8 +
     5.9 +  abstract class Chunk
    5.10 +  {
    5.11 +    def name: Chunk.Name
    5.12 +    def range: Range
    5.13 +    def symbol_index: Symbol.Index
    5.14 +
    5.15 +    private lazy val hash: Int = (name, range, symbol_index).hashCode
    5.16 +    override def hashCode: Int = hash
    5.17 +    override def equals(that: Any): Boolean =
    5.18 +      that match {
    5.19 +        case other: Chunk =>
    5.20 +          hash == other.hash &&
    5.21 +          name == other.name &&
    5.22 +          range == other.range &&
    5.23 +          symbol_index == other.symbol_index
    5.24 +        case _ => false
    5.25 +      }
    5.26 +    override def toString: String = "Text.Chunk(" + name + ")"
    5.27 +
    5.28 +    def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
    5.29 +    def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
    5.30 +    def incorporate(symbol_range: Symbol.Range): Option[Range] =
    5.31 +    {
    5.32 +      def in(r: Symbol.Range): Option[Range] =
    5.33 +        range.try_restrict(decode(r)) match {
    5.34 +          case Some(r1) if !r1.is_singularity => Some(r1)
    5.35 +          case _ => None
    5.36 +        }
    5.37 +     in(symbol_range) orElse in(symbol_range - 1)
    5.38 +    }
    5.39 +  }
    5.40 +
    5.41 +  object Chunk
    5.42 +  {
    5.43 +    sealed abstract class Name
    5.44 +    case object Default extends Name
    5.45 +    case class File_Name(file_name: String) extends Name
    5.46 +
    5.47 +    class File(file_name: String, text: CharSequence) extends Chunk
    5.48 +    {
    5.49 +      val name = File_Name(file_name)
    5.50 +      val range = Range(0, text.length)
    5.51 +      val symbol_index = Symbol.Index(text)
    5.52 +    }
    5.53 +  }
    5.54 +
    5.55 +
    5.56    /* perspective */
    5.57  
    5.58    object Perspective
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 14:59:36 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 15:12:54 2014 +0200
     6.3 @@ -138,7 +138,7 @@
     6.4  
     6.5    /* blob */
     6.6  
     6.7 -  private var _blob: Option[(Bytes, Command.Chunk.File)] = None  // owned by Swing thread
     6.8 +  private var _blob: Option[(Bytes, Text.Chunk.File)] = None  // owned by Swing thread
     6.9  
    6.10    private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
    6.11  
    6.12 @@ -151,8 +151,7 @@
    6.13              case Some(x) => x
    6.14              case None =>
    6.15                val bytes = PIDE.resources.file_content(buffer)
    6.16 -              val file =
    6.17 -                new Command.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength))
    6.18 +              val file = new Text.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength))
    6.19                _blob = Some((bytes, file))
    6.20                (bytes, file)
    6.21            }