release file errors at runtime: Command.eval instead of Command.read;

--- a/src/Pure/Isar/token.ML	Tue Nov 19 19:33:27 2013 +0100
+++ b/src/Pure/Isar/token.ML	Tue Nov 19 19:43:26 2013 +0100
@@ -13,7 +13,7 @@
   type file = {src_path: Path.T, text: string, pos: Position.T}
   datatype value =
     Text of string | Typ of typ | Term of term | Fact of thm list |
-    Attribute of morphism -> attribute | Files of file list
+    Attribute of morphism -> attribute | Files of file Exn.result list
   type T
   val str_of_kind: kind -> string
   val position_of: T -> Position.T
@@ -46,8 +46,8 @@
   val content_of: T -> string
   val unparse: T -> string
   val text_of: T -> string * string
-  val get_files: T -> file list
-  val put_files: file list -> T -> T
+  val get_files: T -> file Exn.result list
+  val put_files: file Exn.result list -> T -> T
   val get_value: T -> value option
   val map_value: (value -> value) -> T -> T
   val mk_text: string -> T
@@ -88,7 +88,7 @@
   Term of term |
   Fact of thm list |
   Attribute of morphism -> attribute |
-  Files of file list;
+  Files of file Exn.result list;
 
 datatype slot =
   Slot |

--- a/src/Pure/PIDE/command.ML	Tue Nov 19 19:33:27 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Tue Nov 19 19:43:26 2013 +0100
@@ -89,9 +89,9 @@
   (case Thy_Syntax.parse_spans toks of
     [span] => span
       |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
-        blobs |> map (Exn.release #> (fn (file, text) =>
+        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)))
+          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end))
       |> Thy_Syntax.span_content
   | _ => toks);
 

--- a/src/Pure/Thy/thy_load.ML	Tue Nov 19 19:33:27 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Tue Nov 19 19:43:26 2013 +0100
@@ -76,7 +76,7 @@
   Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
     (case Token.get_files tok of
       [] => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)
-    | files => files));
+    | files => map Exn.release files));
 
 
 (* theory files *)
@@ -170,7 +170,9 @@
 
     val lexs = Keyword.get_lexicons ();
     val toks = Thy_Syntax.parse_tokens lexs text_pos text;
-    val spans = map (Thy_Syntax.resolve_files (read_files master_dir)) (Thy_Syntax.parse_spans toks);
+    val spans =
+      map (Thy_Syntax.resolve_files (map Exn.Res oo read_files master_dir))
+        (Thy_Syntax.parse_spans toks);
     val elements = Thy_Syntax.parse_elements spans;
 
     fun init () =

--- a/src/Pure/Thy/thy_syntax.ML	Tue Nov 19 19:33:27 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Nov 19 19:43:26 2013 +0100
@@ -15,7 +15,7 @@
   val span_content: span -> Token.T list
   val present_span: span -> Output.output
   val parse_spans: Token.T list -> span list
-  val resolve_files: (string -> Path.T * Position.T -> Token.file list) -> span -> span
+  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val atom: 'a -> 'a element
   val map_element: ('a -> 'b) -> 'a element -> 'b element