# HG changeset patch
# User wenzelm
# Date 1392137069 -3600
# Node ID e0f20a44ff9d33e1ff1967c805c83222d93c2640
# Parent  8eb6c740ec1abc0f4ee99af6441f41690806779e
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;

diff -r 8eb6c740ec1a -r e0f20a44ff9d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Feb 11 15:55:05 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Feb 11 17:44:29 2014 +0100
@@ -94,8 +94,8 @@
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
-              case XML.Elem(Markup(name, atts @ Position.Reported(id, file, raw_range)), args)
-              if (id == command.id || id == alt_id) && file == "" &&
+              case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
+              if (id == command.id || id == alt_id) && file_name == "" &&
                   command.range.contains(command.decode(raw_range)) =>
                 val range = command.decode(raw_range)
                 val props = Position.purge(atts)
@@ -120,7 +120,7 @@
               val st0 = copy(results = results + (i -> message1))
               val st1 =
                 if (Protocol.is_inlined(message))
-                  (st0 /: Protocol.message_positions(command, message))(
+                  (st0 /: Protocol.message_positions(command.id, command, message))(
                     (st, range) => st.add_markup(Text.Info(range, message2)))
                 else st0
 
@@ -139,12 +139,34 @@
   }
 
 
+
+  /** static content **/
+
+  /* text chunks */
+
+  abstract class Chunk
+  {
+    def file_name: String
+    def length: Int
+    def range: Text.Range
+    def decode(r: Text.Range): Text.Range
+  }
+
+  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(r: Text.Range): Text.Range = symbol_index.decode(r)
+  }
+
+
   /* make commands */
 
   def name(span: List[Token]): String =
     span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
-  type Blob = Exn.Result[(Document.Node.Name, Option[SHA1.Digest])]
+  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
 
   def apply(
     id: Document_ID.Command,
@@ -220,6 +242,7 @@
     val source: String,
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
+  extends Command.Chunk
 {
   /* classification */
 
@@ -243,11 +266,13 @@
     for (Exn.Res((name, _)) <- blobs) yield name
 
   def blobs_digests: List[SHA1.Digest] =
-    for (Exn.Res((_, Some(digest))) <- blobs) yield digest
+    for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
 
 
   /* source */
 
+  def file_name: String = ""
+
   def length: Int = source.length
   val range: Text.Range = Text.Range(0, length)
 
diff -r 8eb6c740ec1a -r e0f20a44ff9d src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Feb 11 15:55:05 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Feb 11 17:44:29 2014 +0100
@@ -47,7 +47,7 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
-  type Blobs = Map[Node.Name, Bytes]
+  type Blobs = Map[Node.Name, (Bytes, Command.File)]
 
   object Node
   {
diff -r 8eb6c740ec1a -r e0f20a44ff9d src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Feb 11 15:55:05 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Feb 11 17:44:29 2014 +0100
@@ -274,22 +274,25 @@
 
   private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
-  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
+  def message_positions(command_id: Document_ID.Command, chunk: Command.Chunk, message: XML.Elem)
+    : Set[Text.Range] =
   {
     def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body)
       : Set[Text.Range] =
     {
-      val range = command.decode(raw_range).restrict(command.range)
+      val range = chunk.decode(raw_range).restrict(chunk.range)
       body.foldLeft(if (range.is_singularity) set else set + range)(positions)
     }
 
     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
-        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file, range)), _, body)
-        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
+        case XML.Wrapped_Elem(Markup(name, Position.Reported(id, file_name, range)), _, body)
+        if include_pos(name) && id == command_id && file_name == chunk.file_name =>
+        elem_positions(range, set, body)
 
-        case XML.Elem(Markup(name, Position.Reported(id, file, range)), body)
-        if include_pos(name) && id == command.id && file == "" => elem_positions(range, set, body)
+        case XML.Elem(Markup(name, Position.Reported(id, file_name, range)), body)
+        if include_pos(name) && id == command_id && file_name == chunk.file_name =>
+        elem_positions(range, set, body)
 
         case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)
 
@@ -300,7 +303,7 @@
 
     val set = positions(Set.empty, message)
     if (set.isEmpty)
-      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
+      set ++ Position.Range.unapply(message.markup.properties).map(chunk.decode(_))
     else set
   }
 }
@@ -323,7 +326,7 @@
       val encode_blob: T[Command.Blob] =
         variant(List(
           { case Exn.Res((a, b)) =>
-              (Nil, pair(string, option(string))((a.node, b.map(_.toString)))) },
+              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
       YXML.string_of_body(list(encode_blob)(command.blobs))
     }
diff -r 8eb6c740ec1a -r e0f20a44ff9d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Feb 11 15:55:05 2014 +0100
+++ b/src/Pure/System/session.scala	Tue Feb 11 17:44:29 2014 +0100
@@ -379,7 +379,7 @@
           digest <- command.blobs_digests
           if !global_state().defined_blob(digest)
         } {
-          doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
+          doc_blobs.collectFirst({ case (_, (b, _)) if b.sha1_digest == digest => b }) match {
             case Some(blob) =>
               global_state >> (_.define_blob(digest))
               prover.get.define_blob(blob)
diff -r 8eb6c740ec1a -r e0f20a44ff9d src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Feb 11 15:55:05 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Feb 11 17:44:29 2014 +0100
@@ -264,11 +264,16 @@
       doc_blobs: Document.Blobs)
     : List[Command.Blob] =
   {
-    span_files(syntax, span).map(file =>
+    span_files(syntax, span).map(file_name =>
       Exn.capture {
         val name =
-          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
-        (name, doc_blobs.get(name).map(_.sha1_digest))
+          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name)))
+        val blob =
+          doc_blobs.get(name) match {
+            case Some((bytes, file)) => Some((bytes.sha1_digest, file))
+            case None => None
+          }
+        (name, blob)
       }
     )
   }
diff -r 8eb6c740ec1a -r e0f20a44ff9d src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Feb 11 15:55:05 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Feb 11 17:44:29 2014 +0100
@@ -131,18 +131,19 @@
 
   /* blob */
 
-  private var _blob: Option[Bytes] = None  // owned by Swing thread
+  private var _blob: Option[(Bytes, Command.File)] = None  // owned by Swing thread
 
   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
 
-  def blob(): Bytes =
+  def blob(): (Bytes, Command.File) =
     Swing_Thread.require {
       _blob match {
-        case Some(b) => b
+        case Some(x) => x
         case None =>
           val b = PIDE.thy_load.file_content(buffer)
-          _blob = Some(b)
-          b
+          val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
+          _blob = Some((b, file))
+          (b, file)
       }
     }