src/Pure/Thy/thy_load.ML
changeset 48881 46e053eda5dd
parent 48880 03232f0bb5c4
child 48886 9604c6563226
equal deleted inserted replaced
48880:03232f0bb5c4 48881:46e053eda5dd
    90   |> filter (fn (_, tok) => Token.is_proper tok)
    90   |> filter (fn (_, tok) => Token.is_proper tok)
    91   |> clean;
    91   |> clean;
    92 
    92 
    93 fun find_file toks =
    93 fun find_file toks =
    94   rev (clean_tokens toks) |> get_first (fn (i, tok) =>
    94   rev (clean_tokens toks) |> get_first (fn (i, tok) =>
    95     if Token.is_name tok then SOME (i, Path.explode (Token.content_of tok))
    95     if Token.is_name tok then
       
    96     SOME (i, Path.explode (Token.content_of tok))
       
    97       handle ERROR msg => error (msg ^ Token.pos_of tok)
    96     else NONE);
    98     else NONE);
    97 
    99 
    98 fun command_files path exts =
   100 fun command_files path exts =
    99   if null exts then [path]
   101   if null exts then [path]
   100   else map (fn ext => Path.ext ext path) exts;
   102   else map (fn ext => Path.ext ext path) exts;
   124       command_files path (Keyword.command_files cmd)
   126       command_files path (Keyword.command_files cmd)
   125       |> map (check_file dir #> (fn p => (File.read p, Path.position p)));
   127       |> map (check_file dir #> (fn p => (File.read p, Path.position p)));
   126   in (dir, files) end;
   128   in (dir, files) end;
   127 
   129 
   128 fun parse_files cmd =
   130 fun parse_files cmd =
   129   Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, path) => fn thy =>
   131   Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
   130     (case Token.get_files tok of
   132     (case Token.get_files tok of
   131       SOME files => files
   133       SOME files => files
   132     | NONE =>
   134     | NONE =>
   133         (warning ("Dynamic loading of files: " ^ Path.print path ^ Token.pos_of tok);
   135         let
   134           read_files cmd (master_directory thy) path)));
   136           val path = Path.explode name;
       
   137           val _ = warning ("Dynamic loading of files: " ^ Path.print path);
       
   138         in read_files cmd (master_directory thy) path end));
   135 
   139 
   136 fun resolve_files dir span =
   140 fun resolve_files dir span =
   137   (case span of
   141   (case span of
   138     Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) =>
   142     Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) =>
   139       if Keyword.is_theory_load cmd then
   143       if Keyword.is_theory_load cmd then