1.1 --- a/src/Pure/Isar/token.ML	Tue Nov 19 13:54:02 2013 +0100
     1.2 +++ b/src/Pure/Isar/token.ML	Tue Nov 19 19:33:27 2013 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4    val content_of: T -> string
     1.5    val unparse: T -> string
     1.6    val text_of: T -> string * string
     1.7 -  val get_files: T -> file list option
     1.8 +  val get_files: T -> file list
     1.9    val put_files: file list -> T -> T
    1.10    val get_value: T -> value option
    1.11    val map_value: (value -> value) -> T -> T
    1.12 @@ -244,10 +244,11 @@
    1.13  
    1.14  (* inlined file content *)
    1.15  
    1.16 -fun get_files (Token (_, _, Value (SOME (Files files)))) = SOME files
    1.17 -  | get_files _ = NONE;
    1.18 +fun get_files (Token (_, _, Value (SOME (Files files)))) = files
    1.19 +  | get_files _ = [];
    1.20  
    1.21 -fun put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
    1.22 +fun put_files [] tok = tok
    1.23 +  | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
    1.24    | put_files _ tok =
    1.25        raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok));
    1.26  

     2.1 --- a/src/Pure/PIDE/command.ML	Tue Nov 19 13:54:02 2013 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Tue Nov 19 19:33:27 2013 +0100
     2.3 @@ -6,13 +6,14 @@
     2.4  
     2.5  signature COMMAND =
     2.6  sig
     2.7 -  val read: (unit -> theory) -> Token.T list -> Toplevel.transition
     2.8 +  type blob = (string * string) Exn.result
     2.9 +  val read: (unit -> theory) -> blob list -> Token.T list -> Toplevel.transition
    2.10    type eval
    2.11    val eval_eq: eval * eval -> bool
    2.12    val eval_running: eval -> bool
    2.13    val eval_finished: eval -> bool
    2.14    val eval_result_state: eval -> Toplevel.state
    2.15 -  val eval: (unit -> theory) -> Token.T list -> eval -> eval
    2.16 +  val eval: (unit -> theory) -> blob list -> Token.T list -> eval -> eval
    2.17    type print
    2.18    val print: bool -> (string * string list) list -> string ->
    2.19      eval -> print list -> print list option
    2.20 @@ -82,7 +83,19 @@
    2.21  
    2.22  (* read *)
    2.23  
    2.24 -fun read init span =
    2.25 +type blob = (string * string) Exn.result;  (*file node name, digest or text*)
    2.26 +
    2.27 +fun resolve_files blobs toks =
    2.28 +  (case Thy_Syntax.parse_spans toks of
    2.29 +    [span] => span
    2.30 +      |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
    2.31 +        blobs |> map (Exn.release #> (fn (file, text) =>
    2.32 +          let val _ = Position.report pos (Markup.path file);
    2.33 +          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end)))
    2.34 +      |> Thy_Syntax.span_content
    2.35 +  | _ => toks);
    2.36 +
    2.37 +fun read init blobs span =
    2.38    let
    2.39      val outer_syntax = #2 (Outer_Syntax.get_syntax ());
    2.40      val command_reports = Outer_Syntax.command_reports outer_syntax;
    2.41 @@ -99,7 +112,7 @@
    2.42    in
    2.43      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    2.44      else
    2.45 -      (case Outer_Syntax.read_spans outer_syntax span of
    2.46 +      (case Outer_Syntax.read_spans outer_syntax (resolve_files blobs span) of
    2.47          [tr] =>
    2.48            if Keyword.is_control (Toplevel.name_of tr) then
    2.49              Toplevel.malformed pos "Illegal control command"
    2.50 @@ -180,14 +193,14 @@
    2.51  
    2.52  in
    2.53  
    2.54 -fun eval init span eval0 =
    2.55 +fun eval init blobs span eval0 =
    2.56    let
    2.57      val exec_id = Document_ID.make ();
    2.58      fun process () =
    2.59        let
    2.60          val tr =
    2.61            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
    2.62 -            (fn () => read init span |> Toplevel.exec_id exec_id) ();
    2.63 +            (fn () => read init blobs span |> Toplevel.exec_id exec_id) ();
    2.64        in eval_state span tr (eval_result eval0) end;
    2.65    in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
    2.66  

     3.1 --- a/src/Pure/PIDE/command.scala	Tue Nov 19 13:54:02 2013 +0100
     3.2 +++ b/src/Pure/PIDE/command.scala	Tue Nov 19 19:33:27 2013 +0100
     3.3 @@ -144,13 +144,13 @@
     3.4    def name(span: List[Token]): String =
     3.5      span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
     3.6  
     3.7 -  type Blobs = List[Exn.Result[(Document.Node.Name, SHA1.Digest)]]
     3.8 +  type Blob = Exn.Result[(Document.Node.Name, SHA1.Digest)]
     3.9  
    3.10    def apply(
    3.11      id: Document_ID.Command,
    3.12      node_name: Document.Node.Name,
    3.13 +    blobs: List[Blob],
    3.14      span: List[Token],
    3.15 -    blobs: Blobs,
    3.16      results: Results = Results.empty,
    3.17      markup: Markup_Tree = Markup_Tree.empty): Command =
    3.18    {
    3.19 @@ -169,14 +169,14 @@
    3.20        i += n
    3.21      }
    3.22  
    3.23 -    new Command(id, node_name, span1.toList, source, blobs, results, markup)
    3.24 +    new Command(id, node_name, blobs, span1.toList, source, results, markup)
    3.25    }
    3.26  
    3.27    val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
    3.28  
    3.29    def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
    3.30        : Command =
    3.31 -    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), Nil,
    3.32 +    Command(id, Document.Node.Name.empty, Nil, List(Token(Token.Kind.UNPARSED, source)),
    3.33        results, markup)
    3.34  
    3.35    def unparsed(source: String): Command =
    3.36 @@ -215,9 +215,9 @@
    3.37  final class Command private(
    3.38      val id: Document_ID.Command,
    3.39      val node_name: Document.Node.Name,
    3.40 +    val blobs: List[Command.Blob],
    3.41      val span: List[Token],
    3.42      val source: String,
    3.43 -    val blobs: Command.Blobs,
    3.44      val init_results: Command.Results,
    3.45      val init_markup: Markup_Tree)
    3.46  {
    3.47 @@ -237,6 +237,12 @@
    3.48      id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
    3.49  
    3.50  
    3.51 +  /* blobs */
    3.52 +
    3.53 +  def blobs_digests: List[SHA1.Digest] =
    3.54 +    for (Exn.Res((_, digest)) <- blobs) yield digest
    3.55 +
    3.56 +
    3.57    /* source */
    3.58  
    3.59    def length: Int = source.length

     4.1 --- a/src/Pure/PIDE/document.ML	Tue Nov 19 13:54:02 2013 +0100
     4.2 +++ b/src/Pure/PIDE/document.ML	Tue Nov 19 19:33:27 2013 +0100
     4.3 @@ -18,7 +18,9 @@
     4.4    type edit = string * node_edit
     4.5    type state
     4.6    val init_state: state
     4.7 -  val define_command: Document_ID.command -> string -> string -> state -> state
     4.8 +  val define_blob: string -> string -> state -> state
     4.9 +  val define_command: Document_ID.command -> string -> Command.blob list -> string ->
    4.10 +    state -> state
    4.11    val remove_versions: Document_ID.version list -> state -> state
    4.12    val start_execution: state -> state
    4.13    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    4.14 @@ -231,29 +233,32 @@
    4.15  
    4.16  abstype state = State of
    4.17   {versions: version Inttab.table,  (*version id -> document content*)
    4.18 -  commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named command span*)
    4.19 +  blobs: string Symtab.table,  (*digest -> text*)
    4.20 +  commands: (string * Command.blob list * Token.T list lazy) Inttab.table,
    4.21 +    (*command id -> name, inlined files, command span*)
    4.22    execution: execution}  (*current execution process*)
    4.23  with
    4.24  
    4.25 -fun make_state (versions, commands, execution) =
    4.26 -  State {versions = versions, commands = commands, execution = execution};
    4.27 +fun make_state (versions, blobs, commands, execution) =
    4.28 +  State {versions = versions, blobs = blobs, commands = commands, execution = execution};
    4.29  
    4.30 -fun map_state f (State {versions, commands, execution}) =
    4.31 -  make_state (f (versions, commands, execution));
    4.32 +fun map_state f (State {versions, blobs, commands, execution}) =
    4.33 +  make_state (f (versions, blobs, commands, execution));
    4.34  
    4.35  val init_state =
    4.36 -  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
    4.37 +  make_state (Inttab.make [(Document_ID.none, empty_version)],
    4.38 +    Symtab.empty, Inttab.empty, no_execution);
    4.39  
    4.40  
    4.41  (* document versions *)
    4.42  
    4.43  fun define_version version_id version =
    4.44 -  map_state (fn (versions, commands, {delay_request, frontier, ...}) =>
    4.45 +  map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) =>
    4.46      let
    4.47        val versions' = Inttab.update_new (version_id, version) versions
    4.48          handle Inttab.DUP dup => err_dup "document version" dup;
    4.49        val execution' = new_execution version_id delay_request frontier;
    4.50 -    in (versions', commands, execution') end);
    4.51 +    in (versions', blobs, commands, execution') end);
    4.52  
    4.53  fun the_version (State {versions, ...}) version_id =
    4.54    (case Inttab.lookup versions version_id of
    4.55 @@ -265,10 +270,23 @@
    4.56      handle Inttab.UNDEF _ => err_undef "document version" version_id;
    4.57  
    4.58  
    4.59 +(* inlined files *)
    4.60 +
    4.61 +fun define_blob digest text =
    4.62 +  map_state (fn (versions, blobs, commands, execution) =>
    4.63 +    let val blobs' = Symtab.update (digest, text) blobs
    4.64 +    in (versions, blobs', commands, execution) end);
    4.65 +
    4.66 +fun the_blob (State {blobs, ...}) digest =
    4.67 +  (case Symtab.lookup blobs digest of
    4.68 +    NONE => error ("Undefined blob: " ^ digest)
    4.69 +  | SOME text => text);
    4.70 +
    4.71 +
    4.72  (* commands *)
    4.73  
    4.74 -fun define_command command_id name text =
    4.75 -  map_state (fn (versions, commands, execution) =>
    4.76 +fun define_command command_id name command_blobs text =
    4.77 +  map_state (fn (versions, blobs, commands, execution) =>
    4.78      let
    4.79        val id = Document_ID.print command_id;
    4.80        val span =
    4.81 @@ -279,9 +297,9 @@
    4.82          Position.setmp_thread_data (Position.id_only id)
    4.83            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    4.84        val commands' =
    4.85 -        Inttab.update_new (command_id, (name, span)) commands
    4.86 +        Inttab.update_new (command_id, (name, command_blobs, span)) commands
    4.87            handle Inttab.DUP dup => err_dup "command" dup;
    4.88 -    in (versions, commands', execution) end);
    4.89 +    in (versions, blobs, commands', execution) end);
    4.90  
    4.91  fun the_command (State {commands, ...}) command_id =
    4.92    (case Inttab.lookup commands command_id of
    4.93 @@ -295,7 +313,7 @@
    4.94  
    4.95  (* remove_versions *)
    4.96  
    4.97 -fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
    4.98 +fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) =>
    4.99    let
   4.100      val _ =
   4.101        member (op =) version_ids (#version_id execution) andalso
   4.102 @@ -308,12 +326,17 @@
   4.103            String_Graph.fold (fn (_, (node, _)) => node |>
   4.104              iterate_entries (fn ((_, command_id), _) =>
   4.105                SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
   4.106 -  in (versions', commands', execution) end);
   4.107 +    val blobs' =
   4.108 +      (commands', Symtab.empty) |->
   4.109 +        Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
   4.110 +          fold (fn Exn.Res (_, digest) => Symtab.update (digest, the_blob state digest) | _ => I));
   4.111 +
   4.112 +  in (versions', blobs', commands', execution) end);
   4.113  
   4.114  
   4.115  (* document execution *)
   4.116  
   4.117 -fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
   4.118 +fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
   4.119    timeit "Document.start_execution" (fn () =>
   4.120      let
   4.121        val {version_id, execution_id, delay_request, frontier} = execution;
   4.122 @@ -350,7 +373,7 @@
   4.123        val execution' =
   4.124          {version_id = version_id, execution_id = execution_id,
   4.125           delay_request = delay_request', frontier = frontier'};
   4.126 -    in (versions, commands, execution') end));
   4.127 +    in (versions, blobs, commands, execution') end));
   4.128  
   4.129  
   4.130  
   4.131 @@ -476,9 +499,12 @@
   4.132  
   4.133        val command_visible = visible_command node command_id';
   4.134        val command_overlays = overlays node command_id';
   4.135 -      val (command_name, span) = the_command state command_id' ||> Lazy.force;
   4.136 +      val (command_name, blobs0, span0) = the_command state command_id';
   4.137 +      val blobs = map (Exn.map_result (apsnd (the_blob state))) blobs0;
   4.138 +      val span = Lazy.force span0;
   4.139  
   4.140 -      val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
   4.141 +      val eval' =
   4.142 +        Command.eval (fn () => the_default illegal_init init span) blobs span eval;
   4.143        val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
   4.144        val exec' = (eval', prints');
   4.145  

     5.1 --- a/src/Pure/PIDE/document.scala	Tue Nov 19 13:54:02 2013 +0100
     5.2 +++ b/src/Pure/PIDE/document.scala	Tue Nov 19 19:33:27 2013 +0100
     5.3 @@ -397,6 +397,7 @@
     5.4  
     5.5    final case class State private(
     5.6      val versions: Map[Document_ID.Version, Version] = Map.empty,
     5.7 +    val blobs: Set[SHA1.Digest] = Set.empty,   // inlined files
     5.8      val commands: Map[Document_ID.Command, Command.State] = Map.empty,  // static markup from define_command
     5.9      val execs: Map[Document_ID.Exec, Command.State] = Map.empty,  // dynamic markup from execution
    5.10      val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
    5.11 @@ -411,6 +412,9 @@
    5.12          assignments = assignments + (id -> assignment.unfinished))
    5.13      }
    5.14  
    5.15 +    def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest)
    5.16 +    def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest)
    5.17 +
    5.18      def define_command(command: Command): State =
    5.19      {
    5.20        val id = command.id
    5.21 @@ -514,6 +518,7 @@
    5.22      {
    5.23        val versions1 = versions -- removed
    5.24        val assignments1 = assignments -- removed
    5.25 +      var blobs1 = Set.empty[SHA1.Digest]
    5.26        var commands1 = Map.empty[Document_ID.Command, Command.State]
    5.27        var execs1 = Map.empty[Document_ID.Exec, Command.State]
    5.28        for {
    5.29 @@ -522,14 +527,19 @@
    5.30          (_, node) <- version.nodes.entries
    5.31          command <- node.commands.iterator
    5.32        } {
    5.33 +        for (digest <- command.blobs_digests; if !blobs1.contains(digest))
    5.34 +          blobs1 += digest
    5.35 +
    5.36          if (!commands1.isDefinedAt(command.id))
    5.37            commands.get(command.id).foreach(st => commands1 += (command.id -> st))
    5.38 +
    5.39          for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
    5.40            if (!execs1.isDefinedAt(exec_id))
    5.41              execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
    5.42          }
    5.43        }
    5.44 -      copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
    5.45 +      copy(versions = versions1, blobs = blobs1, commands = commands1, execs = execs1,
    5.46 +        assignments = assignments1)
    5.47      }
    5.48  
    5.49      def command_state(version: Version, command: Command): Command.State =

     6.1 --- a/src/Pure/PIDE/protocol.ML	Tue Nov 19 13:54:02 2013 +0100
     6.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Nov 19 19:33:27 2013 +0100
     6.3 @@ -23,9 +23,23 @@
     6.4        end);
     6.5  
     6.6  val _ =
     6.7 +  Isabelle_Process.protocol_command "Document.define_blob"
     6.8 +    (fn [digest, content] => Document.change_state (Document.define_blob digest content));
     6.9 +
    6.10 +val _ =
    6.11    Isabelle_Process.protocol_command "Document.define_command"
    6.12 -    (fn [id, name, text] =>
    6.13 -      Document.change_state (Document.define_command (Document_ID.parse id) name text));
    6.14 +    (fn [id, name, blobs_yxml, text] =>
    6.15 +      let
    6.16 +        val blobs =
    6.17 +          YXML.parse_body blobs_yxml |>
    6.18 +            let open XML.Decode in
    6.19 +              list (variant
    6.20 +               [fn ([a, b], []) => Exn.Res (a, b),
    6.21 +                fn ([a], []) => Exn.Exn (ERROR a)])
    6.22 +            end;
    6.23 +      in
    6.24 +        Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
    6.25 +      end);
    6.26  
    6.27  val _ =
    6.28    Isabelle_Process.protocol_command "Document.discontinue_execution"

     7.1 --- a/src/Pure/PIDE/protocol.scala	Tue Nov 19 13:54:02 2013 +0100
     7.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Nov 19 19:33:27 2013 +0100
     7.3 @@ -308,11 +308,27 @@
     7.4  
     7.5  trait Protocol extends Isabelle_Process
     7.6  {
     7.7 +  /* inlined files */
     7.8 +
     7.9 +  def define_blob(blob: Bytes): Unit =
    7.10 +    protocol_command_raw("Document.define_blob", Bytes(blob.sha1_digest.toString), blob)
    7.11 +
    7.12 +
    7.13    /* commands */
    7.14  
    7.15    def define_command(command: Command): Unit =
    7.16 +  {
    7.17 +    val blobs_yxml =
    7.18 +    { import XML.Encode._
    7.19 +      val encode_blob: T[Command.Blob] =
    7.20 +        variant(List(
    7.21 +          { case Exn.Res((a, b)) => (List(a.node, b.toString), Nil) },
    7.22 +          { case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
    7.23 +      YXML.string_of_body(list(encode_blob)(command.blobs))
    7.24 +    }
    7.25      protocol_command("Document.define_command",
    7.26 -      Document_ID(command.id), encode(command.name), encode(command.source))
    7.27 +      Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
    7.28 +  }
    7.29  
    7.30  
    7.31    /* execution */

     8.1 --- a/src/Pure/System/session.scala	Tue Nov 19 13:54:02 2013 +0100
     8.2 +++ b/src/Pure/System/session.scala	Tue Nov 19 19:33:27 2013 +0100
     8.3 @@ -179,12 +179,12 @@
     8.4  
     8.5          case Text_Edits(previous, text_edits, version_result) =>
     8.6            val prev = previous.get_finished
     8.7 -          val (doc_edits, version) =
     8.8 +          val (all_blobs, doc_edits, version) =
     8.9              Timing.timeit("Thy_Load.text_edits", timing) {
    8.10                thy_load.text_edits(reparse_limit, prev, text_edits)
    8.11              }
    8.12            version_result.fulfill(version)
    8.13 -          sender ! Change(doc_edits, prev, version)
    8.14 +          sender ! Change(all_blobs, doc_edits, prev, version)
    8.15  
    8.16          case bad => System.err.println("change_parser: ignoring bad message " + bad)
    8.17        }
    8.18 @@ -250,6 +250,7 @@
    8.19    private case class Start(args: List[String])
    8.20    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    8.21    private case class Change(
    8.22 +    all_blobs: Map[Document.Node.Name, Bytes],
    8.23      doc_edits: List[Document.Edit_Command],
    8.24      previous: Document.Version,
    8.25      version: Document.Version)
    8.26 @@ -374,6 +375,18 @@
    8.27  
    8.28        def id_command(command: Command)
    8.29        {
    8.30 +        for {
    8.31 +          digest <- command.blobs_digests
    8.32 +          if !global_state().defined_blob(digest)
    8.33 +        } {
    8.34 +          change.all_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
    8.35 +            case Some(blob) =>
    8.36 +              global_state >> (_.define_blob(digest))
    8.37 +              prover.get.define_blob(blob)
    8.38 +            case None => System.err.println("Missing blob for SHA1 digest " + digest)
    8.39 +          }
    8.40 +        }
    8.41 +
    8.42          if (!global_state().defined_command(command.id)) {
    8.43            global_state >> (_.define_command(command))
    8.44            prover.get.define_command(command)

     9.1 --- a/src/Pure/Thy/thy_load.ML	Tue Nov 19 13:54:02 2013 +0100
     9.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Nov 19 19:33:27 2013 +0100
     9.3 @@ -9,7 +9,6 @@
     9.4    val master_directory: theory -> Path.T
     9.5    val imports_of: theory -> (string * Position.T) list
     9.6    val thy_path: Path.T -> Path.T
     9.7 -  val read_files: Path.T -> string -> Path.T * Position.T -> Token.file list
     9.8    val parse_files: string -> (theory -> Token.file list) parser
     9.9    val check_thy: Path.T -> string ->
    9.10     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    9.11 @@ -76,8 +75,8 @@
    9.12  fun parse_files cmd =
    9.13    Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
    9.14      (case Token.get_files tok of
    9.15 -      SOME files => files
    9.16 -    | NONE => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)));
    9.17 +      [] => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)
    9.18 +    | files => files));
    9.19  
    9.20  
    9.21  (* theory files *)
    9.22 @@ -146,7 +145,7 @@
    9.23    let
    9.24      fun prepare_span span =
    9.25        Thy_Syntax.span_content span
    9.26 -      |> Command.read init
    9.27 +      |> Command.read init []
    9.28        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    9.29  
    9.30      fun element_result span_elem (st, _) =

    10.1 --- a/src/Pure/Thy/thy_load.scala	Tue Nov 19 13:54:02 2013 +0100
    10.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Nov 19 19:33:27 2013 +0100
    10.3 @@ -100,7 +100,7 @@
    10.4    /* theory text edits */
    10.5  
    10.6    def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
    10.7 -      : (List[Document.Edit_Command], Document.Version) =
    10.8 +      : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) =
    10.9      Thy_Syntax.text_edits(this, reparse_limit, previous, edits)
   10.10  }
   10.11  

    11.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 13:54:02 2013 +0100
    11.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 19:33:27 2013 +0100
    11.3 @@ -68,7 +68,7 @@
    11.4        /* result structure */
    11.5  
    11.6        val spans = parse_spans(syntax.scan(text))
    11.7 -      spans.foreach(span => add(Command(Document_ID.none, node_name, span, Nil)))
    11.8 +      spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
    11.9        result()
   11.10      }
   11.11    }
   11.12 @@ -257,7 +257,7 @@
   11.13        node_name: Document.Node.Name,
   11.14        span: List[Token],
   11.15        all_blobs: Map[Document.Node.Name, Bytes])
   11.16 -    : Command.Blobs =
   11.17 +    : List[Command.Blob] =
   11.18    {
   11.19      span_files(syntax, span).map(file =>
   11.20        Exn.capture {
   11.21 @@ -265,7 +265,7 @@
   11.22            Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
   11.23          all_blobs.get(name) match {
   11.24            case Some(blob) => (name, blob.sha1_digest)
   11.25 -          case None => error("Bad file: " + quote(name.toString))
   11.26 +          case None => error("No such file: " + quote(name.toString))
   11.27          }
   11.28        }
   11.29      )
   11.30 @@ -275,10 +275,10 @@
   11.31    /* reparse range of command spans */
   11.32  
   11.33    @tailrec private def chop_common(
   11.34 -      cmds: List[Command], spans: List[(List[Token], Command.Blobs)])
   11.35 -      : (List[Command], List[(List[Token], Command.Blobs)]) =
   11.36 +      cmds: List[Command], spans: List[(List[Command.Blob], List[Token])])
   11.37 +      : (List[Command], List[(List[Command.Blob], List[Token])]) =
   11.38      (cmds, spans) match {
   11.39 -      case (c :: cs, (span, blobs) :: ps) if c.span == span && c.blobs == blobs =>
   11.40 +      case (c :: cs, (blobs, span) :: ps) if c.blobs == blobs && c.span == span =>
   11.41          chop_common(cs, ps)
   11.42        case _ => (cmds, spans)
   11.43      }
   11.44 @@ -294,7 +294,7 @@
   11.45      val cmds0 = commands.iterator(first, last).toList
   11.46      val spans0 =
   11.47        parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
   11.48 -        map(span => (span, resolve_files(thy_load, syntax, name, span, all_blobs)))
   11.49 +        map(span => (resolve_files(thy_load, syntax, name, span, all_blobs), span))
   11.50  
   11.51      val (cmds1, spans1) = chop_common(cmds0, spans0)
   11.52  
   11.53 @@ -309,7 +309,7 @@
   11.54        case cmd :: _ =>
   11.55          val hook = commands.prev(cmd)
   11.56          val inserted =
   11.57 -          spans2.map({ case (span, blobs) => Command(Document_ID.make(), name, span, blobs) })
   11.58 +          spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
   11.59          (commands /: cmds2)(_ - _).append_after(hook, inserted)
   11.60      }
   11.61    }
   11.62 @@ -428,7 +428,7 @@
   11.63        reparse_limit: Int,
   11.64        previous: Document.Version,
   11.65        edits: List[Document.Edit_Text])
   11.66 -    : (List[Document.Edit_Command], Document.Version) =
   11.67 +    : (Map[Document.Node.Name, Bytes], List[Document.Edit_Command], Document.Version) =
   11.68    {
   11.69      val (syntax, reparse0, nodes0, doc_edits0) =
   11.70        header_edits(thy_load.base_syntax, previous, edits)
   11.71 @@ -477,6 +477,6 @@
   11.72          nodes += (name -> node2)
   11.73      }
   11.74  
   11.75 -    (doc_edits.toList, Document.Version.make(syntax, nodes))
   11.76 +    (all_blobs, doc_edits.toList, Document.Version.make(syntax, nodes))
   11.77    }
   11.78  }