# HG changeset patch # User wenzelm # Date 1300639245 -3600 # Node ID 6e45dc518ebb513054b28d34b694ad06d5303313 # Parent ac7097bd861118217d043f1c52b452b3f01a764e 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; diff -r ac7097bd8611 -r 6e45dc518ebb src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sun Mar 20 17:40:45 2011 +0100 @@ -22,8 +22,7 @@ "expected file ending " ^ quote ext) val base_path = Path.explode base_name |> tap check_ext - val (full_path, _) = - Thy_Load.check_file (Thy_Load.master_directory thy) base_path + val full_path = Thy_Load.check_file (Thy_Load.master_directory thy) base_path val _ = Boogie_VCs.is_closed thy orelse error ("Found the beginning of a new Boogie environment, " ^ diff -r ac7097bd8611 -r 6e45dc518ebb src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/HOL/SPARK/Tools/spark_commands.ML Sun Mar 20 17:40:45 2011 +0100 @@ -15,8 +15,7 @@ fun spark_open vc_name thy = let - val (vc_path, _) = Thy_Load.check_file - (Thy_Load.master_directory thy) (Path.explode vc_name); + val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name); val (base, header) = (case Path.split_ext vc_path of (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ()) diff -r ac7097bd8611 -r 6e45dc518ebb src/Pure/General/file.ML --- a/src/Pure/General/file.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/Pure/General/file.ML Sun Mar 20 17:40:45 2011 +0100 @@ -11,12 +11,13 @@ val shell_path: Path.T -> string val cd: Path.T -> unit val pwd: unit -> Path.T - val full_path: Path.T -> Path.T + val full_path: Path.T -> Path.T -> Path.T val tmp_path: Path.T -> Path.T val exists: Path.T -> bool - val check: Path.T -> unit val rm: Path.T -> unit val is_dir: Path.T -> bool + val check_dir: Path.T -> Path.T + val check_file: Path.T -> Path.T val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a @@ -51,9 +52,18 @@ val cd = cd o platform_path; val pwd = Path.explode o pwd; -fun full_path path = - if Path.is_absolute path then path - else Path.append (pwd ()) path; + +(* full_path *) + +fun full_path dir path = + let + val path' = Path.expand path; + val _ = Path.is_current path' andalso error "Bad file specification"; + val path'' = Path.append dir path'; + in + if Path.is_absolute path'' then path'' + else Path.append (pwd ()) path'' + end; (* tmp_path *) @@ -66,15 +76,19 @@ val exists = can OS.FileSys.modTime o platform_path; -fun check path = - if exists path then () - else error ("No such file or directory: " ^ Path.print path); - val rm = OS.FileSys.remove o platform_path; fun is_dir path = the_default false (try OS.FileSys.isDir (platform_path path)); +fun check_dir path = + if exists path andalso is_dir path then path + else error ("No such directory: " ^ Path.print path); + +fun check_file path = + if exists path andalso not (is_dir path) then path + else error ("No such file: " ^ Path.print path); + (* open files *) diff -r ac7097bd8611 -r 6e45dc518ebb src/Pure/ProofGeneral/pgip_types.ML --- a/src/Pure/ProofGeneral/pgip_types.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/Pure/ProofGeneral/pgip_types.ML Sun Mar 20 17:40:45 2011 +0100 @@ -364,7 +364,9 @@ fun string_of_pgipurl p = Path.implode p -fun attrval_of_pgipurl purl = "file:" ^ (XML.text (File.platform_path (File.full_path purl))) +fun attrval_of_pgipurl purl = + "file:" ^ XML.text (File.platform_path (File.full_path Path.current purl)) + fun attrs_of_pgipurl purl = [("url", attrval_of_pgipurl purl)] val pgipurl_of_attrs = pgipurl_of_string o get_attr "url" diff -r ac7097bd8611 -r 6e45dc518ebb src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Mar 20 17:40:45 2011 +0100 @@ -588,14 +588,14 @@ fun filerefs f = let val thy = thy_name f - val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy) + val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy)) in issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile, name=NONE, idtables=[], fileurls=filerefs}) end fun thyrefs thy = - let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy) + let val thyrefs = #imports (Thy_Load.check_thy Path.current thy) in issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory, name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory, diff -r ac7097bd8611 -r 6e45dc518ebb src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/Pure/Thy/present.ML Sun Mar 20 17:40:45 2011 +0100 @@ -462,7 +462,7 @@ val files_html = files |> map (fn (raw_path, loadit) => let - val path = #1 (Thy_Load.check_file dir raw_path); + val path = Thy_Load.check_file dir raw_path; val base = Path.base path; val base_html = html_ext base; val _ = add_file (Path.append html_prefix base_html, diff -r ac7097bd8611 -r 6e45dc518ebb src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/Pure/Thy/thy_header.ML Sun Mar 20 17:40:45 2011 +0100 @@ -7,7 +7,7 @@ signature THY_HEADER = sig val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list - val read: Position.T -> string -> string * string list * (string * bool) list + val read: Position.T -> string -> string * string list * (Path.T * bool) list val thy_path: string -> Path.T val split_thy_path: Path.T -> Path.T * string val consistent_name: string -> string -> unit @@ -63,7 +63,8 @@ |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE |> Source.get_single; in - (case res of SOME (x, _) => x + (case res of + SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses) | NONE => error ("Unexpected end of input" ^ Position.str_of pos)) end; diff -r ac7097bd8611 -r 6e45dc518ebb src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/Pure/Thy/thy_info.ML Sun Mar 20 17:40:45 2011 +0100 @@ -232,7 +232,7 @@ val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val pos = Path.position thy_path; - val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text)); + val (_, _, uses) = Thy_Header.read pos text; fun init _ = Thy_Load.begin_theory dir name imports parent_thys uses |> Present.begin_theory update_time dir uses; @@ -251,24 +251,20 @@ fun check_deps dir name = (case lookup_deps name of - SOME NONE => (true, NONE, get_parents name, NONE) + SOME NONE => (true, NONE, get_parents name) | NONE => - let val {master, text, imports, ...} = Thy_Load.deps_thy dir name - in (false, SOME (make_deps master imports), imports, SOME text) end + let val {master, text, imports, ...} = Thy_Load.check_thy dir name + in (false, SOME (make_deps master imports, text), imports) end | SOME (SOME {master, imports}) => - let val master' = Thy_Load.check_thy dir name in - if #2 master <> #2 master' then - let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name; - in (false, SOME (make_deps master' imports'), imports', SOME text') end - else - let - val current = - (case lookup_theory name of - NONE => false - | SOME theory => Thy_Load.all_current theory); - val deps' = SOME (make_deps master' imports); - in (current, deps', imports, NONE) end - end); + let + val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name; + val deps' = SOME (make_deps master' imports', text'); + val current = + #2 master = #2 master' andalso + (case lookup_theory name of + NONE => false + | SOME theory => Thy_Load.all_current theory); + in (current, deps', imports') end); in @@ -285,14 +281,15 @@ SOME task => (task_finished task, tasks) | NONE => let - val (current, deps, imports, opt_text) = check_deps dir' name + val (current, deps, imports) = check_deps dir' name handle ERROR msg => cat_error msg (loader_msg "the error(s) above occurred while examining theory" [name] ^ required_by "\n" initiators); val parents = map base_name imports; val (parents_current, tasks') = - require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks; + require_thys (name :: initiators) + (Path.append dir (master_dir (Option.map #1 deps))) imports tasks; val all_current = current andalso parents_current; val task = @@ -300,10 +297,8 @@ else (case deps of NONE => raise Fail "Malformed deps" - | SOME (dep as {master = (thy_path, _), ...}) => - let - val text = (case opt_text of SOME text => text | NONE => File.read thy_path); - val update_time = serial (); + | SOME (dep, text) => + let val update_time = serial () in Task (parents, load_thy initiators update_time dep text name) end); in (all_current, new_entry name parents task tasks') end) end; @@ -336,7 +331,7 @@ fun register_thy theory = let val name = Context.theory_name theory; - val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name; + val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name; val parents = map Context.theory_name (Theory.parents_of theory); val imports = Thy_Load.imports_of theory; val deps = make_deps master imports; diff -r ac7097bd8611 -r 6e45dc518ebb src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/Pure/Thy/thy_load.ML Sun Mar 20 17:40:45 2011 +0100 @@ -9,10 +9,9 @@ val master_directory: theory -> Path.T val imports_of: theory -> string list val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory - val check_file: Path.T -> Path.T -> Path.T * SHA1.digest - val check_thy: Path.T -> string -> Path.T * SHA1.digest - val deps_thy: Path.T -> string -> - {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list} + val check_file: Path.T -> Path.T -> Path.T + val check_thy: Path.T -> string -> + {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list} val loaded_files: theory -> Path.T list val all_current: theory -> bool val provide_file: Path.T -> theory -> theory @@ -70,37 +69,23 @@ (* check files *) -fun get_file dir src_path = +fun check_file dir file = File.check_file (File.full_path dir file); + +fun digest_file dir file = let - val path = Path.expand src_path; - val _ = Path.is_current path andalso error "Bad file specification"; - val full_path = File.full_path (Path.append dir path); - in - if File.exists full_path - then SOME (full_path, SHA1.digest (File.read full_path)) - else NONE - end; - -fun check_file dir file = - (case get_file dir file of - SOME path_id => path_id - | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir)); + val full_path = check_file dir file; + val id = SHA1.digest (File.read full_path); + in (full_path, id) end; fun check_thy dir name = - check_file dir (Thy_Header.thy_path name); - - -(* theory deps *) - -fun deps_thy master_dir name = let - val master as (thy_path, _) = check_thy master_dir name; - val text = File.read thy_path; - val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text; + val master_file = check_file dir (Thy_Header.thy_path name); + val text = File.read master_file; + val (name', imports, uses) = + if name = Context.PureN then (Context.PureN, [], []) + else Thy_Header.read (Path.position master_file) text; val _ = Thy_Header.consistent_name name name'; - val uses = map (Path.explode o #1) uses; - in {master = master, text = text, imports = imports, uses = uses} end; - + in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end; (* loaded files *) @@ -125,7 +110,7 @@ let val {master_dir, provided, ...} = Files.get thy; fun current (src_path, (_, id)) = - (case get_file master_dir src_path of + (case try (digest_file master_dir) src_path of NONE => false | SOME (_, id') => id = id'); in can check_loaded thy andalso forall current provided end; @@ -136,15 +121,15 @@ (* provide files *) fun provide_file src_path thy = - provide (src_path, check_file (master_directory thy) src_path) thy; + provide (src_path, digest_file (master_directory thy) src_path) thy; fun use_ml src_path = if is_none (Context.thread_data ()) then - ML_Context.eval_file (#1 (check_file Path.current src_path)) + ML_Context.eval_file (check_file Path.current src_path) else let val thy = ML_Context.the_global_context (); - val (path, id) = check_file (master_directory thy) src_path; + val (path, id) = digest_file (master_directory thy) src_path; val _ = ML_Context.eval_file path; val _ = Context.>> Local_Theory.propagate_ml_env; diff -r ac7097bd8611 -r 6e45dc518ebb src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Sun Mar 20 13:49:21 2011 +0100 +++ b/src/Tools/Code/code_haskell.ML Sun Mar 20 17:40:45 2011 +0100 @@ -350,7 +350,7 @@ (*serialization*) fun write_module width (SOME destination) (module_name, content) = let - val _ = File.check destination; + val _ = File.check_dir destination; val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode o separate "/" o Long_Name.explode) module_name; val _ = Isabelle_System.mkdirs (Path.dir filepath);