# HG changeset patch # User wenzelm # Date 1184879939 -7200 # Node ID f449381e2caa5a2c16c745776e1753f511f56e01 # Parent 0dd5696f58b671fd3e80c5573d57f5862971a546 tuned signature; load_path: always used, even for partially qualified path names; check_file: precise (no adding of extensions!); misc cleanup; diff -r 0dd5696f58b6 -r f449381e2caa src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Thu Jul 19 23:18:58 2007 +0200 +++ b/src/Pure/Thy/thy_load.ML Thu Jul 19 23:18:59 2007 +0200 @@ -22,21 +22,23 @@ val ml_exts: string list val ml_path: string -> Path.T val thy_path: string -> Path.T - val check_file: Path.T option -> Path.T -> (Path.T * File.info) option - val load_file: Path.T option -> Path.T -> (Path.T * File.info) - eqtype master - val get_thy: master -> Path.T * File.info - val check_thy: Path.T -> string -> bool -> master - val deps_thy: Path.T -> string -> bool -> master * (string list * Path.T list) - val load_thy: Path.T -> string -> bool -> bool -> master + val check_file: Path.T list -> Path.T -> (Path.T * File.ident) option + val check_ml: Path.T list -> Path.T -> (Path.T * File.ident) option + val check_thy: Path.T list -> string -> bool -> + (Path.T * File.ident) * (Path.T * File.ident) option + val deps_thy: Path.T list -> string -> bool -> + ((Path.T * File.ident) * (Path.T * File.ident) option) * (string list * Path.T list) + val load_ml: Path.T list -> Path.T -> Path.T * File.ident + val load_thy: Path.T list -> string -> bool -> bool -> + (Path.T * File.ident) * (Path.T * File.ident) option end; (*this backdoor sealed later*) signature PRIVATE_THY_LOAD = sig include THY_LOAD - val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref - val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref + val load_thy_fn: (Path.T list -> string -> bool -> bool -> + (Path.T * File.ident) * (Path.T * File.ident) option) ref end; structure ThyLoad: PRIVATE_THY_LOAD = @@ -46,12 +48,11 @@ (* maintain load path *) val load_path = ref [Path.current]; -fun change_path f = load_path := f (! load_path); fun show_path () = map Path.implode (! load_path); -fun del_path s = change_path (filter_out (equal (Path.explode s))); -fun add_path s = (del_path s; change_path (cons (Path.explode s))); -fun path_add s = (del_path s; change_path (fn path => path @ [Path.explode s])); +fun del_path s = change load_path (remove (op =) (Path.explode s)); +fun add_path s = (del_path s; change load_path (cons (Path.explode s))); +fun path_add s = (del_path s; change load_path (fn path => path @ [Path.explode s])); fun reset_path () = load_path := [Path.current]; fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x; fun with_path s f x = with_paths [s] f x; @@ -59,85 +60,66 @@ (* file formats *) -val ml_exts = ["", "ML", "sml"]; +val ml_exts = ["ML", "sml"]; val ml_path = Path.ext "ML" o Path.basic; val thy_path = Path.ext "thy" o Path.basic; -(* check_file *) +(* check files *) -fun check_file current src_path = +fun augment_path (ps: Path.T list) qs = distinct (op =) (ps @ qs); + +fun check_ext exts dirs src_path = let val path = Path.expand src_path; + val _ = Path.is_current path andalso error "Bad file specification"; + val paths = augment_path dirs (! load_path); fun find_ext rel_path ext = let val ext_path = Path.expand (Path.ext ext rel_path) - in Option.map (fn info => (File.full_path ext_path, info)) (File.info ext_path) end; - - fun find_dir dir = - get_first (find_ext (Path.append dir path)) ml_exts; - - fun add_current ps = (case current of NONE => ps - | (SOME p) => if Path.is_current p then ps else p :: ps); - - val paths = - if Path.is_current path then error "Bad file specification" - else if Path.is_basic path then add_current (! load_path) - else add_current [Path.current]; + in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end; + fun find_dir dir = get_first (find_ext (Path.append dir path)) ("" :: exts); in get_first find_dir paths end; - -(* load_file *) +val check_file = check_ext []; +val check_ml = check_ext ml_exts; -fun load_file current raw_path = - (case check_file current raw_path of - NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path)) - | SOME (path, info) => (ML_Context.use path; (path, info))); - - -(* datatype master *) - -datatype master = Master of (Path.T * File.info) * (Path.T * File.info) option; - -fun get_thy (Master (thy, _)) = thy; +fun check_thy dirs name ml = + let val thy_file = thy_path name in + (case check_file dirs thy_file of + NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^ + " in dir(s) " ^ commas_quote (map Path.implode (augment_path dirs (! load_path)))) + | SOME thy_id => (thy_id, if ml then check_file dirs (ml_path name) else NONE)) + end; -(* check / process theory files *) - -local - -fun check_thy_aux (name, ml) = - let val thy_file = thy_path name in - case check_file NONE thy_file of - NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^ - " in dir(s) " ^ commas_quote (show_path ())) - | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE) - end; +(* theory deps *) -fun cond_add_path path f x = - if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x; - -in - -fun check_thy dir name ml = Master (cond_add_path dir check_thy_aux (name, ml)); - -fun process_thy dir f name ml = - let val master as Master ((path, _), _) = check_thy dir name ml - in (master, cond_add_path dir f path) end; - -end; +fun deps_thy dirs name ml = + let + val master as ((path, _), _) = check_thy dirs name ml; + val (name', imports, uses) = + ThyHeader.read (Position.path path) (Source.of_string (File.read path)); + val _ = name = name' orelse + error ("Filename " ^ quote (Path.implode (Path.base path)) ^ + " does not agree with theory name " ^ quote name'); + val ml_file = + if ml andalso is_some (check_file [] (ml_path name)) + then [ml_path name] else []; + in (master, (imports, map (Path.explode o #1) uses @ ml_file)) end; -(* deps_thy and load_thy *) +(* load files *) -(*hooks for theory syntax dependent operations*) -fun undefined _ = raise Match; -val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list); -val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit); +fun load_ml dirs raw_path = + (case check_ml dirs raw_path of + NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path)) + | SOME (path, id) => (ML_Context.use path; (path, id))); -fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml; -fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name ml); - +(*dependent on outer syntax*) +val load_thy_fn = ref (undefined: Path.T list -> string -> bool -> bool -> + (Path.T * File.ident) * (Path.T * File.ident) option); +fun load_thy dirs name ml time = ! load_thy_fn dirs name ml time; end;