# HG changeset patch
# User wenzelm
# Date 1396271124 -7200
# Node ID 8953d4cc060abd46f107114ae495fc5d525984e7
# Parent  6b3739fee456ed44af90988445bfbbf4649d4a04
store blob content within document node: aux. files that were once open are made persistent;
proper structural equality for Command.File and Symbol.Index;

diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 31 12:35:39 2014 +0200
+++ b/src/Pure/General/symbol.scala	Mon Mar 31 15:05:24 2014 +0200
@@ -165,6 +165,13 @@
       else index(i).chr + sym - index(i).sym
     }
     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
+
+    override def hashCode: Int = index.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Index => index.sameElements(other.index)
+        case _ => false
+      }
   }
 
 
diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Mar 31 12:35:39 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Mar 31 15:05:24 2014 +0200
@@ -225,6 +225,7 @@
     }
   }
 
+  // file name and position information, *without* persistent text
   class File(val file_name: String, text: CharSequence) extends Chunk
   {
     val length = text.length
@@ -232,6 +233,17 @@
     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 + ")"
   }
 
diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Mar 31 12:35:39 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Mar 31 15:05:24 2014 +0200
@@ -46,20 +46,25 @@
   /* document blobs: auxiliary files */
 
   sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
+  {
+    def unchanged: Blob = copy(changed = false)
+  }
 
   object Blobs
   {
-    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
+    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs, Nodes.empty)
     val empty: Blobs = apply(Map.empty)
   }
 
-  final class Blobs private(blobs: Map[Node.Name, Blob])
+  final class Blobs private(blobs: Map[Node.Name, Blob], default_nodes: Nodes)
   {
     private lazy val digests: Map[SHA1.Digest, Blob] =
       for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
 
     def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
-    def get(name: Node.Name): Option[Blob] = blobs.get(name)
+
+    def get(name: Node.Name): Option[Blob] =
+      blobs.get(name) orElse default_nodes(name).get_blob
 
     def changed(name: Node.Name): Boolean =
       get(name) match {
@@ -67,6 +72,8 @@
         case None => false
       }
 
+    def default(nodes: Nodes): Blobs = new Blobs(blobs, nodes)
+
     override def toString: String = blobs.mkString("Blobs(", ",", ")")
   }
 
@@ -157,7 +164,7 @@
       }
     }
     case class Clear[A, B]() extends Edit[A, B]
-    case class Blob[A, B]() extends Edit[A, B]
+    case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
 
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
@@ -222,7 +229,7 @@
   }
 
   final class Node private(
-    val is_blob: Boolean = false,
+    val get_blob: Option[Document.Blob] = None,
     val header: Node.Header = Node.bad_header("Bad theory header"),
     val perspective: Node.Perspective_Command =
       Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
@@ -230,13 +237,13 @@
   {
     def clear: Node = new Node(header = header)
 
-    def init_blob: Node = new Node(is_blob = true)
+    def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
 
     def update_header(new_header: Node.Header): Node =
-      new Node(is_blob, new_header, perspective, _commands)
+      new Node(get_blob, new_header, perspective, _commands)
 
     def update_perspective(new_perspective: Node.Perspective_Command): Node =
-      new Node(is_blob, header, new_perspective, _commands)
+      new Node(get_blob, header, new_perspective, _commands)
 
     def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
       perspective.required == other_perspective.required &&
@@ -248,7 +255,7 @@
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
-      else new Node(is_blob, header, perspective, Node.Commands(new_commands))
+      else new Node(get_blob, header, perspective, Node.Commands(new_commands))
 
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.range(i)
diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Mar 31 12:35:39 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Mar 31 15:05:24 2014 +0200
@@ -319,9 +319,8 @@
 {
   /* inlined files */
 
-  def define_blob(blob: Document.Blob): Unit =
-    protocol_command_raw(
-      "Document.define_blob", Bytes(blob.bytes.sha1_digest.toString), blob.bytes)
+  def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
+    protocol_command_raw("Document.define_blob", Bytes(digest.toString), bytes)
 
 
   /* commands */
diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Mar 31 12:35:39 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Mar 31 15:05:24 2014 +0200
@@ -384,7 +384,7 @@
           change.doc_blobs.get(digest) match {
             case Some(blob) =>
               global_state >> (_.define_blob(digest))
-              prover.get.define_blob(blob)
+              prover.get.define_blob(digest, blob.bytes)
             case None =>
               System.err.println("Missing blob for SHA1 digest " + digest)
           }
diff -r 6b3739fee456 -r 8953d4cc060a src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Mar 31 12:35:39 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Mar 31 15:05:24 2014 +0200
@@ -262,14 +262,14 @@
       syntax: Outer_Syntax,
       node_name: Document.Node.Name,
       span: List[Token],
-      doc_blobs: Document.Blobs)
+      doc_blobs_default: Document.Blobs)
     : List[Command.Blob] =
   {
     span_files(syntax, span).map(file_name =>
       Exn.capture {
         val name =
           Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
-        val blob = doc_blobs.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
+        val blob = doc_blobs_default.get(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
         (name, blob)
       })
   }
@@ -292,7 +292,7 @@
   private def reparse_spans(
     resources: Resources,
     syntax: Outer_Syntax,
-    doc_blobs: Document.Blobs,
+    doc_blobs_default: Document.Blobs,
     name: Document.Node.Name,
     commands: Linear_Set[Command],
     first: Command, last: Command): Linear_Set[Command] =
@@ -300,7 +300,7 @@
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
       parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
-        map(span => (resolve_files(resources, syntax, name, span, doc_blobs), span))
+        map(span => (resolve_files(resources, syntax, name, span, doc_blobs_default), span))
 
     val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
 
@@ -327,7 +327,7 @@
   private def recover_spans(
     resources: Resources,
     syntax: Outer_Syntax,
-    doc_blobs: Document.Blobs,
+    doc_blobs_default: Document.Blobs,
     name: Document.Node.Name,
     perspective: Command.Perspective,
     commands: Linear_Set[Command]): Linear_Set[Command] =
@@ -343,7 +343,7 @@
         case Some(first_unparsed) =>
           val first = next_invisible_command(cmds.reverse, first_unparsed)
           val last = next_invisible_command(cmds, first_unparsed)
-          recover(reparse_spans(resources, syntax, doc_blobs, name, cmds, first, last))
+          recover(reparse_spans(resources, syntax, doc_blobs_default, name, cmds, first, last))
         case None => cmds
       }
     recover(commands)
@@ -355,7 +355,7 @@
   private def consolidate_spans(
     resources: Resources,
     syntax: Outer_Syntax,
-    doc_blobs: Document.Blobs,
+    doc_blobs_default: Document.Blobs,
     reparse_limit: Int,
     name: Document.Node.Name,
     perspective: Command.Perspective,
@@ -375,7 +375,8 @@
                 last = it.next
                 i += last.length
               }
-              reparse_spans(resources, syntax, doc_blobs, name, commands, first_unfinished, last)
+              reparse_spans(
+                resources, syntax, doc_blobs_default, name, commands, first_unfinished, last)
             case None => commands
           }
         case None => commands
@@ -399,24 +400,25 @@
   private def text_edit(
     resources: Resources,
     syntax: Outer_Syntax,
-    doc_blobs: Document.Blobs,
+    doc_blobs_default: Document.Blobs,
     reparse_limit: Int,
     node: Document.Node, edit: Document.Edit_Text): Document.Node =
   {
     edit match {
       case (_, Document.Node.Clear()) => node.clear
 
-      case (_, Document.Node.Blob()) => node.init_blob
+      case (_, Document.Node.Blob(blob)) => node.init_blob(blob)
 
       case (name, Document.Node.Edits(text_edits)) =>
-        if (node.is_blob) node
-        else {
+        if (name.is_theory) {
           val commands0 = node.commands
           val commands1 = edit_text(text_edits, commands0)
           val commands2 =
-            recover_spans(resources, syntax, doc_blobs, name, node.perspective.visible, commands1)
+            recover_spans(
+              resources, syntax, doc_blobs_default, name, node.perspective.visible, commands1)
           node.update_commands(commands2)
         }
+        else node
 
       case (_, Document.Node.Deps(_)) => node
 
@@ -427,7 +429,7 @@
         if (node.same_perspective(perspective)) node
         else
           node.update_perspective(perspective).update_commands(
-            consolidate_spans(resources, syntax, doc_blobs, reparse_limit,
+            consolidate_spans(resources, syntax, doc_blobs_default, reparse_limit,
               name, visible, node.commands))
     }
   }
@@ -454,6 +456,8 @@
             })
         val reparse_set = reparse.toSet
 
+        val doc_blobs_default = doc_blobs.default(previous.nodes)
+
         var nodes = nodes0
         val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
 
@@ -469,11 +473,11 @@
             val node1 =
               if (reparse_set(name) && !commands.isEmpty)
                 node.update_commands(
-                  reparse_spans(resources, syntax, doc_blobs,
+                  reparse_spans(resources, syntax, doc_blobs_default,
                     name, commands, commands.head, commands.last))
               else node
             val node2 =
-              (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _))
+              (node1 /: edits)(text_edit(resources, syntax, doc_blobs_default, reparse_limit, _, _))
 
             if (!(node.same_perspective(node2.perspective)))
               doc_edits += (name -> node2.perspective)
diff -r 6b3739fee456 -r 8953d4cc060a src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Mar 31 12:35:39 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Mar 31 15:05:24 2014 +0200
@@ -164,28 +164,25 @@
   /* edits */
 
   def node_edits(
-    clear: Boolean,
-    text_edits: List[Text.Edit],
-    perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
-  {
-    Swing_Thread.require()
-
-    if (is_theory) {
-      val header_edit = session.header_edit(node_name, node_header())
-      if (clear)
-        List(header_edit,
-          node_name -> Document.Node.Clear(),
-          node_name -> Document.Node.Edits(text_edits),
-          node_name -> perspective)
-      else
-        List(header_edit,
-          node_name -> Document.Node.Edits(text_edits),
-          node_name -> perspective)
+      clear: Boolean,
+      text_edits: List[Text.Edit],
+      perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
+    get_blob() match {
+      case None =>
+        val header_edit = session.header_edit(node_name, node_header())
+        if (clear)
+          List(header_edit,
+            node_name -> Document.Node.Clear(),
+            node_name -> Document.Node.Edits(text_edits),
+            node_name -> perspective)
+        else
+          List(header_edit,
+            node_name -> Document.Node.Edits(text_edits),
+            node_name -> perspective)
+      case Some(blob) =>
+        List(node_name -> Document.Node.Blob(blob),
+          node_name -> Document.Node.Edits(text_edits))
     }
-    else
-      List(node_name -> Document.Node.Blob(),
-        node_name -> Document.Node.Edits(text_edits))
-  }
 
 
   /* pending edits */