diff -r 6c896dfef33b -r 7968c57ea240 src/Pure/PIDE/command_span.ML
--- 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;
-