# HG changeset patch # User wenzelm # Date 1290863944 -3600 # Node ID 17d6293a1e264a98524cbde0105e6e07a9957776 # Parent 6bff052e4f48bd45beb1ec7bf91d1c4053c9a6b4 moved file identification to thy_load.ML (where it is actually used); diff -r 6bff052e4f48 -r 17d6293a1e26 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Sat Nov 27 12:02:19 2010 +0100 +++ b/src/Pure/General/file.ML Sat Nov 27 14:19:04 2010 +0100 @@ -14,9 +14,6 @@ val full_path: Path.T -> Path.T val tmp_path: Path.T -> Path.T val isabelle_tool: string -> string -> int - eqtype ident - val rep_ident: ident -> string - val ident: Path.T -> ident option val exists: Path.T -> bool val check: Path.T -> unit val rm: Path.T -> unit @@ -84,47 +81,6 @@ else (); -(* file identification *) - -local - val ident_cache = - Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table); -in - -fun check_cache (path, time) = - (case Symtab.lookup (! ident_cache) path of - NONE => NONE - | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE); - -fun update_cache (path, (time, id)) = CRITICAL (fn () => - Unsynchronized.change ident_cache - (Symtab.update (path, {time_stamp = time, id = id}))); - -end; - -datatype ident = Ident of string; -fun rep_ident (Ident s) = s; - -fun ident path = - let val physical_path = perhaps (try OS.FileSys.fullPath) (platform_path path) in - (case try (Time.toString o OS.FileSys.modTime) physical_path of - NONE => NONE - | SOME mod_time => SOME (Ident - (case getenv "ISABELLE_FILE_IDENT" of - "" => physical_path ^ ": " ^ mod_time - | cmd => - (case check_cache (physical_path, mod_time) of - SOME id => id - | NONE => - let val (id, rc) = (*potentially slow*) - bash_output ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path) - in - if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id) - else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd) - end)))) - end; - - (* directory entries *) val exists = can OS.FileSys.modTime o platform_path; diff -r 6bff052e4f48 -r 17d6293a1e26 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Nov 27 12:02:19 2010 +0100 +++ b/src/Pure/Thy/thy_info.ML Sat Nov 27 14:19:04 2010 +0100 @@ -64,8 +64,8 @@ (* thy database *) type deps = - {master: (Path.T * File.ident), (*master dependencies for thy file*) - imports: string list}; (*source specification of imports (partially qualified)*) + {master: (Path.T * Thy_Load.file_ident), (*master dependencies for thy file*) + imports: string list}; (*source specification of imports (partially qualified)*) fun make_deps master imports : deps = {master = master, imports = imports}; diff -r 6bff052e4f48 -r 17d6293a1e26 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Sat Nov 27 12:02:19 2010 +0100 +++ b/src/Pure/Thy/thy_load.ML Sat Nov 27 14:19:04 2010 +0100 @@ -17,14 +17,17 @@ signature THY_LOAD = sig include BASIC_THY_LOAD + eqtype file_ident + val pretty_file_ident: file_ident -> Pretty.T + val file_ident: Path.T -> file_ident option val set_master_path: Path.T -> unit val get_master_path: unit -> Path.T val master_directory: theory -> Path.T - val provide: Path.T * (Path.T * File.ident) -> theory -> theory - val check_file: Path.T list -> Path.T -> Path.T * File.ident - val check_thy: Path.T -> string -> Path.T * File.ident + val provide: Path.T * (Path.T * file_ident) -> theory -> theory + val check_file: Path.T list -> Path.T -> Path.T * file_ident + val check_thy: Path.T -> string -> Path.T * file_ident val deps_thy: Path.T -> string -> - {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list} + {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list} val loaded_files: theory -> Path.T list val all_current: theory -> bool val provide_file: Path.T -> theory -> theory @@ -36,12 +39,56 @@ structure Thy_Load: THY_LOAD = struct +(* file identification *) + +local + val ident_cache = + Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table); +in + +fun check_cache (path, time) = + (case Symtab.lookup (! ident_cache) path of + NONE => NONE + | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE); + +fun update_cache (path, (time, id)) = CRITICAL (fn () => + Unsynchronized.change ident_cache + (Symtab.update (path, {time_stamp = time, id = id}))); + +end; + +datatype file_ident = File_Ident of string; + +fun pretty_file_ident (File_Ident s) = Pretty.str (quote s); + +fun file_ident path = + let val physical_path = perhaps (try OS.FileSys.fullPath) (File.platform_path path) in + (case try (Time.toString o OS.FileSys.modTime) physical_path of + NONE => NONE + | SOME mod_time => SOME (File_Ident + (case getenv "ISABELLE_FILE_IDENT" of + "" => physical_path ^ ": " ^ mod_time + | cmd => + (case check_cache (physical_path, mod_time) of + SOME id => id + | NONE => + let + val (id, rc) = (*potentially slow*) + bash_output + ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path); + in + if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id) + else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd) + end)))) + end; + + (* manage source files *) type files = - {master_dir: Path.T, (*master directory of theory source*) - required: Path.T list, (*source path*) - provided: (Path.T * (Path.T * File.ident)) list}; (*source path, physical path, identifier*) + {master_dir: Path.T, (*master directory of theory source*) + required: Path.T list, (*source path*) + provided: (Path.T * (Path.T * file_ident)) list}; (*source path, physical path, identifier*) fun make_files (master_dir, required, provided): files = {master_dir = master_dir, required = required, provided = provided}; @@ -115,7 +162,7 @@ in dirs |> get_first (fn dir => let val full_path = File.full_path (Path.append dir path) in - (case File.ident full_path of + (case file_ident full_path of NONE => NONE | SOME id => SOME (full_path, id)) end) diff -r 6bff052e4f48 -r 17d6293a1e26 src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Sat Nov 27 12:02:19 2010 +0100 +++ b/src/Pure/pure_setup.ML Sat Nov 27 14:19:04 2010 +0100 @@ -36,7 +36,7 @@ toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; -toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident"; +toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident"; toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"\")"; toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";