# HG changeset patch # User wenzelm # Date 1396952373 -7200 # Node ID b64b0cb845fef2fe0b207c4c0a07fdfc672afabc # Parent ae33d153f6cc5db149967f60c2433c6667362b1e more explicit Command.Chunk types, less ooddities; tuned; diff -r ae33d153f6cc -r b64b0cb845fe src/Pure/General/position.scala --- a/src/Pure/General/position.scala Tue Apr 08 10:24:42 2014 +0200 +++ b/src/Pure/General/position.scala Tue Apr 08 12:19:33 2014 +0200 @@ -79,10 +79,15 @@ object Reported { - def unapply(pos: T): Option[(Long, String, Symbol.Range)] = + def unapply(pos: T): Option[(Long, Command.Chunk.Name, Symbol.Range)] = (pos, pos) match { case (Id(id), Range(range)) => - Some((id, File.unapply(pos).getOrElse(""), range)) + val chunk_name = + pos match { + case File(name) => Command.Chunk.File_Name(name) + case _ => Command.Chunk.Self + } + Some((id, chunk_name, range)) case _ => None } } diff -r ae33d153f6cc -r b64b0cb845fe src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Apr 08 10:24:42 2014 +0200 +++ b/src/Pure/PIDE/command.scala Tue Apr 08 12:19:33 2014 +0200 @@ -15,7 +15,7 @@ object Command { type Edit = (Option[Command], Option[Command]) - type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])] + type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Chunk.File)])] @@ -56,14 +56,68 @@ } + /* source chunks */ + + abstract class Chunk + { + def name: Chunk.Name + def length: Int + def range: Text.Range + def symbol_index: Symbol.Index + + 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 // non-persistent! + ) extends Chunk + { + val name = Chunk.File_Name(file_name) + val length = text.length + val range = Text.Range(0, length) + val symbol_index = Symbol.Index(text) + + private val hash: Int = (name, length, symbol_index).hashCode + override def hashCode: Int = hash + override def equals(that: Any): Boolean = + that match { + case other: File => + hash == other.hash && + name == other.name && + length == other.length && + symbol_index == other.symbol_index + case _ => false + } + override def toString: String = "Command.Chunk.File(" + file_name + ")" + } + } + + /* markup */ object Markup_Index { - val markup: Markup_Index = Markup_Index(false, "") + val markup: Markup_Index = Markup_Index(false, Chunk.Self) } - sealed case class Markup_Index(status: Boolean, file_name: String) + sealed case class Markup_Index(status: Boolean, chunk_name: Chunk.Name) object Markups { @@ -134,13 +188,13 @@ private def add_status(st: Markup): State = copy(status = st :: status) - private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State = + private def add_markup(status: Boolean, chunk_name: Command.Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Protocol.liberal_status_elements(m.info.name)) - markups.add(Markup_Index(true, file_name), m) + markups.add(Markup_Index(true, chunk_name), m) else markups - copy(markups = markups1.add(Markup_Index(false, file_name), m)) + copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) } def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State = @@ -151,7 +205,7 @@ case elem @ XML.Elem(markup, Nil) => state. add_status(markup). - add_markup(true, "", Text.Info(command.proper_range, elem)) + add_markup(true, Command.Chunk.Self, Text.Info(command.proper_range, elem)) case _ => System.err.println("Ignored status message: " + msg) state @@ -164,15 +218,15 @@ msg match { case XML.Elem(Markup(name, - atts @ Position.Reported(id, file_name, symbol_range)), args) + atts @ Position.Reported(id, chunk_name, symbol_range)), args) if valid_id(id) => - command.chunks.get(file_name) match { + command.chunks.get(chunk_name) match { case Some(chunk) => chunk.incorporate(symbol_range) match { case Some(range) => val props = Position.purge(atts) val info = Text.Info(range, XML.Elem(Markup(name, props), args)) - state.add_markup(false, file_name, info) + state.add_markup(false, chunk_name, info) case None => bad(); state } case None => bad(); state @@ -183,7 +237,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, "", info) + state.add_markup(false, Command.Chunk.Self, info) case _ => /* FIXME bad(); */ state } @@ -197,9 +251,9 @@ var st = copy(results = results + (i -> message1)) if (Protocol.is_inlined(message)) { for { - (file_name, chunk) <- command.chunks + (chunk_name, chunk) <- command.chunks range <- Protocol.message_positions(valid_id, chunk, message) - } st = st.add_markup(false, file_name, Text.Info(range, message2)) + } st = st.add_markup(false, chunk_name, Text.Info(range, message2)) } st @@ -214,49 +268,6 @@ /** static content **/ - /* text chunks */ - - abstract class Chunk - { - def file_name: String - def length: Int - def range: Text.Range - def decode(symbol_range: Symbol.Range): Text.Range - - def incorporate(symbol_range: Symbol.Range): Option[Text.Range] = - { - def inc(r: Symbol.Range): Option[Text.Range] = - range.try_restrict(decode(r)) match { - case Some(r1) if !r1.is_singularity => Some(r1) - case _ => None - } - inc(symbol_range) orElse inc(symbol_range - 1) - } - } - - // file name and position information, *without* persistent text - class File(val file_name: String, text: CharSequence) extends Chunk - { - val length = text.length - val range = Text.Range(0, length) - private val symbol_index = Symbol.Index(text) - def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range) - - private val hash: Int = (file_name, length, symbol_index).hashCode - override def hashCode: Int = hash - override def equals(that: Any): Boolean = - that match { - case other: File => - hash == other.hash && - file_name == other.file_name && - length == other.length && - symbol_index == other.symbol_index - case _ => false - } - override def toString: String = "Command.File(" + file_name + ")" - } - - /* make commands */ def name(span: List[Token]): String = @@ -344,7 +355,6 @@ val source: String, val init_results: Command.Results, val init_markup: Markup_Tree) - extends Command.Chunk { /* classification */ @@ -373,14 +383,8 @@ def blobs_digests: List[SHA1.Digest] = for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest - val chunks: Map[String, Command.Chunk] = - (("" -> this) :: - (for (Exn.Res((name, Some((_, file)))) <- blobs) yield (name.node -> file))).toMap - - /* source */ - - def file_name: String = "" + /* source chunks */ def length: Int = source.length val range: Text.Range = Text.Range(0, length) @@ -390,9 +394,18 @@ def source(range: Text.Range): String = source.substring(range.start, range.stop) - private lazy val symbol_index = Symbol.Index(source) - 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) + val chunk: Command.Chunk = + new Command.Chunk { + def name: Command.Chunk.Name = Command.Chunk.Self + def length: Int = Command.this.length + 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) :: + (for (Exn.Res((name, Some((_, file)))) <- blobs) + yield (Command.Chunk.File_Name(name.node) -> file))).toMap /* accumulated results */ diff -r ae33d153f6cc -r b64b0cb845fe src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Apr 08 10:24:42 2014 +0200 +++ b/src/Pure/PIDE/document.scala Tue Apr 08 12:19:33 2014 +0200 @@ -45,7 +45,7 @@ /* document blobs: auxiliary files */ - sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean) + sealed case class Blob(bytes: Bytes, file: Command.Chunk.File, changed: Boolean) { def unchanged: Blob = copy(changed = false) } @@ -731,15 +731,15 @@ status: Boolean = false): List[Text.Info[A]] = { val former_range = revert(range) - val (file_name, command_iterator) = + val (chunk_name, command_iterator) = load_commands match { - case command :: _ => (node_name.node, Iterator((command, 0))) - case _ => ("", node.command_iterator(former_range)) + case command :: _ => (Command.Chunk.File_Name(node_name.node), Iterator((command, 0))) + case _ => (Command.Chunk.Self, node.command_iterator(former_range)) } - val markup_index = Command.Markup_Index(status, file_name) + val markup_index = Command.Markup_Index(status, chunk_name) (for { (command, command_start) <- command_iterator - chunk <- command.chunks.get(file_name).iterator + chunk <- command.chunks.get(chunk_name).iterator states = state.command_states(version, command) res = result(states) range = (former_range - command_start).restrict(chunk.range) diff -r ae33d153f6cc -r b64b0cb845fe src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Apr 08 10:24:42 2014 +0200 +++ b/src/Pure/PIDE/protocol.scala Tue Apr 08 12:19:33 2014 +0200 @@ -307,8 +307,8 @@ { def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = props match { - case Position.Reported(id, file_name, symbol_range) - if valid_id(id) && file_name == chunk.file_name => + case Position.Reported(id, chunk_name, symbol_range) + if valid_id(id) && chunk_name == chunk.name => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set diff -r ae33d153f6cc -r b64b0cb845fe src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Apr 08 10:24:42 2014 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Tue Apr 08 12:19:33 2014 +0200 @@ -138,7 +138,7 @@ /* blob */ - private var _blob: Option[(Bytes, Command.File)] = None // owned by Swing thread + private var _blob: Option[(Bytes, Command.Chunk.File)] = None // owned by Swing thread private def reset_blob(): Unit = Swing_Thread.require { _blob = None } @@ -151,7 +151,8 @@ case Some(x) => x case None => val bytes = PIDE.resources.file_content(buffer) - val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength)) + val file = + new Command.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength)) _blob = Some((bytes, file)) (bytes, file) } diff -r ae33d153f6cc -r b64b0cb845fe src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Tue Apr 08 10:24:42 2014 +0200 +++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Apr 08 12:19:33 2014 +0200 @@ -220,7 +220,7 @@ val sources_iterator = node.commands.iterator.takeWhile(_ != command).map(_.source) ++ (if (offset == 0) Iterator.empty - else Iterator.single(command.source(Text.Range(0, command.decode(offset))))) + else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset))))) val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column) Some(hyperlink_file(file_name, line, column)) }