discontinued separate list of required files -- maintain only provided files as they occur at runtime;
authorwenzelm
Wed Aug 22 21:02:02 2012 +0200 (2012-08-22 ago)
changeset 488869604c6563226
parent 48885 d5fdaf7dd1f8
child 48887 c49eca45cbb0
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
tuned signature;
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 22 18:04:30 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 22 21:02:02 2012 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4            #2 master = #2 master' andalso
     1.5              (case lookup_theory name of
     1.6                NONE => false
     1.7 -            | SOME theory => Thy_Load.all_current theory);
     1.8 +            | SOME theory => Thy_Load.load_current theory);
     1.9        in (current, deps', imports', uses', keywords') end);
    1.10  
    1.11  in
     2.1 --- a/src/Pure/Thy/thy_load.ML	Wed Aug 22 18:04:30 2012 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Aug 22 21:02:02 2012 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4    val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
     2.5    val use_file: Path.T -> theory -> string * theory
     2.6    val loaded_files: theory -> Path.T list
     2.7 -  val all_current: theory -> bool
     2.8 +  val load_current: theory -> bool
     2.9    val use_ml: Path.T -> unit
    2.10    val exec_ml: Path.T -> generic_theory -> generic_theory
    2.11    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    2.12 @@ -37,41 +37,34 @@
    2.13  type files =
    2.14   {master_dir: Path.T,  (*master directory of theory source*)
    2.15    imports: string list,  (*source specification of imports*)
    2.16 -  required: Path.T list,  (*source path*)
    2.17    provided: (Path.T * (Path.T * SHA1.digest)) list};  (*source path, physical path, digest*)
    2.18  
    2.19 -fun make_files (master_dir, imports, required, provided): files =
    2.20 - {master_dir = master_dir, imports = imports, required = required, provided = provided};
    2.21 +fun make_files (master_dir, imports, provided): files =
    2.22 + {master_dir = master_dir, imports = imports, provided = provided};
    2.23  
    2.24  structure Files = Theory_Data
    2.25  (
    2.26    type T = files;
    2.27 -  val empty = make_files (Path.current, [], [], []);
    2.28 +  val empty = make_files (Path.current, [], []);
    2.29    fun extend _ = empty;
    2.30    fun merge _ = empty;
    2.31  );
    2.32  
    2.33  fun map_files f =
    2.34 -  Files.map (fn {master_dir, imports, required, provided} =>
    2.35 -    make_files (f (master_dir, imports, required, provided)));
    2.36 +  Files.map (fn {master_dir, imports, provided} =>
    2.37 +    make_files (f (master_dir, imports, provided)));
    2.38  
    2.39  
    2.40  val master_directory = #master_dir o Files.get;
    2.41  val imports_of = #imports o Files.get;
    2.42  
    2.43 -fun put_deps dir imports = map_files (fn _ => (dir, imports, [], []));
    2.44 -
    2.45 -fun require src_path =
    2.46 -  map_files (fn (master_dir, imports, required, provided) =>
    2.47 -    if member (op =) required src_path then
    2.48 -      error ("Duplicate source file dependency: " ^ Path.print src_path)
    2.49 -    else (master_dir, imports, src_path :: required, provided));
    2.50 +fun put_deps dir imports = map_files (fn _ => (dir, imports, []));
    2.51  
    2.52  fun provide (src_path, path_id) =
    2.53 -  map_files (fn (master_dir, imports, required, provided) =>
    2.54 +  map_files (fn (master_dir, imports, provided) =>
    2.55      if AList.defined (op =) provided src_path then
    2.56 -      error ("Duplicate resolution of source file dependency: " ^ Path.print src_path)
    2.57 -    else (master_dir, imports, required, (src_path, path_id) :: provided));
    2.58 +      error ("Duplicate use of source file: " ^ Path.print src_path)
    2.59 +    else (master_dir, imports, (src_path, path_id) :: provided));
    2.60  
    2.61  
    2.62  (* inlined files *)
    2.63 @@ -93,8 +86,8 @@
    2.64  fun find_file toks =
    2.65    rev (clean_tokens toks) |> get_first (fn (i, tok) =>
    2.66      if Token.is_name tok then
    2.67 -    SOME (i, Path.explode (Token.content_of tok))
    2.68 -      handle ERROR msg => error (msg ^ Token.pos_of tok)
    2.69 +      SOME (i, Path.explode (Token.content_of tok))
    2.70 +        handle ERROR msg => error (msg ^ Token.pos_of tok)
    2.71      else NONE);
    2.72  
    2.73  fun command_files path exts =
    2.74 @@ -196,30 +189,12 @@
    2.75  
    2.76  val loaded_files = map (#1 o #2) o #provided o Files.get;
    2.77  
    2.78 -fun check_loaded thy =
    2.79 -  let
    2.80 -    val {required, provided, ...} = Files.get thy;
    2.81 -    val provided_paths = map #1 provided;
    2.82 -    val _ =
    2.83 -      (case subtract (op =) provided_paths required of
    2.84 -        [] => NONE
    2.85 -      | bad => error ("Pending source file dependencies: " ^ commas (map Path.print (rev bad))));
    2.86 -    val _ =
    2.87 -      (case subtract (op =) required provided_paths of
    2.88 -        [] => NONE
    2.89 -      | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.print (rev bad))));
    2.90 -  in () end;
    2.91 -
    2.92 -fun all_current thy =
    2.93 -  let
    2.94 -    val {provided, ...} = Files.get thy;
    2.95 -    fun current (src_path, (_, id)) =
    2.96 +fun load_current thy =
    2.97 +  #provided (Files.get thy) |>
    2.98 +    forall (fn (src_path, (_, id)) =>
    2.99        (case try (load_file thy) src_path of
   2.100          NONE => false
   2.101 -      | SOME ((_, id'), _) => id = id');
   2.102 -  in can check_loaded thy andalso forall current provided end;
   2.103 -
   2.104 -val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
   2.105 +      | SOME ((_, id'), _) => id = id'));
   2.106  
   2.107  
   2.108  (* provide files *)
   2.109 @@ -251,7 +226,6 @@
   2.110    Theory.begin_theory name parents
   2.111    |> put_deps dir imports
   2.112    |> fold Thy_Header.declare_keyword keywords
   2.113 -  |> fold (require o fst) uses
   2.114    |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   2.115    |> Theory.checkpoint;
   2.116