more uniform handling of inlined files;

--- a/src/Pure/Isar/keyword.ML	Tue Nov 19 20:59:05 2013 +0100
+++ b/src/Pure/Isar/keyword.ML	Tue Nov 19 21:49:31 2013 +0100
@@ -51,7 +51,7 @@
   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   val is_keyword: string -> bool
   val command_keyword: string -> T option
-  val command_files: string -> string list
+  val command_files: string -> Path.T -> Path.T list
   val command_tags: string -> string list
   val dest: unit -> string list * string list
   val define: string * T option -> unit
@@ -196,7 +196,15 @@
   in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
 
 fun command_keyword name = Symtab.lookup (get_commands ()) name;
-val command_files = these o Option.map (#2 o kind_files_of) o command_keyword;
+
+fun command_files name path =
+  (case command_keyword name of
+    NONE => []
+  | SOME (Keyword {kind, files, ...}) =>
+      if kind <> kind_of thy_load then []
+      else if null files then [path]
+      else map (fn ext => Path.ext ext path) files);
+
 val command_tags = these o Option.map tags_of o command_keyword;
 
 fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());

--- a/src/Pure/PIDE/command.ML	Tue Nov 19 20:59:05 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Tue Nov 19 21:49:31 2013 +0100
@@ -88,10 +88,20 @@
 fun resolve_files blobs toks =
   (case Thy_Syntax.parse_spans toks of
     [span] => span
-      |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
-        blobs |> (map o Exn.map_result) (fn (file, text) =>
-          let val _ = Position.report pos (Markup.path file);
-          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end))
+      |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
+        let
+          fun make_file src_path (Exn.Res (file, text)) =
+                let val _ = Position.report pos (Markup.path file);
+                in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
+            | make_file _ (Exn.Exn e) = Exn.Exn e;
+
+          val src_paths = Keyword.command_files cmd path;
+        in
+          if null blobs then []
+          else if length src_paths <> length blobs then
+            error ("Misalignment of inlined files" ^ Position.here pos)
+          else map2 make_file src_paths blobs
+        end)
       |> Thy_Syntax.span_content
   | _ => toks);
 

--- a/src/Pure/Thy/thy_load.ML	Tue Nov 19 20:59:05 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Tue Nov 19 21:49:31 2013 +0100
@@ -61,16 +61,12 @@
 
 fun read_files dir cmd (path, pos) =
   let
-    fun make_file file =
+    fun make_file src_path =
       let
-        val _ = Position.report pos (Markup.path (Path.implode file));
-        val full_path = check_file dir file;
-      in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
-    val paths =
-      (case Keyword.command_files cmd of
-        [] => [path]
-      | exts => map (fn ext => Path.ext ext path) exts);
-  in map make_file paths end;
+        val full_path = check_file dir src_path;
+        val _ = Position.report pos (Markup.path (Path.implode full_path));
+      in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
+  in map make_file (Keyword.command_files cmd path) end;
 
 fun parse_files cmd =
   Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>