replaced File.check by specific File.check_file, File.check_dir;
authorwenzelm
Sun Mar 20 17:40:45 2011 +0100 (2011-03-20)
changeset 420036e45dc518ebb
parent 42002 ac7097bd8611
child 42004 e06351ffb475
replaced File.check by specific File.check_file, File.check_dir;
clarified File.full_path -- include parts of former Thy_Load.get_file;
simplified Thy_Load.check_file -- do not read/digest yet;
merged Thy_Load.check_thy/deps_thy -- always read text and parse header;
clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator;
Thy_Info.check_deps etc.: File.read exactly once;
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/SPARK/Tools/spark_commands.ML
src/Pure/General/file.ML
src/Pure/ProofGeneral/pgip_types.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Tools/Code/code_haskell.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Mar 20 13:49:21 2011 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Mar 20 17:40:45 2011 +0100
     1.3 @@ -22,8 +22,7 @@
     1.4          "expected file ending " ^ quote ext)
     1.5  
     1.6      val base_path = Path.explode base_name |> tap check_ext
     1.7 -    val (full_path, _) =
     1.8 -      Thy_Load.check_file (Thy_Load.master_directory thy) base_path
     1.9 +    val full_path = Thy_Load.check_file (Thy_Load.master_directory thy) base_path
    1.10  
    1.11      val _ = Boogie_VCs.is_closed thy orelse
    1.12        error ("Found the beginning of a new Boogie environment, " ^
     2.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Sun Mar 20 13:49:21 2011 +0100
     2.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sun Mar 20 17:40:45 2011 +0100
     2.3 @@ -15,8 +15,7 @@
     2.4  
     2.5  fun spark_open vc_name thy =
     2.6    let
     2.7 -    val (vc_path, _) = Thy_Load.check_file
     2.8 -      (Thy_Load.master_directory thy) (Path.explode vc_name);
     2.9 +    val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name);
    2.10      val (base, header) =
    2.11        (case Path.split_ext vc_path of
    2.12          (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
     3.1 --- a/src/Pure/General/file.ML	Sun Mar 20 13:49:21 2011 +0100
     3.2 +++ b/src/Pure/General/file.ML	Sun Mar 20 17:40:45 2011 +0100
     3.3 @@ -11,12 +11,13 @@
     3.4    val shell_path: Path.T -> string
     3.5    val cd: Path.T -> unit
     3.6    val pwd: unit -> Path.T
     3.7 -  val full_path: Path.T -> Path.T
     3.8 +  val full_path: Path.T -> Path.T -> Path.T
     3.9    val tmp_path: Path.T -> Path.T
    3.10    val exists: Path.T -> bool
    3.11 -  val check: Path.T -> unit
    3.12    val rm: Path.T -> unit
    3.13    val is_dir: Path.T -> bool
    3.14 +  val check_dir: Path.T -> Path.T
    3.15 +  val check_file: Path.T -> Path.T
    3.16    val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
    3.17    val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
    3.18    val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
    3.19 @@ -51,9 +52,18 @@
    3.20  val cd = cd o platform_path;
    3.21  val pwd = Path.explode o pwd;
    3.22  
    3.23 -fun full_path path =
    3.24 -  if Path.is_absolute path then path
    3.25 -  else Path.append (pwd ()) path;
    3.26 +
    3.27 +(* full_path *)
    3.28 +
    3.29 +fun full_path dir path =
    3.30 +  let
    3.31 +    val path' = Path.expand path;
    3.32 +    val _ = Path.is_current path' andalso error "Bad file specification";
    3.33 +    val path'' = Path.append dir path';
    3.34 +  in
    3.35 +    if Path.is_absolute path'' then path''
    3.36 +    else Path.append (pwd ()) path''
    3.37 +  end;
    3.38  
    3.39  
    3.40  (* tmp_path *)
    3.41 @@ -66,15 +76,19 @@
    3.42  
    3.43  val exists = can OS.FileSys.modTime o platform_path;
    3.44  
    3.45 -fun check path =
    3.46 -  if exists path then ()
    3.47 -  else error ("No such file or directory: " ^ Path.print path);
    3.48 -
    3.49  val rm = OS.FileSys.remove o platform_path;
    3.50  
    3.51  fun is_dir path =
    3.52    the_default false (try OS.FileSys.isDir (platform_path path));
    3.53  
    3.54 +fun check_dir path =
    3.55 +  if exists path andalso is_dir path then path
    3.56 +  else error ("No such directory: " ^ Path.print path);
    3.57 +
    3.58 +fun check_file path =
    3.59 +  if exists path andalso not (is_dir path) then path
    3.60 +  else error ("No such file: " ^ Path.print path);
    3.61 +
    3.62  
    3.63  (* open files *)
    3.64  
     4.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Sun Mar 20 13:49:21 2011 +0100
     4.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Sun Mar 20 17:40:45 2011 +0100
     4.3 @@ -364,7 +364,9 @@
     4.4  
     4.5  fun string_of_pgipurl p = Path.implode p
     4.6  
     4.7 -fun attrval_of_pgipurl purl = "file:" ^ (XML.text (File.platform_path (File.full_path purl)))
     4.8 +fun attrval_of_pgipurl purl =
     4.9 +  "file:" ^ XML.text (File.platform_path (File.full_path Path.current purl))
    4.10 +
    4.11  fun attrs_of_pgipurl purl = [("url", attrval_of_pgipurl purl)]
    4.12  
    4.13  val pgipurl_of_attrs = pgipurl_of_string o get_attr "url"
     5.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Mar 20 13:49:21 2011 +0100
     5.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Mar 20 17:40:45 2011 +0100
     5.3 @@ -588,14 +588,14 @@
     5.4  
     5.5          fun filerefs f =
     5.6              let val thy = thy_name f
     5.7 -                val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy)
     5.8 +                val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy))
     5.9              in
    5.10                  issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
    5.11                                       name=NONE, idtables=[], fileurls=filerefs})
    5.12              end
    5.13  
    5.14          fun thyrefs thy =
    5.15 -            let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy)
    5.16 +            let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
    5.17              in
    5.18                  issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
    5.19                                       name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
     6.1 --- a/src/Pure/Thy/present.ML	Sun Mar 20 13:49:21 2011 +0100
     6.2 +++ b/src/Pure/Thy/present.ML	Sun Mar 20 17:40:45 2011 +0100
     6.3 @@ -462,7 +462,7 @@
     6.4  
     6.5      val files_html = files |> map (fn (raw_path, loadit) =>
     6.6        let
     6.7 -        val path = #1 (Thy_Load.check_file dir raw_path);
     6.8 +        val path = Thy_Load.check_file dir raw_path;
     6.9          val base = Path.base path;
    6.10          val base_html = html_ext base;
    6.11          val _ = add_file (Path.append html_prefix base_html,
     7.1 --- a/src/Pure/Thy/thy_header.ML	Sun Mar 20 13:49:21 2011 +0100
     7.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Mar 20 17:40:45 2011 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  signature THY_HEADER =
     7.5  sig
     7.6    val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
     7.7 -  val read: Position.T -> string -> string * string list * (string * bool) list
     7.8 +  val read: Position.T -> string -> string * string list * (Path.T * bool) list
     7.9    val thy_path: string -> Path.T
    7.10    val split_thy_path: Path.T -> Path.T * string
    7.11    val consistent_name: string -> string -> unit
    7.12 @@ -63,7 +63,8 @@
    7.13      |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
    7.14      |> Source.get_single;
    7.15    in
    7.16 -    (case res of SOME (x, _) => x
    7.17 +    (case res of
    7.18 +      SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses)
    7.19      | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
    7.20    end;
    7.21  
     8.1 --- a/src/Pure/Thy/thy_info.ML	Sun Mar 20 13:49:21 2011 +0100
     8.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Mar 20 17:40:45 2011 +0100
     8.3 @@ -232,7 +232,7 @@
     8.4      val {master = (thy_path, _), imports} = deps;
     8.5      val dir = Path.dir thy_path;
     8.6      val pos = Path.position thy_path;
     8.7 -    val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
     8.8 +    val (_, _, uses) = Thy_Header.read pos text;
     8.9      fun init _ =
    8.10        Thy_Load.begin_theory dir name imports parent_thys uses
    8.11        |> Present.begin_theory update_time dir uses;
    8.12 @@ -251,24 +251,20 @@
    8.13  
    8.14  fun check_deps dir name =
    8.15    (case lookup_deps name of
    8.16 -    SOME NONE => (true, NONE, get_parents name, NONE)
    8.17 +    SOME NONE => (true, NONE, get_parents name)
    8.18    | NONE =>
    8.19 -      let val {master, text, imports, ...} = Thy_Load.deps_thy dir name
    8.20 -      in (false, SOME (make_deps master imports), imports, SOME text) end
    8.21 +      let val {master, text, imports, ...} = Thy_Load.check_thy dir name
    8.22 +      in (false, SOME (make_deps master imports, text), imports) end
    8.23    | SOME (SOME {master, imports}) =>
    8.24 -      let val master' = Thy_Load.check_thy dir name in
    8.25 -        if #2 master <> #2 master' then
    8.26 -          let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name;
    8.27 -          in (false, SOME (make_deps master' imports'), imports', SOME text') end
    8.28 -        else
    8.29 -          let
    8.30 -            val current =
    8.31 -              (case lookup_theory name of
    8.32 -                NONE => false
    8.33 -              | SOME theory => Thy_Load.all_current theory);
    8.34 -            val deps' = SOME (make_deps master' imports);
    8.35 -          in (current, deps', imports, NONE) end
    8.36 -      end);
    8.37 +      let
    8.38 +        val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name;
    8.39 +        val deps' = SOME (make_deps master' imports', text');
    8.40 +        val current =
    8.41 +          #2 master = #2 master' andalso
    8.42 +            (case lookup_theory name of
    8.43 +              NONE => false
    8.44 +            | SOME theory => Thy_Load.all_current theory);
    8.45 +      in (current, deps', imports') end);
    8.46  
    8.47  in
    8.48  
    8.49 @@ -285,14 +281,15 @@
    8.50        SOME task => (task_finished task, tasks)
    8.51      | NONE =>
    8.52          let
    8.53 -          val (current, deps, imports, opt_text) = check_deps dir' name
    8.54 +          val (current, deps, imports) = check_deps dir' name
    8.55              handle ERROR msg => cat_error msg
    8.56                (loader_msg "the error(s) above occurred while examining theory" [name] ^
    8.57                  required_by "\n" initiators);
    8.58  
    8.59            val parents = map base_name imports;
    8.60            val (parents_current, tasks') =
    8.61 -            require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks;
    8.62 +            require_thys (name :: initiators)
    8.63 +              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
    8.64  
    8.65            val all_current = current andalso parents_current;
    8.66            val task =
    8.67 @@ -300,10 +297,8 @@
    8.68              else
    8.69                (case deps of
    8.70                  NONE => raise Fail "Malformed deps"
    8.71 -              | SOME (dep as {master = (thy_path, _), ...}) =>
    8.72 -                  let
    8.73 -                    val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
    8.74 -                    val update_time = serial ();
    8.75 +              | SOME (dep, text) =>
    8.76 +                  let val update_time = serial ()
    8.77                    in Task (parents, load_thy initiators update_time dep text name) end);
    8.78          in (all_current, new_entry name parents task tasks') end)
    8.79    end;
    8.80 @@ -336,7 +331,7 @@
    8.81  fun register_thy theory =
    8.82    let
    8.83      val name = Context.theory_name theory;
    8.84 -    val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
    8.85 +    val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
    8.86      val parents = map Context.theory_name (Theory.parents_of theory);
    8.87      val imports = Thy_Load.imports_of theory;
    8.88      val deps = make_deps master imports;
     9.1 --- a/src/Pure/Thy/thy_load.ML	Sun Mar 20 13:49:21 2011 +0100
     9.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Mar 20 17:40:45 2011 +0100
     9.3 @@ -9,10 +9,9 @@
     9.4    val master_directory: theory -> Path.T
     9.5    val imports_of: theory -> string list
     9.6    val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
     9.7 -  val check_file: Path.T -> Path.T -> Path.T * SHA1.digest
     9.8 -  val check_thy: Path.T -> string -> Path.T * SHA1.digest
     9.9 -  val deps_thy: Path.T -> string ->
    9.10 -   {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list}
    9.11 +  val check_file: Path.T -> Path.T -> Path.T
    9.12 +  val check_thy: Path.T -> string ->
    9.13 +    {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
    9.14    val loaded_files: theory -> Path.T list
    9.15    val all_current: theory -> bool
    9.16    val provide_file: Path.T -> theory -> theory
    9.17 @@ -70,37 +69,23 @@
    9.18  
    9.19  (* check files *)
    9.20  
    9.21 -fun get_file dir src_path =
    9.22 +fun check_file dir file = File.check_file (File.full_path dir file);
    9.23 +
    9.24 +fun digest_file dir file =
    9.25    let
    9.26 -    val path = Path.expand src_path;
    9.27 -    val _ = Path.is_current path andalso error "Bad file specification";
    9.28 -    val full_path = File.full_path (Path.append dir path);
    9.29 -  in
    9.30 -    if File.exists full_path
    9.31 -    then SOME (full_path, SHA1.digest (File.read full_path))
    9.32 -    else NONE
    9.33 -  end;
    9.34 -
    9.35 -fun check_file dir file =
    9.36 -  (case get_file dir file of
    9.37 -    SOME path_id => path_id
    9.38 -  | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir));
    9.39 +    val full_path = check_file dir file;
    9.40 +    val id = SHA1.digest (File.read full_path);
    9.41 +  in (full_path, id) end;
    9.42  
    9.43  fun check_thy dir name =
    9.44 -  check_file dir (Thy_Header.thy_path name);
    9.45 -
    9.46 -
    9.47 -(* theory deps *)
    9.48 -
    9.49 -fun deps_thy master_dir name =
    9.50    let
    9.51 -    val master as (thy_path, _) = check_thy master_dir name;
    9.52 -    val text = File.read thy_path;
    9.53 -    val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
    9.54 +    val master_file = check_file dir (Thy_Header.thy_path name);
    9.55 +    val text = File.read master_file;
    9.56 +    val (name', imports, uses) =
    9.57 +      if name = Context.PureN then (Context.PureN, [], [])
    9.58 +      else Thy_Header.read (Path.position master_file) text;
    9.59      val _ = Thy_Header.consistent_name name name';
    9.60 -    val uses = map (Path.explode o #1) uses;
    9.61 -  in {master = master, text = text, imports = imports, uses = uses} end;
    9.62 -
    9.63 +  in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
    9.64  
    9.65  
    9.66  (* loaded files *)
    9.67 @@ -125,7 +110,7 @@
    9.68    let
    9.69      val {master_dir, provided, ...} = Files.get thy;
    9.70      fun current (src_path, (_, id)) =
    9.71 -      (case get_file master_dir src_path of
    9.72 +      (case try (digest_file master_dir) src_path of
    9.73          NONE => false
    9.74        | SOME (_, id') => id = id');
    9.75    in can check_loaded thy andalso forall current provided end;
    9.76 @@ -136,15 +121,15 @@
    9.77  (* provide files *)
    9.78  
    9.79  fun provide_file src_path thy =
    9.80 -  provide (src_path, check_file (master_directory thy) src_path) thy;
    9.81 +  provide (src_path, digest_file (master_directory thy) src_path) thy;
    9.82  
    9.83  fun use_ml src_path =
    9.84    if is_none (Context.thread_data ()) then
    9.85 -    ML_Context.eval_file (#1 (check_file Path.current src_path))
    9.86 +    ML_Context.eval_file (check_file Path.current src_path)
    9.87    else
    9.88      let
    9.89        val thy = ML_Context.the_global_context ();
    9.90 -      val (path, id) = check_file (master_directory thy) src_path;
    9.91 +      val (path, id) = digest_file (master_directory thy) src_path;
    9.92  
    9.93        val _ = ML_Context.eval_file path;
    9.94        val _ = Context.>> Local_Theory.propagate_ml_env;
    10.1 --- a/src/Tools/Code/code_haskell.ML	Sun Mar 20 13:49:21 2011 +0100
    10.2 +++ b/src/Tools/Code/code_haskell.ML	Sun Mar 20 17:40:45 2011 +0100
    10.3 @@ -350,7 +350,7 @@
    10.4      (*serialization*)
    10.5      fun write_module width (SOME destination) (module_name, content) =
    10.6            let
    10.7 -            val _ = File.check destination;
    10.8 +            val _ = File.check_dir destination;
    10.9              val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
   10.10                o separate "/" o Long_Name.explode) module_name;
   10.11              val _ = Isabelle_System.mkdirs (Path.dir filepath);