(*  Title:      Pure/Thy/thy_load.ML

     ID:         $Id$

     Author:     Markus Wenzel, TU Muenchen

 Theory loader primitives, including load path.

 *)

 signature BASIC_THY_LOAD =

 sig

   val show_path: unit -> string list

   val add_path: string -> unit

   val path_add: string -> unit

   val del_path: string -> unit

   val with_path: string -> ('a -> 'b) -> 'a -> 'b

   val with_paths: string list -> ('a -> 'b) -> 'a -> 'b

   val reset_path: unit -> unit

 end;

 signature THY_LOAD =

 sig

   include BASIC_THY_LOAD

   val ml_exts: string list

   val ml_path: string -> Path.T

   val thy_path: string -> Path.T

   val check_file: Path.T -> Path.T -> (Path.T * File.ident) option

   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option

   val check_thy: Path.T -> string -> Path.T * File.ident

   val deps_thy: Path.T -> string ->

    {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}

   val load_ml: Path.T -> Path.T -> Path.T * File.ident

   val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit

 end;

 signature PRIVATE_THY_LOAD =

 sig

   include THY_LOAD

   (*this backdoor is sealed later*)

   val load_thy_fn: (Path.T -> string -> Position.T -> string list -> bool -> unit) ref

 end;

 structure ThyLoad: PRIVATE_THY_LOAD =

 struct

 (* maintain load path *)

 local val load_path = ref [Path.current] in

 fun show_path () = map Path.implode (! load_path);

 fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s)));

 fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s))));

 fun path_add s =

   CRITICAL (fn () => (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 =

   CRITICAL (fn () => Library.setmp load_path (! load_path @ map Path.explode ss) f x);

 fun with_path s f x = with_paths [s] f x;

 fun search_path dir path =

   distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));

 end;

 (* file formats *)

 val ml_exts = ["ML", "sml"];

 val ml_path = Path.ext "ML" o Path.basic;

 val thy_path = Path.ext "thy" o Path.basic;

 (* check files *)

 fun check_ext exts paths dir src_path =

   let

     val path = Path.expand src_path;

     val _ = Path.is_current path andalso error "Bad file specification";

     fun try_ext rel_path ext =

       let val ext_path = Path.expand (Path.ext ext rel_path)

       in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;

     fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);

   in get_first try_prfx paths end;

 fun check_file dir path = check_ext [] (search_path dir path) dir path;

 fun check_ml dir path = check_ext ml_exts (search_path dir path) dir path;

 fun check_thy dir name =

   let

     val thy_file = thy_path name;

     val paths = search_path dir thy_file;

   in

     (case check_ext [] paths dir thy_file of

       NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^

         " in " ^ commas_quote (map Path.implode paths))

     | SOME thy_id => thy_id)

   end;

 (* theory deps *)

 fun deps_thy dir name =

   let

     val master as (path, _) = check_thy dir name;

     val text = explode (File.read path);

     val (name', imports, uses) =

       ThyHeader.read (Position.path path) (Source.of_list_limited 8000 text);

     val _ = name = name' orelse

       error ("Filename " ^ quote (Path.implode (Path.base path)) ^

         " does not agree with theory name " ^ quote name');

     val uses = map (Path.explode o #1) uses;

   in {master = master, text = text, imports = imports, uses = uses} end;

 (* load files *)

 fun load_ml dir raw_path =

   (case check_ml dir raw_path of

     NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))

   | SOME (path, id) => (ML_Context.eval_file path; (path, id)));

 (*dependent on outer syntax*)

 val load_thy_fn =

   ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> unit);

 fun load_thy dir name pos text time = ! load_thy_fn dir name pos text time;

 end;

 structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;

 open BasicThyLoad;