--- 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;
--- 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};
--- 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)
--- 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 \"<Proof.state>\")";
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";