release file errors at runtime: Command.eval instead of Command.read;
authorwenzelm
Tue Nov 19 19:43:26 2013 +0100 (2013-11-19 ago)
changeset 54520cee77d2e9582
parent 54519 5fed81762406
child 54521 744ea0025e11
release file errors at runtime: Command.eval instead of Command.read;
src/Pure/Isar/token.ML
src/Pure/PIDE/command.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/src/Pure/Isar/token.ML	Tue Nov 19 19:33:27 2013 +0100
     1.2 +++ b/src/Pure/Isar/token.ML	Tue Nov 19 19:43:26 2013 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    type file = {src_path: Path.T, text: string, pos: Position.T}
     1.5    datatype value =
     1.6      Text of string | Typ of typ | Term of term | Fact of thm list |
     1.7 -    Attribute of morphism -> attribute | Files of file list
     1.8 +    Attribute of morphism -> attribute | Files of file Exn.result list
     1.9    type T
    1.10    val str_of_kind: kind -> string
    1.11    val position_of: T -> Position.T
    1.12 @@ -46,8 +46,8 @@
    1.13    val content_of: T -> string
    1.14    val unparse: T -> string
    1.15    val text_of: T -> string * string
    1.16 -  val get_files: T -> file list
    1.17 -  val put_files: file list -> T -> T
    1.18 +  val get_files: T -> file Exn.result list
    1.19 +  val put_files: file Exn.result list -> T -> T
    1.20    val get_value: T -> value option
    1.21    val map_value: (value -> value) -> T -> T
    1.22    val mk_text: string -> T
    1.23 @@ -88,7 +88,7 @@
    1.24    Term of term |
    1.25    Fact of thm list |
    1.26    Attribute of morphism -> attribute |
    1.27 -  Files of file list;
    1.28 +  Files of file Exn.result list;
    1.29  
    1.30  datatype slot =
    1.31    Slot |
     2.1 --- a/src/Pure/PIDE/command.ML	Tue Nov 19 19:33:27 2013 +0100
     2.2 +++ b/src/Pure/PIDE/command.ML	Tue Nov 19 19:43:26 2013 +0100
     2.3 @@ -89,9 +89,9 @@
     2.4    (case Thy_Syntax.parse_spans toks of
     2.5      [span] => span
     2.6        |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
     2.7 -        blobs |> map (Exn.release #> (fn (file, text) =>
     2.8 +        blobs |> (map o Exn.map_result) (fn (file, text) =>
     2.9            let val _ = Position.report pos (Markup.path file);
    2.10 -          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end)))
    2.11 +          in {src_path = path (* FIXME *), text = text, pos = Position.file file} end))
    2.12        |> Thy_Syntax.span_content
    2.13    | _ => toks);
    2.14  
     3.1 --- a/src/Pure/Thy/thy_load.ML	Tue Nov 19 19:33:27 2013 +0100
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Nov 19 19:43:26 2013 +0100
     3.3 @@ -76,7 +76,7 @@
     3.4    Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
     3.5      (case Token.get_files tok of
     3.6        [] => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)
     3.7 -    | files => files));
     3.8 +    | files => map Exn.release files));
     3.9  
    3.10  
    3.11  (* theory files *)
    3.12 @@ -170,7 +170,9 @@
    3.13  
    3.14      val lexs = Keyword.get_lexicons ();
    3.15      val toks = Thy_Syntax.parse_tokens lexs text_pos text;
    3.16 -    val spans = map (Thy_Syntax.resolve_files (read_files master_dir)) (Thy_Syntax.parse_spans toks);
    3.17 +    val spans =
    3.18 +      map (Thy_Syntax.resolve_files (map Exn.Res oo read_files master_dir))
    3.19 +        (Thy_Syntax.parse_spans toks);
    3.20      val elements = Thy_Syntax.parse_elements spans;
    3.21  
    3.22      fun init () =
     4.1 --- a/src/Pure/Thy/thy_syntax.ML	Tue Nov 19 19:33:27 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_syntax.ML	Tue Nov 19 19:43:26 2013 +0100
     4.3 @@ -15,7 +15,7 @@
     4.4    val span_content: span -> Token.T list
     4.5    val present_span: span -> Output.output
     4.6    val parse_spans: Token.T list -> span list
     4.7 -  val resolve_files: (string -> Path.T * Position.T -> Token.file list) -> span -> span
     4.8 +  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
     4.9    datatype 'a element = Element of 'a * ('a element list * 'a) option
    4.10    val atom: 'a -> 'a element
    4.11    val map_element: ('a -> 'b) -> 'a element -> 'b element