simplified Command.resolve_files in ML, using blobs_index from Scala;
clarified modules;

--- a/src/Pure/PIDE/command.ML	Fri Mar 13 12:44:16 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Mar 13 12:58:49 2015 +0100
@@ -10,14 +10,14 @@
   val read_file: Path.T -> Position.T -> Path.T -> Token.file
   val read_thy: Toplevel.state -> theory
   val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) ->
-    blob list -> Token.T list -> Toplevel.transition
+    blob list * int -> Token.T list -> Toplevel.transition
   type eval
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
   val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
-    blob list -> Token.T list -> eval -> eval
+    blob list * int -> Token.T list -> eval -> eval
   type print
   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
@@ -78,26 +78,33 @@
       | SOME exec_id => Position.put_id exec_id);
   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
 
-fun resolve_files keywords master_dir blobs toks =
+fun resolve_files keywords master_dir (blobs, blobs_index) toks =
   (case Outer_Syntax.parse_spans toks of
-    [span] => span
-      |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) =>
-        let
-          fun make_file src_path (Exn.Res (file_node, NONE)) =
-                Exn.interruptible_capture (fn () =>
-                  read_file_node file_node master_dir pos src_path) ()
-            | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
-                Exn.Res (blob_file src_path lines digest file_node)
-            | make_file _ (Exn.Exn e) = Exn.Exn e;
-          val src_paths = Keyword.command_files keywords cmd path;
-        in
-          if null blobs then
-            map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
-          else if length src_paths = length blobs then
-            map2 make_file src_paths blobs
-          else error ("Misalignment of inlined files" ^ Position.here pos)
-        end)
-      |> Command_Span.content
+    [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] =>
+      (case try (nth toks) blobs_index of
+        SOME tok =>
+          let
+            val pos = Token.pos_of tok;
+            val path = Path.explode (Token.content_of tok)
+              handle ERROR msg => error (msg ^ Position.here pos);
+            fun make_file src_path (Exn.Res (file_node, NONE)) =
+                  Exn.interruptible_capture (fn () =>
+                    read_file_node file_node master_dir pos src_path) ()
+              | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
+                  Exn.Res (blob_file src_path lines digest file_node)
+              | make_file _ (Exn.Exn e) = Exn.Exn e;
+            val src_paths = Keyword.command_files keywords cmd path;
+            val files =
+              if null blobs then
+                map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
+              else if length src_paths = length blobs then
+                map2 make_file src_paths blobs
+              else error ("Misalignment of inlined files" ^ Position.here pos);
+          in
+            toks |> map_index (fn (i, tok) =>
+              if i = blobs_index then Token.put_files files tok else tok)
+          end
+      | NONE => toks)
   | _ => toks);
 
 val bootstrap_thy = ML_Context.the_global_context ();
@@ -106,7 +113,7 @@
 
 fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
 
-fun read keywords thy master_dir init blobs span =
+fun read keywords thy master_dir init blobs_info span =
   let
     val command_reports = Outer_Syntax.command_reports thy;
 
@@ -121,7 +128,7 @@
   in
     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     else
-      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs span) of
+      (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs_info span) of
         [tr] => Toplevel.modify_init init tr
       | [] => Toplevel.ignored (#1 (Token.range_of span))
       | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
@@ -218,7 +225,7 @@
 
 in
 
-fun eval keywords master_dir init blobs span eval0 =
+fun eval keywords master_dir init blobs_info span eval0 =
   let
     val exec_id = Document_ID.make ();
     fun process () =
@@ -227,7 +234,8 @@
         val thy = read_thy (#state eval_state0);
         val tr =
           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
-            (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
+            (fn () =>
+              read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) ();
       in eval_state keywords span tr eval_state0 end;
   in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
 

--- a/src/Pure/PIDE/command.scala	Fri Mar 13 12:44:16 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Mar 13 12:58:49 2015 +0100
@@ -307,6 +307,66 @@
         (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
     }
   }
+
+
+  /* resolve inlined files */
+
+  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
+  {
+    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
+      toks match {
+        case (t1, i1) :: (t2, i2) :: rest =>
+          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
+          else (t1, i1) :: clean((t2, i2) :: rest)
+        case _ => toks
+      }
+    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
+  }
+
+  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
+    tokens match {
+      case (tok, _) :: toks =>
+        if (tok.is_command)
+          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
+        else None
+      case Nil => None
+    }
+
+  def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
+    span.kind match {
+      case Command_Span.Command_Span(name, _) =>
+        syntax.load_command(name) match {
+          case Some(exts) =>
+            find_file(clean_tokens(span.content)) match {
+              case Some((file, i)) =>
+                if (exts.isEmpty) (List(file), i)
+                else (exts.map(ext => file + "." + ext), i)
+              case None => (Nil, -1)
+            }
+          case None => (Nil, -1)
+        }
+      case _ => (Nil, -1)
+    }
+
+  def resolve_files(
+      resources: Resources,
+      syntax: Prover.Syntax,
+      node_name: Document.Node.Name,
+      span: Command_Span.Span,
+      get_blob: Document.Node.Name => Option[Document.Blob])
+    : (List[Command.Blob], Int) =
+  {
+    val (files, index) = span_files(syntax, span)
+    val blobs =
+      files.map(file =>
+        Exn.capture {
+          val name =
+            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+          val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
+          (name, blob)
+        })
+    (blobs, index)
+  }
 }
 
 

--- a/src/Pure/PIDE/command_span.ML	Fri Mar 13 12:44:16 2015 +0100
+++ b/src/Pure/PIDE/command_span.ML	Fri Mar 13 12:58:49 2015 +0100
@@ -10,8 +10,6 @@
   datatype span = Span of kind * Token.T list
   val kind: span -> kind
   val content: span -> Token.T list
-  val resolve_files: Keyword.keywords ->
-    (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
 end;
 
 structure Command_Span: COMMAND_SPAN =
@@ -23,47 +21,4 @@
 fun kind (Span (k, _)) = k;
 fun content (Span (_, toks)) = toks;
 
-
-(* resolve inlined files *)
-
-local
-
-fun clean ((t1, i1) :: (t2, i2) :: rest) =
-      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean rest
-      else (t1, i1) :: clean ((t2, i2) :: rest)
-  | clean toks = toks;
-
-fun clean_tokens tokens =
-  clean (filter (fn (t, _) => Token.is_proper t) (tokens ~~ (0 upto length tokens - 1)));
-
-fun find_file ((tok, _) :: toks) =
-      if Token.is_command tok then
-        toks |> get_first (fn (t, i) =>
-          if Token.is_name t then
-            SOME ((Path.explode (Token.content_of t), Token.pos_of t), i)
-              handle ERROR msg => error (msg ^ Position.here (Token.pos_of t))
-          else NONE)
-      else NONE
-  | find_file [] = NONE;
-
-in
-
-fun resolve_files keywords read_files span =
-  (case span of
-    Span (Command_Span (cmd, pos), toks) =>
-      if Keyword.is_theory_load keywords cmd then
-        (case find_file (clean_tokens toks) of
-          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
-        | SOME (path, i) =>
-            let
-              val toks' = toks |> map_index (fn (j, tok) =>
-                if i = j then Token.put_files (read_files cmd path) tok
-                else tok);
-            in Span (Command_Span (cmd, pos), toks') end)
-      else span
-  | _ => span);
-
 end;
-
-end;
-

--- a/src/Pure/PIDE/command_span.scala	Fri Mar 13 12:44:16 2015 +0100
+++ b/src/Pure/PIDE/command_span.scala	Fri Mar 13 12:58:49 2015 +0100
@@ -52,64 +52,4 @@
 
   def unparsed(source: String): Span =
     Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
-
-
-  /* resolve inlined files */
-
-  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
-  {
-    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
-      toks match {
-        case (t1, i1) :: (t2, i2) :: rest =>
-          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
-          else (t1, i1) :: clean((t2, i2) :: rest)
-        case _ => toks
-      }
-    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
-  }
-
-  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
-    tokens match {
-      case (tok, _) :: toks =>
-        if (tok.is_command)
-          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
-        else None
-      case Nil => None
-    }
-
-  def span_files(syntax: Prover.Syntax, span: Span): (List[String], Int) =
-    span.kind match {
-      case Command_Span(name, _) =>
-        syntax.load_command(name) match {
-          case Some(exts) =>
-            find_file(clean_tokens(span.content)) match {
-              case Some((file, i)) =>
-                if (exts.isEmpty) (List(file), i)
-                else (exts.map(ext => file + "." + ext), i)
-              case None => (Nil, -1)
-            }
-          case None => (Nil, -1)
-        }
-      case _ => (Nil, -1)
-    }
-
-  def resolve_files(
-      resources: Resources,
-      syntax: Prover.Syntax,
-      node_name: Document.Node.Name,
-      span: Span,
-      get_blob: Document.Node.Name => Option[Document.Blob])
-    : (List[Command.Blob], Int) =
-  {
-    val (files, index) = span_files(syntax, span)
-    val blobs =
-      files.map(file =>
-        Exn.capture {
-          val name =
-            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
-          val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
-          (name, blob)
-        })
-    (blobs, index)
-  }
 }

--- a/src/Pure/PIDE/document.ML	Fri Mar 13 12:44:16 2015 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Mar 13 12:58:49 2015 +0100
@@ -307,8 +307,8 @@
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
   blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
-  commands: (string * blob_digest list * Token.T list lazy) Inttab.table,
-    (*command id -> name, inlined files, command span*)
+  commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table,
+    (*command id -> name, inlined files, token index of files, command span*)
   execution: execution}  (*current execution process*)
 with
 
@@ -385,7 +385,7 @@
                   else ();
               in tokens end) ());
       val commands' =
-        Inttab.update_new (command_id, (name, command_blobs, span)) commands
+        Inttab.update_new (command_id, (name, command_blobs, blobs_index, span)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
       val _ =
         Position.setmp_thread_data (Position.id_only id)
@@ -419,7 +419,7 @@
               SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
     val blobs' =
       (commands', Symtab.empty) |->
-        Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
+        Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |>
           fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
 
   in (versions', blobs', commands', execution) end);
@@ -585,13 +585,13 @@
 
       val command_visible = visible_command node command_id';
       val command_overlays = overlays node command_id';
-      val (command_name, blob_digests, span0) = the_command state command_id';
+      val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
       val blobs = map (resolve_blob state) blob_digests;
       val span = Lazy.force span0;
 
       val eval' =
         Command.eval keywords (master_directory node)
-          (fn () => the_default illegal_init init span) blobs span eval;
+          (fn () => the_default illegal_init init span) (blobs, blobs_index) span eval;
       val prints' =
         perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
       val exec' = (eval', prints');

--- a/src/Pure/PIDE/resources.ML	Fri Mar 13 12:44:16 2015 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Mar 13 12:58:49 2015 +0100
@@ -128,7 +128,7 @@
   let
     fun prepare_span st span =
       Command_Span.content span
-      |> Command.read keywords (Command.read_thy st) master_dir init []
+      |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
     fun element_result span_elem (st, _) =

--- a/src/Pure/PIDE/resources.scala	Fri Mar 13 12:44:16 2015 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Mar 13 12:58:49 2015 +0100
@@ -57,7 +57,7 @@
   def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
     if (syntax.load_commands_in(text)) {
       val spans = syntax.parse_spans(text)
-      spans.iterator.map(Command_Span.span_files(syntax, _)._1).flatten.toList
+      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
     }
     else Nil
 

--- a/src/Pure/Thy/thy_syntax.scala	Fri Mar 13 12:44:16 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Mar 13 12:58:49 2015 +0100
@@ -164,7 +164,7 @@
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
       syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
-        map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
+        map(span => (Command.resolve_files(resources, syntax, name, span, get_blob), span))
 
     val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)