simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
authorwenzelm
Wed Aug 08 23:07:48 2007 +0200 (2007-08-08)
changeset 241891fa9852643a3
parent 24188 d5960310c4d5
child 24190 b400ec231fde
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Aug 08 23:07:47 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Aug 08 23:07:48 2007 +0200
     1.3 @@ -692,14 +692,14 @@
     1.4  
     1.5          fun filerefs f =
     1.6              let val thy = thy_name f
     1.7 -                val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy true)
     1.8 +                val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
     1.9              in
    1.10                  issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
    1.11                                       name=NONE, idtables=[], fileurls=filerefs})
    1.12              end
    1.13  
    1.14          fun thyrefs thy =
    1.15 -            let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy true)
    1.16 +            let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
    1.17              in
    1.18                  issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
    1.19                                       name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
     2.1 --- a/src/Pure/Thy/thy_load.ML	Wed Aug 08 23:07:47 2007 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Aug 08 23:07:48 2007 +0200
     2.3 @@ -24,19 +24,18 @@
     2.4    val thy_path: string -> Path.T
     2.5    val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
     2.6    val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
     2.7 -  val check_thy: Path.T -> string -> bool -> (Path.T * File.ident) * (Path.T * File.ident) option
     2.8 -  val deps_thy: Path.T -> string -> bool ->
     2.9 -   {master: (Path.T * File.ident) * (Path.T * File.ident) option,
    2.10 -    text: string list, imports: string list, uses: Path.T list}
    2.11 +  val check_thy: Path.T -> string -> Path.T * File.ident
    2.12 +  val deps_thy: Path.T -> string ->
    2.13 +   {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
    2.14    val load_ml: Path.T -> Path.T -> Path.T * File.ident
    2.15 -  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> bool -> unit
    2.16 +  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit
    2.17  end;
    2.18  
    2.19  signature PRIVATE_THY_LOAD =
    2.20  sig
    2.21    include THY_LOAD
    2.22    (*this backdoor is sealed later*)
    2.23 -  val load_thy_fn: (Path.T -> string -> Position.T -> string list -> bool -> bool -> unit) ref
    2.24 +  val load_thy_fn: (Path.T -> string -> Position.T -> string list -> bool -> unit) ref
    2.25  end;
    2.26  
    2.27  structure ThyLoad: PRIVATE_THY_LOAD =
    2.28 @@ -88,7 +87,7 @@
    2.29  fun check_file dir path = check_ext [] (search_path dir path) dir path;
    2.30  fun check_ml dir path = check_ext ml_exts (search_path dir path) dir path;
    2.31  
    2.32 -fun check_thy dir name ml =
    2.33 +fun check_thy dir name =
    2.34    let
    2.35      val thy_file = thy_path name;
    2.36      val paths = search_path dir thy_file;
    2.37 @@ -96,25 +95,22 @@
    2.38      (case check_ext [] paths dir thy_file of
    2.39        NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
    2.40          " in " ^ commas_quote (map Path.implode paths))
    2.41 -    | SOME thy_id => (thy_id, if ml then check_file dir (ml_path name) else NONE))
    2.42 +    | SOME thy_id => thy_id)
    2.43    end;
    2.44  
    2.45  
    2.46  (* theory deps *)
    2.47  
    2.48 -fun deps_thy dir name ml =
    2.49 +fun deps_thy dir name =
    2.50    let
    2.51 -    val master as ((path, _), _) = check_thy dir name ml;
    2.52 +    val master as (path, _) = check_thy dir name;
    2.53      val text = explode (File.read path);
    2.54      val (name', imports, uses) =
    2.55        ThyHeader.read (Position.path path) (Source.of_list_limited 8000 text);
    2.56      val _ = name = name' orelse
    2.57        error ("Filename " ^ quote (Path.implode (Path.base path)) ^
    2.58          " does not agree with theory name " ^ quote name');
    2.59 -    val ml_file =
    2.60 -      if ml andalso is_some (check_file dir (ml_path name))
    2.61 -      then [ml_path name] else [];
    2.62 -    val uses = map (Path.explode o #1) uses @ ml_file;
    2.63 +    val uses = map (Path.explode o #1) uses;
    2.64    in {master = master, text = text, imports = imports, uses = uses} end;
    2.65  
    2.66  
    2.67 @@ -127,8 +123,8 @@
    2.68  
    2.69  (*dependent on outer syntax*)
    2.70  val load_thy_fn =
    2.71 -  ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> bool -> unit);
    2.72 -fun load_thy dir name pos text ml time = ! load_thy_fn dir name pos text ml time;
    2.73 +  ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> unit);
    2.74 +fun load_thy dir name pos text time = ! load_thy_fn dir name pos text time;
    2.75  
    2.76  end;
    2.77