tuned errors;

--- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Aug 21 22:26:34 2012 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Wed Aug 22 11:56:13 2012 +0200
@@ -101,7 +101,7 @@
     val text = implode (map (Print_Mode.setmp [] Thy_Syntax.present_token) toks);
   in
     (case kind of
-      Thy_Syntax.Command name => parse_command name text
+      Thy_Syntax.Command (name, _) => parse_command name text
     | Thy_Syntax.Ignored => [D.Whitespace {text = text}]
     | Thy_Syntax.Malformed => [D.Unparseable {text = text}])
   end;

--- a/src/Pure/Thy/thy_load.ML	Tue Aug 21 22:26:34 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Aug 22 11:56:13 2012 +0200
@@ -76,6 +76,8 @@
 
 (* inlined files *)
 
+fun check_file dir file = File.check_file (File.full_path dir file);
+
 local
 
 fun clean ((i1, t1) :: (i2, t2) :: toks) =
@@ -105,7 +107,7 @@
       Thy_Syntax.parse_tokens (Keyword.lexicons_of syntax) Position.none text
       |> Thy_Syntax.parse_spans
       |> maps
-        (fn Thy_Syntax.Span (Thy_Syntax.Command cmd, toks) =>
+        (fn Thy_Syntax.Span (Thy_Syntax.Command (cmd, _), toks) =>
               (case AList.lookup (op =) thy_load_commands cmd of
                 SOME exts =>
                   (case find_file toks of
@@ -121,7 +123,7 @@
     val path = Path.explode (Token.content_of tok);
     val files =
       command_files path (Keyword.command_files cmd)
-      |> map (File.full_path dir #> (fn path => (File.read path, Path.position path)));
+      |> map (check_file dir #> (fn path => (File.read path, Path.position path)));
   in (dir, files) end;
 
 fun parse_files cmd =
@@ -135,16 +137,17 @@
 
 fun resolve_files dir span =
   (case span of
-    Thy_Syntax.Span (Thy_Syntax.Command cmd, toks) =>
+    Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) =>
       if Keyword.is_theory_load cmd then
         (case find_first (Token.is_name o #2) (rev (clean_tokens toks)) of
-          NONE => span  (* FIXME error *)
+          NONE =>
+            error ("Cannot resolve file argument of command " ^ quote cmd ^ Position.str_of pos)
         | SOME (i, path) =>
             let
               val toks' = toks |> map_index (fn (j, tok) =>
                 if i = j then Token.put_files (read_files cmd dir path) tok
                 else tok);
-            in Thy_Syntax.Span (Thy_Syntax.Command cmd, toks') end)
+            in Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks') end)
       else span
   | span => span);
 
@@ -153,8 +156,6 @@
 
 (* check files *)
 
-fun check_file dir file = File.check_file (File.full_path dir file);
-
 val thy_path = Path.ext "thy";
 
 fun check_thy base_keywords dir thy_name =

--- a/src/Pure/Thy/thy_syntax.ML	Tue Aug 21 22:26:34 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Aug 22 11:56:13 2012 +0200
@@ -9,7 +9,7 @@
   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
   val reports_of_tokens: Token.T list -> bool * (Position.report * string) list
   val present_token: Token.T -> Output.output
-  datatype span_kind = Command of string | Ignored | Malformed
+  datatype span_kind = Command of string * Position.T | Ignored | Malformed
   datatype span = Span of span_kind * Token.T list
   val span_kind: span -> span_kind
   val span_content: span -> Token.T list
@@ -100,7 +100,7 @@
 
 (* type span *)
 
-datatype span_kind = Command of string | Ignored | Malformed;
+datatype span_kind = Command of string * Position.T | Ignored | Malformed;
 datatype span = Span of span_kind * Token.T list;
 
 fun span_kind (Span (k, _)) = k;
@@ -115,7 +115,7 @@
 
 fun make_span toks =
   if not (null toks) andalso Token.is_command (hd toks) then
-    Span (Command (Token.content_of (hd toks)), toks)
+    Span (Command (Token.content_of (hd toks), Token.position_of (hd toks)), toks)
   else if forall (not o Token.is_proper) toks then Span (Ignored, toks)
   else Span (Malformed, toks);
 
@@ -142,9 +142,9 @@
 
 (* scanning spans *)
 
-val eof = Span (Command "", []);
+val eof = Span (Command ("", Position.none), []);
 
-fun is_eof (Span (Command "", _)) = true
+fun is_eof (Span (Command ("", _), _)) = true
   | is_eof _ = false;
 
 val not_eof = not o is_eof;
@@ -156,7 +156,8 @@
 
 local
 
-fun command_with pred = Scan.one (fn (Span (Command name, _)) => pred name | _ => false);
+fun command_with pred =
+  Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
 
 val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
   if d <= 0 then Scan.fail