common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
authorwenzelm
Tue Feb 11 17:44:29 2014 +0100 (2014-02-11)
changeset 55431e0f20a44ff9d
parent 55430 8eb6c740ec1a
child 55432 9c53198dbb1c
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Feb 11 15:55:05 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Feb 11 17:44:29 2014 +0100
     1.3 @@ -94,8 +94,8 @@
     1.4          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
     1.5            (this /: msgs)((state, msg) =>
     1.6              msg match {
     1.7 -              case XML.Elem(Markup(name, atts @ Position.Reported(id, file, raw_range)), args)
     1.8 -              if (id == command.id || id == alt_id) && file == "" &&
     1.9 +              case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
    1.10 +              if (id == command.id || id == alt_id) && file_name == "" &&
    1.11                    command.range.contains(command.decode(raw_range)) =>
    1.12                  val range = command.decode(raw_range)
    1.13                  val props = Position.purge(atts)
    1.14 @@ -120,7 +120,7 @@
    1.15                val st0 = copy(results = results + (i -> message1))
    1.16                val st1 =
    1.17                  if (Protocol.is_inlined(message))
    1.18 -                  (st0 /: Protocol.message_positions(command, message))(
    1.19 +                  (st0 /: Protocol.message_positions(command.id, command, message))(
    1.20                      (st, range) => st.add_markup(Text.Info(range, message2)))
    1.21                  else st0
    1.22  
    1.23 @@ -139,12 +139,34 @@
    1.24    }
    1.25  
    1.26  
    1.27 +
    1.28 +  /** static content **/
    1.29 +
    1.30 +  /* text chunks */
    1.31 +
    1.32 +  abstract class Chunk
    1.33 +  {
    1.34 +    def file_name: String
    1.35 +    def length: Int
    1.36 +    def range: Text.Range
    1.37 +    def decode(r: Text.Range): Text.Range
    1.38 +  }
    1.39 +
    1.40 +  class File(val file_name: String, text: CharSequence) extends Chunk
    1.41 +  {
    1.42 +    val length = text.length
    1.43 +    val range = Text.Range(0, length)
    1.44 +    private val symbol_index = Symbol.Index(text)
    1.45 +    def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
    1.46 +  }
    1.47 +
    1.48 +
    1.49    /* make commands */
    1.50  
    1.51    def name(span: List[Token]): String =
    1.52      span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
    1.53  
    1.54 -  type Blob = Exn.Result[(Document.Node.Name, Option[SHA1.Digest])]
    1.55 +  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
    1.56  
    1.57    def apply(
    1.58      id: Document_ID.Command,
    1.59 @@ -220,6 +242,7 @@
    1.60      val source: String,
    1.61      val init_results: Command.Results,
    1.62      val init_markup: Markup_Tree)
    1.63 +  extends Command.Chunk
    1.64  {
    1.65    /* classification */
    1.66  
    1.67 @@ -243,11 +266,13 @@
    1.68      for (Exn.Res((name, _)) <- blobs) yield name
    1.69  
    1.70    def blobs_digests: List[SHA1.Digest] =
    1.71 -    for (Exn.Res((_, Some(digest))) <- blobs) yield digest
    1.72 +    for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
    1.73  
    1.74  
    1.75    /* source */
    1.76  
    1.77 +  def file_name: String = ""
    1.78 +
    1.79    def length: Int = source.length
    1.80    val range: Text.Range = Text.Range(0, length)
    1.81  
     2.1 --- a/src/Pure/PIDE/document.scala	Tue Feb 11 15:55:05 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Tue Feb 11 17:44:29 2014 +0100
     2.3 @@ -47,7 +47,7 @@
     2.4    type Edit_Text = Edit[Text.Edit, Text.Perspective]
     2.5    type Edit_Command = Edit[Command.Edit, Command.Perspective]
     2.6  
     2.7 -  type Blobs = Map[Node.Name, Bytes]
     2.8 +  type Blobs = Map[Node.Name, (Bytes, Command.File)]
     2.9  
    2.10    object Node
    2.11    {
     3.1 --- a/src/Pure/PIDE/protocol.scala	Tue Feb 11 15:55:05 2014 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Feb 11 17:44:29 2014 +0100
     3.3 @@ -274,22 +274,25 @@
     3.4  
     3.5    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     3.6  
     3.7 -  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
     3.8 +  def message_positions(command_id: Document_ID.Command, chunk: Command.Chunk, message: XML.Elem)
     3.9 +    : Set[Text.Range] =
    3.10    {
    3.11      def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body)
    3.12        : Set[Text.Range] =
    3.13      {
    3.14 -      val range = command.decode(raw_range).restrict(command.range)
    3.15 +      val range = chunk.decode(raw_range).restrict(chunk.range)
    3.16        body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    3.17      }
    3.18  
    3.19      def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    3.20        tree match {
    3.21 -        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file, range)), _, body)
    3.22 -        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
    3.23 +        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file_name, range)), _, body)
    3.24 +        if include_pos(name) && id == command_id && file_name == chunk.file_name =>
    3.25 +        elem_positions(range, set, body)
    3.26  
    3.27 -        case XML.Elem(Markup(name, Position.Reported(id, file, range)), body)
    3.28 -        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
    3.29 +        case XML.Elem(Markup(name, Position.Reported(id, file_name, range)), body)
    3.30 +        if include_pos(name) && id == command_id && file_name == chunk.file_name =>
    3.31 +        elem_positions(range, set, body)
    3.32  
    3.33          case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)
    3.34  
    3.35 @@ -300,7 +303,7 @@
    3.36  
    3.37      val set = positions(Set.empty, message)
    3.38      if (set.isEmpty)
    3.39 -      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
    3.40 +      set ++ Position.Range.unapply(message.markup.properties).map(chunk.decode(_))
    3.41      else set
    3.42    }
    3.43  }
    3.44 @@ -323,7 +326,7 @@
    3.45        val encode_blob: T[Command.Blob] =
    3.46          variant(List(
    3.47            { case Exn.Res((a, b)) =>
    3.48 -              (Nil, pair(string, option(string))((a.node, b.map(_.toString)))) },
    3.49 +              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
    3.50            { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    3.51        YXML.string_of_body(list(encode_blob)(command.blobs))
    3.52      }
     4.1 --- a/src/Pure/System/session.scala	Tue Feb 11 15:55:05 2014 +0100
     4.2 +++ b/src/Pure/System/session.scala	Tue Feb 11 17:44:29 2014 +0100
     4.3 @@ -379,7 +379,7 @@
     4.4            digest <- command.blobs_digests
     4.5            if !global_state().defined_blob(digest)
     4.6          } {
     4.7 -          doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
     4.8 +          doc_blobs.collectFirst({ case (_, (b, _)) if b.sha1_digest == digest => b }) match {
     4.9              case Some(blob) =>
    4.10                global_state >> (_.define_blob(digest))
    4.11                prover.get.define_blob(blob)
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Feb 11 15:55:05 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Feb 11 17:44:29 2014 +0100
     5.3 @@ -264,11 +264,16 @@
     5.4        doc_blobs: Document.Blobs)
     5.5      : List[Command.Blob] =
     5.6    {
     5.7 -    span_files(syntax, span).map(file =>
     5.8 +    span_files(syntax, span).map(file_name =>
     5.9        Exn.capture {
    5.10          val name =
    5.11 -          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
    5.12 -        (name, doc_blobs.get(name).map(_.sha1_digest))
    5.13 +          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name)))
    5.14 +        val blob =
    5.15 +          doc_blobs.get(name) match {
    5.16 +            case Some((bytes, file)) => Some((bytes.sha1_digest, file))
    5.17 +            case None => None
    5.18 +          }
    5.19 +        (name, blob)
    5.20        }
    5.21      )
    5.22    }
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Feb 11 15:55:05 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Feb 11 17:44:29 2014 +0100
     6.3 @@ -131,18 +131,19 @@
     6.4  
     6.5    /* blob */
     6.6  
     6.7 -  private var _blob: Option[Bytes] = None  // owned by Swing thread
     6.8 +  private var _blob: Option[(Bytes, Command.File)] = None  // owned by Swing thread
     6.9  
    6.10    private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
    6.11  
    6.12 -  def blob(): Bytes =
    6.13 +  def blob(): (Bytes, Command.File) =
    6.14      Swing_Thread.require {
    6.15        _blob match {
    6.16 -        case Some(b) => b
    6.17 +        case Some(x) => x
    6.18          case None =>
    6.19            val b = PIDE.thy_load.file_content(buffer)
    6.20 -          _blob = Some(b)
    6.21 -          b
    6.22 +          val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
    6.23 +          _blob = Some((b, file))
    6.24 +          (b, file)
    6.25        }
    6.26      }
    6.27