src/Pure/Thy/thy_load.ML
changeset 48869 4371a8d029f2
parent 48868 aeea516440c8
child 48874 ff9cd47be39b
     1.1 --- a/src/Pure/Thy/thy_load.ML	Mon Aug 20 21:52:31 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Aug 21 11:00:54 2012 +0200
     1.3 @@ -73,6 +73,59 @@
     1.4      else (master_dir, imports, required, (src_path, path_id) :: provided));
     1.5  
     1.6  
     1.7 +(* inlined files *)
     1.8 +
     1.9 +fun command_files cmd path =
    1.10 +  (case Keyword.command_files cmd of
    1.11 +    [] => [path]
    1.12 +  | exts => map (fn ext => Path.ext ext path) exts);
    1.13 +
    1.14 +fun read_files cmd dir tok =
    1.15 +  let
    1.16 +    val path = Path.explode (Token.content_of tok);
    1.17 +    val files =
    1.18 +      command_files cmd path
    1.19 +      |> map (Path.append dir #> (fn p => (File.read p, Path.position p)));
    1.20 +  in (dir, files) end;
    1.21 +
    1.22 +fun parse_files cmd =
    1.23 +  Scan.ahead Parse.not_eof -- Parse.group (fn () => "file name/path specification") Parse.name
    1.24 +    >> (fn (tok, name) => fn thy =>
    1.25 +      (case Token.get_files tok of
    1.26 +        SOME files => files
    1.27 +      | NONE =>
    1.28 +          (warning ("Dynamic loading of files: " ^ quote name ^ Token.pos_of tok);
    1.29 +            read_files cmd (master_directory thy) tok)));
    1.30 +
    1.31 +local
    1.32 +
    1.33 +fun clean ((i1, t1) :: (i2, t2) :: toks) =
    1.34 +      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
    1.35 +      else (i1, t1) :: clean ((i2, t2) :: toks)
    1.36 +  | clean toks = toks;
    1.37 +
    1.38 +fun clean_tokens toks =
    1.39 +  ((0 upto length toks - 1) ~~ toks)
    1.40 +  |> filter (fn (_, tok) => Token.is_proper tok) |> clean;
    1.41 +
    1.42 +in
    1.43 +
    1.44 +fun resolve_files dir (span as Thy_Syntax.Span (Thy_Syntax.Command cmd, toks)) =
    1.45 +      if Keyword.is_theory_load cmd then
    1.46 +        (case find_first (Token.is_name o #2) (rev (clean_tokens toks)) of
    1.47 +          NONE => span
    1.48 +        | SOME (i, _) =>
    1.49 +            let
    1.50 +              val toks' = toks |> map_index (fn (j, tok) =>
    1.51 +                if i = j then Token.put_files (read_files cmd dir tok) tok
    1.52 +                else tok);
    1.53 +            in Thy_Syntax.Span (Thy_Syntax.Command cmd, toks') end)
    1.54 +      else span
    1.55 +  | resolve_files _ span = span;
    1.56 +
    1.57 +end;
    1.58 +
    1.59 +
    1.60  (* check files *)
    1.61  
    1.62  fun check_file dir file = File.check_file (File.full_path dir file);
    1.63 @@ -160,51 +213,6 @@
    1.64  fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
    1.65  
    1.66  
    1.67 -(* inlined files *)
    1.68 -
    1.69 -fun read_files cmd dir tok =
    1.70 -  let
    1.71 -    val path = Path.explode (Token.content_of tok);
    1.72 -    val exts = Keyword.command_files cmd;
    1.73 -    val variants =
    1.74 -      if null exts then [path]
    1.75 -      else map (fn ext => Path.ext ext path) exts;
    1.76 -  in (dir, variants |> map (Path.append dir #> (fn p => (File.read p, Path.position p)))) end;
    1.77 -
    1.78 -
    1.79 -fun clean ((i1, t1) :: (i2, t2) :: toks) =
    1.80 -      if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
    1.81 -      else (i1, t1) :: clean ((i2, t2) :: toks)
    1.82 -  | clean toks = toks;
    1.83 -
    1.84 -fun clean_tokens toks =
    1.85 -  ((0 upto length toks - 1) ~~ toks)
    1.86 -  |> filter (fn (_, tok) => Token.is_proper tok) |> clean;
    1.87 -
    1.88 -fun resolve_files dir (span as Thy_Syntax.Span (Thy_Syntax.Command cmd, toks)) =
    1.89 -      if Keyword.is_theory_load cmd then
    1.90 -        (case find_first (Token.is_name o #2) (rev (clean_tokens toks)) of
    1.91 -          NONE => span
    1.92 -        | SOME (i, _) =>
    1.93 -            let
    1.94 -              val toks' = toks |> map_index (fn (j, tok) =>
    1.95 -                if i = j then Token.put_files (read_files cmd dir tok) tok
    1.96 -                else tok);
    1.97 -            in Thy_Syntax.Span (Thy_Syntax.Command cmd, toks') end)
    1.98 -      else span
    1.99 -  | resolve_files _ span = span;
   1.100 -
   1.101 -fun parse_files cmd =
   1.102 -  Scan.ahead Parse.not_eof -- Parse.group (fn () => "file name/path specification") Parse.name
   1.103 -    >> (fn (tok, name) => fn thy =>
   1.104 -      (case Token.get_files tok of
   1.105 -        SOME files => files
   1.106 -      | NONE =>
   1.107 -          (warning ("Dynamic loading of files: " ^ quote name ^
   1.108 -              Position.str_of (Token.position_of tok));
   1.109 -            read_files cmd (master_directory thy) tok)));
   1.110 -
   1.111 -
   1.112  (* load_thy *)
   1.113  
   1.114  fun begin_theory dir {name, imports, keywords, uses} parents =