# HG changeset patch
# User wenzelm
# Date 1384813575 -3600
# Node ID 5545aff878b17070fab853c13068d4aad632fd68
# Parent  7a92ed889da418b8d6893b056d0ab5227df98244
inline blobs into command, via SHA1 digest;
broadcast all blobs within edit, without storing the result;

diff -r 7a92ed889da4 -r 5545aff878b1 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon Nov 18 22:06:08 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Mon Nov 18 23:26:15 2013 +0100
@@ -58,11 +58,11 @@
 
   def thy_load(span: List[Token]): Option[List[String]] =
     keywords.get(Command.name(span)) match {
-      case Some((Keyword.THY_LOAD, files)) => Some(files)
+      case Some((Keyword.THY_LOAD, exts)) => Some(exts)
       case _ => None
     }
 
-  def thy_load_commands: List[(String, List[String])] =
+  val thy_load_commands: List[(String, List[String])] =
     (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
 
   def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
diff -r 7a92ed889da4 -r 5545aff878b1 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Nov 18 22:06:08 2013 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Nov 18 23:26:15 2013 +0100
@@ -144,11 +144,13 @@
   def name(span: List[Token]): String =
     span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
+  type Blobs = List[(Document.Node.Name, Option[SHA1.Digest])]
+
   def apply(
     id: Document_ID.Command,
     node_name: Document.Node.Name,
     span: List[Token],
-    thy_load: Option[List[String]],
+    blobs: Blobs,
     results: Results = Results.empty,
     markup: Markup_Tree = Markup_Tree.empty): Command =
   {
@@ -167,14 +169,14 @@
       i += n
     }
 
-    new Command(id, node_name, span1.toList, source, thy_load, results, markup)
+    new Command(id, node_name, span1.toList, source, blobs, results, markup)
   }
 
-  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, None)
+  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
 
   def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
       : Command =
-    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), None,
+    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), Nil,
       results, markup)
 
   def unparsed(source: String): Command =
@@ -215,7 +217,7 @@
     val node_name: Document.Node.Name,
     val span: List[Token],
     val source: String,
-    val thy_load: Option[List[String]],
+    val blobs: Command.Blobs,
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
 {
diff -r 7a92ed889da4 -r 5545aff878b1 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Nov 18 22:06:08 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Nov 18 23:26:15 2013 +0100
@@ -154,7 +154,7 @@
     final class Commands private(val commands: Linear_Set[Command])
     {
       lazy val thy_load_commands: List[Command] =
-        commands.iterator.filter(_.thy_load.isDefined).toList
+        commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
 
       private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
       {
@@ -189,31 +189,27 @@
     val header: Node.Header = Node.bad_header("Bad theory header"),
     val perspective: Node.Perspective_Command =
       Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
-    val blob: Bytes = Bytes.empty,
     _commands: Node.Commands = Node.Commands.empty)
   {
     def clear: Node = new Node(header = header)
 
     def update_header(new_header: Node.Header): Node =
-      new Node(new_header, perspective, blob, _commands)
+      new Node(new_header, perspective, _commands)
 
     def update_perspective(new_perspective: Node.Perspective_Command): Node =
-      new Node(header, new_perspective, blob, _commands)
+      new Node(header, new_perspective, _commands)
 
     def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
       perspective.overlays == other_perspective.overlays
 
-    def update_blob(new_blob: Bytes): Node =
-      new Node(header, perspective, new_blob, _commands)
-
     def commands: Linear_Set[Command] = _commands.commands
     def thy_load_commands: List[Command] = _commands.thy_load_commands
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
-      else new Node(header, perspective, blob, Node.Commands(new_commands))
+      else new Node(header, perspective, Node.Commands(new_commands))
 
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.range(i)
diff -r 7a92ed889da4 -r 5545aff878b1 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Mon Nov 18 22:06:08 2013 +0100
+++ b/src/Pure/Thy/thy_load.scala	Mon Nov 18 23:26:15 2013 +0100
@@ -56,39 +56,13 @@
 
   /* theory files */
 
-  private def find_file(tokens: List[Token]): Option[String] =
-  {
-    def clean(toks: List[Token]): List[Token] =
-      toks match {
-        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
-        case t :: ts => t :: clean(ts)
-        case Nil => Nil
-      }
-    val clean_tokens = clean(tokens.filter(_.is_proper))
-    clean_tokens.reverse.find(_.is_name).map(_.content)
-  }
-
   def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
     syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
 
   def body_files(syntax: Outer_Syntax, text: String): List[String] =
   {
-    val thy_load_commands = syntax.thy_load_commands
     val spans = Thy_Syntax.parse_spans(syntax.scan(text))
-    spans.iterator.map({
-      case toks @ (tok :: _) if tok.is_command =>
-        thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
-          case Some((_, exts)) =>
-            find_file(toks) match {
-              case Some(file) =>
-                if (exts.isEmpty) List(file)
-                else exts.map(ext => file + "." + ext)
-              case None => Nil
-            }
-          case None => Nil
-        }
-      case _ => Nil
-    }).flatten.toList
+    spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
   }
 
   def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
diff -r 7a92ed889da4 -r 5545aff878b1 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 22:06:08 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 23:26:15 2013 +0100
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document_ID.none, node_name, span, syntax.thy_load(span))))
+      spans.foreach(span => add(Command(Document_ID.none, node_name, span, Nil)))
       result()
     }
   }
@@ -225,23 +225,69 @@
   }
 
 
+  /* inlined files */
+
+  private def find_file(tokens: List[Token]): Option[String] =
+  {
+    def clean(toks: List[Token]): List[Token] =
+      toks match {
+        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
+        case t :: ts => t :: clean(ts)
+        case Nil => Nil
+      }
+    val clean_tokens = clean(tokens.filter(_.is_proper))
+    clean_tokens.reverse.find(_.is_name).map(_.content)
+  }
+
+  def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
+    syntax.thy_load(span) match {
+      case Some(exts) =>
+        find_file(span) match {
+          case Some(file) =>
+            if (exts.isEmpty) List(file)
+            else exts.map(ext => file + "." + ext)
+          case None => Nil
+        }
+      case None => Nil
+    }
+
+  def resolve_files(
+      syntax: Outer_Syntax,
+      all_blobs: Map[Document.Node.Name, Bytes],
+      name: Document.Node.Name,
+      span: List[Token]): Command.Blobs =
+  {
+    val files = span_files(syntax, span)
+    files.map(file => {
+      // FIXME proper thy_load append
+      val file_name = Document.Node.Name(name.dir + file, name.dir, "")
+      (file_name, all_blobs.get(file_name).map(_.sha1_digest))
+    })
+  }
+
+
   /* reparse range of command spans */
 
   @tailrec private def chop_common(
-      cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
+      cmds: List[Command], spans: List[(List[Token], Command.Blobs)])
+      : (List[Command], List[(List[Token], Command.Blobs)]) =
     (cmds, spans) match {
-      case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
+      case (c :: cs, (span, blobs) :: ps) if c.span == span && c.blobs == blobs =>
+        chop_common(cs, ps)
       case _ => (cmds, spans)
     }
 
   private def reparse_spans(
     syntax: Outer_Syntax,
+    all_blobs: Map[Document.Node.Name, Bytes],
     name: Document.Node.Name,
     commands: Linear_Set[Command],
     first: Command, last: Command): Linear_Set[Command] =
   {
     val cmds0 = commands.iterator(first, last).toList
-    val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
+    val spans0 =
+      parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
+        map(span => (span, resolve_files(syntax, all_blobs, name, span)))
 
     val (cmds1, spans1) = chop_common(cmds0, spans0)
 
@@ -256,7 +302,7 @@
       case cmd :: _ =>
         val hook = commands.prev(cmd)
         val inserted =
-          spans2.map(span => Command(Document_ID.make(), name, span, syntax.thy_load(span)))
+          spans2.map({ case (span, blobs) => Command(Document_ID.make(), name, span, blobs) })
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }
@@ -267,6 +313,7 @@
   // FIXME somewhat slow
   private def recover_spans(
     syntax: Outer_Syntax,
+    all_blobs: Map[Document.Node.Name, Bytes],
     name: Document.Node.Name,
     perspective: Command.Perspective,
     commands: Linear_Set[Command]): Linear_Set[Command] =
@@ -282,7 +329,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(syntax, name, cmds, first, last))
+          recover(reparse_spans(syntax, all_blobs, name, cmds, first, last))
         case None => cmds
       }
     recover(commands)
@@ -293,6 +340,7 @@
 
   private def consolidate_spans(
     syntax: Outer_Syntax,
+    all_blobs: Map[Document.Node.Name, Bytes],
     reparse_limit: Int,
     name: Document.Node.Name,
     perspective: Command.Perspective,
@@ -312,7 +360,7 @@
                 last = it.next
                 i += last.length
               }
-              reparse_spans(syntax, name, commands, first_unfinished, last)
+              reparse_spans(syntax, all_blobs, name, commands, first_unfinished, last)
             case None => commands
           }
         case None => commands
@@ -333,7 +381,10 @@
     inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   }
 
-  private def text_edit(syntax: Outer_Syntax, reparse_limit: Int,
+  private def text_edit(
+    syntax: Outer_Syntax,
+    all_blobs: Map[Document.Node.Name, Bytes],
+    reparse_limit: Int,
     node: Document.Node, edit: Document.Edit_Text): Document.Node =
   {
     edit match {
@@ -342,7 +393,7 @@
       case (name, Document.Node.Edits(text_edits)) =>
         val commands0 = node.commands
         val commands1 = edit_text(text_edits, commands0)
-        val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1)
+        val commands2 = recover_spans(syntax, all_blobs, name, node.perspective.visible, commands1)
         node.update_commands(commands2)
 
       case (_, Document.Node.Deps(_)) => node
@@ -354,9 +405,9 @@
         if (node.same_perspective(perspective)) node
         else
           node.update_perspective(perspective).update_commands(
-            consolidate_spans(syntax, reparse_limit, name, visible, node.commands))
+            consolidate_spans(syntax, all_blobs, reparse_limit, name, visible, node.commands))
 
-      case (_, Document.Node.Blob(blob)) => node.update_blob(blob)
+      case (_, Document.Node.Blob(_)) => node
     }
   }
 
@@ -377,6 +428,14 @@
       (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
         .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
 
+    val all_blobs: Map[Document.Node.Name, Bytes] =
+      (Map.empty[Document.Node.Name, Bytes] /: node_edits) {
+        case (bs1, (_, es)) => (bs1 /: es) {
+          case (bs, (name, Document.Node.Blob(blob))) => bs + (name -> blob)
+          case (bs, _) => bs
+        }
+      }
+
     node_edits foreach {
       case (name, edits) =>
         val node = nodes(name)
@@ -384,9 +443,10 @@
 
         val node1 =
           if (reparse_set(name) && !commands.isEmpty)
-            node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
+            node.update_commands(
+              reparse_spans(syntax, all_blobs, name, commands, commands.head, commands.last))
           else node
-        val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
+        val node2 = (node1 /: edits)(text_edit(syntax, all_blobs, reparse_limit, _, _))
 
         if (!(node.same_perspective(node2.perspective)))
           doc_edits += (name -> node2.perspective)
diff -r 7a92ed889da4 -r 5545aff878b1 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Nov 18 22:06:08 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Nov 18 23:26:15 2013 +0100
@@ -190,7 +190,7 @@
       val clear = pending_clear
       val edits = snapshot()
       val perspective = node_perspective()
-      if (clear || !edits.isEmpty || last_perspective != perspective) {
+      if (!is_theory || clear || !edits.isEmpty || last_perspective != perspective) {
         pending_clear = false
         pending.clear
         last_perspective = perspective