more explicit Command.Chunk types, less ooddities;
authorwenzelm
Tue Apr 08 12:19:33 2014 +0200 (2014-04-08)
changeset 56462b64b0cb845fe
parent 56461 ae33d153f6cc
child 56463 013dfac0811a
more explicit Command.Chunk types, less ooddities;
tuned;
src/Pure/General/position.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/General/position.scala	Tue Apr 08 10:24:42 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Tue Apr 08 12:19:33 2014 +0200
     1.3 @@ -79,10 +79,15 @@
     1.4  
     1.5    object Reported
     1.6    {
     1.7 -    def unapply(pos: T): Option[(Long, String, Symbol.Range)] =
     1.8 +    def unapply(pos: T): Option[(Long, Command.Chunk.Name, Symbol.Range)] =
     1.9        (pos, pos) match {
    1.10          case (Id(id), Range(range)) =>
    1.11 -          Some((id, File.unapply(pos).getOrElse(""), range))
    1.12 +          val chunk_name =
    1.13 +            pos match {
    1.14 +              case File(name) => Command.Chunk.File_Name(name)
    1.15 +              case _ => Command.Chunk.Self
    1.16 +            }
    1.17 +          Some((id, chunk_name, range))
    1.18          case _ => None
    1.19        }
    1.20    }
     2.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 08 10:24:42 2014 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 08 12:19:33 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, File)])]
     2.8 +  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Chunk.File)])]
     2.9  
    2.10  
    2.11  
    2.12 @@ -56,14 +56,68 @@
    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 length: Int
    2.22 +    def range: Text.Range
    2.23 +    def symbol_index: Symbol.Index
    2.24 +
    2.25 +    def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset)
    2.26 +    def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
    2.27 +    def incorporate(symbol_range: Symbol.Range): Option[Text.Range] =
    2.28 +    {
    2.29 +      def in(r: Symbol.Range): Option[Text.Range] =
    2.30 +        range.try_restrict(decode(r)) match {
    2.31 +          case Some(r1) if !r1.is_singularity => Some(r1)
    2.32 +          case _ => None
    2.33 +        }
    2.34 +     in(symbol_range) orElse in(symbol_range - 1)
    2.35 +    }
    2.36 +  }
    2.37 +
    2.38 +  object Chunk
    2.39 +  {
    2.40 +    sealed abstract class Name
    2.41 +    case object Self extends Name
    2.42 +    case class File_Name(file_name: String) extends Name
    2.43 +
    2.44 +    class File(
    2.45 +      file_name: String,
    2.46 +      text: CharSequence  // non-persistent!
    2.47 +    ) extends Chunk
    2.48 +    {
    2.49 +      val name = Chunk.File_Name(file_name)
    2.50 +      val length = text.length
    2.51 +      val range = Text.Range(0, length)
    2.52 +      val symbol_index = Symbol.Index(text)
    2.53 +
    2.54 +      private val hash: Int = (name, length, symbol_index).hashCode
    2.55 +      override def hashCode: Int = hash
    2.56 +      override def equals(that: Any): Boolean =
    2.57 +        that match {
    2.58 +          case other: File =>
    2.59 +            hash == other.hash &&
    2.60 +            name == other.name &&
    2.61 +            length == other.length &&
    2.62 +            symbol_index == other.symbol_index
    2.63 +          case _ => false
    2.64 +        }
    2.65 +      override def toString: String = "Command.Chunk.File(" + file_name + ")"
    2.66 +    }
    2.67 +  }
    2.68 +
    2.69 +
    2.70    /* markup */
    2.71  
    2.72    object Markup_Index
    2.73    {
    2.74 -    val markup: Markup_Index = Markup_Index(false, "")
    2.75 +    val markup: Markup_Index = Markup_Index(false, Chunk.Self)
    2.76    }
    2.77  
    2.78 -  sealed case class Markup_Index(status: Boolean, file_name: String)
    2.79 +  sealed case class Markup_Index(status: Boolean, chunk_name: Chunk.Name)
    2.80  
    2.81    object Markups
    2.82    {
    2.83 @@ -134,13 +188,13 @@
    2.84      private def add_status(st: Markup): State =
    2.85        copy(status = st :: status)
    2.86  
    2.87 -    private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
    2.88 +    private def add_markup(status: Boolean, chunk_name: Command.Chunk.Name, m: Text.Markup): State =
    2.89      {
    2.90        val markups1 =
    2.91          if (status || Protocol.liberal_status_elements(m.info.name))
    2.92 -          markups.add(Markup_Index(true, file_name), m)
    2.93 +          markups.add(Markup_Index(true, chunk_name), m)
    2.94          else markups
    2.95 -      copy(markups = markups1.add(Markup_Index(false, file_name), m))
    2.96 +      copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
    2.97      }
    2.98  
    2.99      def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
   2.100 @@ -151,7 +205,7 @@
   2.101                case elem @ XML.Elem(markup, Nil) =>
   2.102                  state.
   2.103                    add_status(markup).
   2.104 -                  add_markup(true, "", Text.Info(command.proper_range, elem))
   2.105 +                  add_markup(true, Command.Chunk.Self, Text.Info(command.proper_range, elem))
   2.106                case _ =>
   2.107                  System.err.println("Ignored status message: " + msg)
   2.108                  state
   2.109 @@ -164,15 +218,15 @@
   2.110  
   2.111                msg match {
   2.112                  case XML.Elem(Markup(name,
   2.113 -                  atts @ Position.Reported(id, file_name, symbol_range)), args)
   2.114 +                  atts @ Position.Reported(id, chunk_name, symbol_range)), args)
   2.115                  if valid_id(id) =>
   2.116 -                  command.chunks.get(file_name) match {
   2.117 +                  command.chunks.get(chunk_name) match {
   2.118                      case Some(chunk) =>
   2.119                        chunk.incorporate(symbol_range) match {
   2.120                          case Some(range) =>
   2.121                            val props = Position.purge(atts)
   2.122                            val info = Text.Info(range, XML.Elem(Markup(name, props), args))
   2.123 -                          state.add_markup(false, file_name, info)
   2.124 +                          state.add_markup(false, chunk_name, info)
   2.125                          case None => bad(); state
   2.126                        }
   2.127                      case None => bad(); state
   2.128 @@ -183,7 +237,7 @@
   2.129                    val range = command.proper_range
   2.130                    val props = Position.purge(atts)
   2.131                    val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
   2.132 -                  state.add_markup(false, "", info)
   2.133 +                  state.add_markup(false, Command.Chunk.Self, info)
   2.134  
   2.135                  case _ => /* FIXME bad(); */ state
   2.136                }
   2.137 @@ -197,9 +251,9 @@
   2.138                var st = copy(results = results + (i -> message1))
   2.139                if (Protocol.is_inlined(message)) {
   2.140                  for {
   2.141 -                  (file_name, chunk) <- command.chunks
   2.142 +                  (chunk_name, chunk) <- command.chunks
   2.143                    range <- Protocol.message_positions(valid_id, chunk, message)
   2.144 -                } st = st.add_markup(false, file_name, Text.Info(range, message2))
   2.145 +                } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
   2.146                }
   2.147                st
   2.148  
   2.149 @@ -214,49 +268,6 @@
   2.150  
   2.151    /** static content **/
   2.152  
   2.153 -  /* text chunks */
   2.154 -
   2.155 -  abstract class Chunk
   2.156 -  {
   2.157 -    def file_name: String
   2.158 -    def length: Int
   2.159 -    def range: Text.Range
   2.160 -    def decode(symbol_range: Symbol.Range): Text.Range
   2.161 -
   2.162 -    def incorporate(symbol_range: Symbol.Range): Option[Text.Range] =
   2.163 -    {
   2.164 -      def inc(r: Symbol.Range): Option[Text.Range] =
   2.165 -        range.try_restrict(decode(r)) match {
   2.166 -          case Some(r1) if !r1.is_singularity => Some(r1)
   2.167 -          case _ => None
   2.168 -        }
   2.169 -     inc(symbol_range) orElse inc(symbol_range - 1)
   2.170 -    }
   2.171 -  }
   2.172 -
   2.173 -  // file name and position information, *without* persistent text
   2.174 -  class File(val file_name: String, text: CharSequence) extends Chunk
   2.175 -  {
   2.176 -    val length = text.length
   2.177 -    val range = Text.Range(0, length)
   2.178 -    private val symbol_index = Symbol.Index(text)
   2.179 -    def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
   2.180 -
   2.181 -    private val hash: Int = (file_name, length, symbol_index).hashCode
   2.182 -    override def hashCode: Int = hash
   2.183 -    override def equals(that: Any): Boolean =
   2.184 -      that match {
   2.185 -        case other: File =>
   2.186 -          hash == other.hash &&
   2.187 -          file_name == other.file_name &&
   2.188 -          length == other.length &&
   2.189 -          symbol_index == other.symbol_index
   2.190 -        case _ => false
   2.191 -      }
   2.192 -    override def toString: String = "Command.File(" + file_name + ")"
   2.193 -  }
   2.194 -
   2.195 -
   2.196    /* make commands */
   2.197  
   2.198    def name(span: List[Token]): String =
   2.199 @@ -344,7 +355,6 @@
   2.200      val source: String,
   2.201      val init_results: Command.Results,
   2.202      val init_markup: Markup_Tree)
   2.203 -  extends Command.Chunk
   2.204  {
   2.205    /* classification */
   2.206  
   2.207 @@ -373,14 +383,8 @@
   2.208    def blobs_digests: List[SHA1.Digest] =
   2.209      for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
   2.210  
   2.211 -  val chunks: Map[String, Command.Chunk] =
   2.212 -    (("" -> this) ::
   2.213 -      (for (Exn.Res((name, Some((_, file)))) <- blobs) yield (name.node -> file))).toMap
   2.214  
   2.215 -
   2.216 -  /* source */
   2.217 -
   2.218 -  def file_name: String = ""
   2.219 +  /* source chunks */
   2.220  
   2.221    def length: Int = source.length
   2.222    val range: Text.Range = Text.Range(0, length)
   2.223 @@ -390,9 +394,18 @@
   2.224  
   2.225    def source(range: Text.Range): String = source.substring(range.start, range.stop)
   2.226  
   2.227 -  private lazy val symbol_index = Symbol.Index(source)
   2.228 -  def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset)
   2.229 -  def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
   2.230 +  val chunk: Command.Chunk =
   2.231 +    new Command.Chunk {
   2.232 +      def name: Command.Chunk.Name = Command.Chunk.Self
   2.233 +      def length: Int = Command.this.length
   2.234 +      def range: Text.Range = Command.this.range
   2.235 +      lazy val symbol_index = Symbol.Index(source)
   2.236 +    }
   2.237 +
   2.238 +  val chunks: Map[Command.Chunk.Name, Command.Chunk] =
   2.239 +    ((Command.Chunk.Self -> chunk) ::
   2.240 +      (for (Exn.Res((name, Some((_, file)))) <- blobs)
   2.241 +        yield (Command.Chunk.File_Name(name.node) -> file))).toMap
   2.242  
   2.243  
   2.244    /* accumulated results */
     3.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 08 10:24:42 2014 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 08 12:19:33 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.File, changed: Boolean)
     3.8 +  sealed case class Blob(bytes: Bytes, file: Command.Chunk.File, changed: Boolean)
     3.9    {
    3.10      def unchanged: Blob = copy(changed = false)
    3.11    }
    3.12 @@ -731,15 +731,15 @@
    3.13            status: Boolean = false): List[Text.Info[A]] =
    3.14          {
    3.15            val former_range = revert(range)
    3.16 -          val (file_name, command_iterator) =
    3.17 +          val (chunk_name, command_iterator) =
    3.18              load_commands match {
    3.19 -              case command :: _ => (node_name.node, Iterator((command, 0)))
    3.20 -              case _ => ("", node.command_iterator(former_range))
    3.21 +              case command :: _ => (Command.Chunk.File_Name(node_name.node), Iterator((command, 0)))
    3.22 +              case _ => (Command.Chunk.Self, node.command_iterator(former_range))
    3.23              }
    3.24 -          val markup_index = Command.Markup_Index(status, file_name)
    3.25 +          val markup_index = Command.Markup_Index(status, chunk_name)
    3.26            (for {
    3.27              (command, command_start) <- command_iterator
    3.28 -            chunk <- command.chunks.get(file_name).iterator
    3.29 +            chunk <- command.chunks.get(chunk_name).iterator
    3.30              states = state.command_states(version, command)
    3.31              res = result(states)
    3.32              range = (former_range - command_start).restrict(chunk.range)
     4.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 10:24:42 2014 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 12:19:33 2014 +0200
     4.3 @@ -307,8 +307,8 @@
     4.4    {
     4.5      def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
     4.6        props match {
     4.7 -        case Position.Reported(id, file_name, symbol_range)
     4.8 -        if valid_id(id) && file_name == chunk.file_name =>
     4.9 +        case Position.Reported(id, chunk_name, symbol_range)
    4.10 +        if valid_id(id) && chunk_name == chunk.name =>
    4.11            chunk.incorporate(symbol_range) match {
    4.12              case Some(range) => set + range
    4.13              case _ => set
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 10:24:42 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 12:19:33 2014 +0200
     5.3 @@ -138,7 +138,7 @@
     5.4  
     5.5    /* blob */
     5.6  
     5.7 -  private var _blob: Option[(Bytes, Command.File)] = None  // owned by Swing thread
     5.8 +  private var _blob: Option[(Bytes, Command.Chunk.File)] = None  // owned by Swing thread
     5.9  
    5.10    private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
    5.11  
    5.12 @@ -151,7 +151,8 @@
    5.13              case Some(x) => x
    5.14              case None =>
    5.15                val bytes = PIDE.resources.file_content(buffer)
    5.16 -              val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
    5.17 +              val file =
    5.18 +                new Command.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength))
    5.19                _blob = Some((bytes, file))
    5.20                (bytes, file)
    5.21            }
     6.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 08 10:24:42 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 08 12:19:33 2014 +0200
     6.3 @@ -220,7 +220,7 @@
     6.4            val sources_iterator =
     6.5              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
     6.6                (if (offset == 0) Iterator.empty
     6.7 -               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
     6.8 +               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
     6.9            val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
    6.10            Some(hyperlink_file(file_name, line, column))
    6.11        }