diff -r d662d096f72b -r d6824d8490be src/Pure/PIDE/command_span.ML
--- a/src/Pure/PIDE/command_span.ML	Thu Mar 12 14:58:32 2015 +0100
+++ b/src/Pure/PIDE/command_span.ML	Thu Mar 12 16:47:47 2015 +0100
@@ -28,22 +28,20 @@
 
 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)
+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 toks =
-  ((0 upto length toks - 1) ~~ toks)
-  |> filter (fn (_, tok) => Token.is_proper tok)
-  |> clean;
+fun clean_tokens tokens =
+  clean (filter (fn (t, _) => Token.is_proper t) (tokens ~~ (0 upto length tokens - 1)));
 
-fun find_file ((_, tok) :: toks) =
+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))
+        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;
@@ -56,7 +54,7 @@
       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 (i, path) =>
+        | SOME (path, i) =>
             let
               val toks' = toks |> map_index (fn (j, tok) =>
                 if i = j then Token.put_files (read_files cmd path) tok