diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/command_span.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/command_span.ML	Tue Aug 12 00:08:32 2014 +0200
@@ -0,0 +1,70 @@
+(*  Title:      Pure/PIDE/command_span.ML
+    Author:     Makarius
+
+Syntactic representation of command spans.
+*)
+
+signature COMMAND_SPAN =
+sig
+  datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
+  datatype span = Span of kind * Token.T list
+  val kind: span -> kind
+  val content: span -> Token.T list
+  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
+end;
+
+structure Command_Span: COMMAND_SPAN =
+struct
+
+datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
+datatype span = Span of kind * Token.T list;
+
+fun kind (Span (k, _)) = k;
+fun content (Span (_, toks)) = toks;
+
+
+(* resolve inlined files *)
+
+local
+
+fun clean ((i1, t1) :: (i2, t2) :: toks) =
+      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
+      else (i1, t1) :: clean ((i2, t2) :: toks)
+  | clean toks = toks;
+
+fun clean_tokens toks =
+  ((0 upto length toks - 1) ~~ toks)
+  |> filter (fn (_, tok) => Token.is_proper tok)
+  |> clean;
+
+fun find_file ((_, tok) :: toks) =
+      if Token.is_command tok then
+        toks |> get_first (fn (i, tok) =>
+          if Token.is_name tok then
+            SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
+              handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
+          else NONE)
+      else NONE
+  | find_file [] = NONE;
+
+in
+
+fun resolve_files read_files span =
+  (case span of
+    Span (Command_Span (cmd, pos), toks) =>
+      if Keyword.is_theory_load cmd then
+        (case find_file (clean_tokens toks) of
+          NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
+        | SOME (i, path) =>
+            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;
+