moved call of store_theory to end of use t.thy; use t.ML;
authorclasohm
Tue Nov 16 14:23:19 1993 +0100 (1993-11-16)
changeset 1230a2f744e008a
parent 122 db9043a8e372
child 124 858ab9a9b047
moved call of store_theory to end of use t.thy; use t.ML;
use_thy now needs the exact theory name (capital/lower letters);
improved handling of incompletly read theories;
added function unlink_thy, removed function relations;
added reference variable delete_tmpfile;
removed some bugs
src/Pure/Thy/read.ML
src/Pure/Thy/syntax.ML
     1.1 --- a/src/Pure/Thy/read.ML	Tue Nov 16 14:13:11 1993 +0100
     1.2 +++ b/src/Pure/Thy/read.ML	Tue Nov 16 14:23:19 1993 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/Thy/read
     1.5      ID:         $Id$
     1.6      Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
     1.7 -    Copyright   1992  TU Muenchen
     1.8 +    Copyright   1993  TU Muenchen
     1.9  
    1.10  Reading and writing the theory definition files.
    1.11  
    1.12 @@ -10,39 +10,43 @@
    1.13                  and it then tries to read XXX.ML
    1.14  *)
    1.15  
    1.16 +datatype thy_info = ThyInfo of {name: string, path: string,
    1.17 +                                children: string list,
    1.18 +                                thy_info: string option, ml_info: string option,
    1.19 +                                theory: Thm.theory option};
    1.20 +
    1.21  signature READTHY =
    1.22  sig
    1.23 -  type thy_info
    1.24 -  datatype BaseType = Thy  of string
    1.25 +  datatype basetype = Thy  of string
    1.26                      | File of string
    1.27  
    1.28 +  val loadpath       : string list ref
    1.29 +  val delete_tmpfiles: bool ref
    1.30 +
    1.31    val use_thy        : string -> unit
    1.32    val update         : unit -> unit
    1.33    val time_use_thy   : string -> unit
    1.34 -  val base_on        : BaseType list -> string -> Thm.theory
    1.35 +  val unlink_thy     : string -> unit
    1.36 +  val base_on        : basetype list -> string -> Thm.theory
    1.37    val store_theory   : string -> Thm.theory -> unit
    1.38    val list_loaded    : unit -> thy_info list
    1.39    val set_loaded     : thy_info list -> unit
    1.40 -  val set_loadpath   : string list -> unit
    1.41 -  val relations      : string -> unit
    1.42  end;
    1.43  
    1.44  
    1.45  functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY =
    1.46  struct
    1.47  
    1.48 -datatype thy_info = ThyInfo of {name: string, children: string list, 
    1.49 -                                thy_info: string, ml_info: string, 
    1.50 -                                theory: Thm.theory};
    1.51 -
    1.52 -datatype BaseType = Thy  of string
    1.53 +datatype basetype = Thy  of string
    1.54                    | File of string;
    1.55  
    1.56 -val loaded_thys = ref [ThyInfo {name = "pure", children = [], thy_info = "",
    1.57 -                       ml_info = "", theory = Thm.pure_thy}];
    1.58 +val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [], 
    1.59 +                                thy_info = Some "", ml_info = Some "", 
    1.60 +                                theory = Some Thm.pure_thy}];
    1.61  
    1.62 -val loadpath = ref ["."];
    1.63 +val loadpath = ref ["."];           (*default search path for theory files *)
    1.64  
    1.65 +val delete_tmpfiles = ref true;         (*remove temporary files after use *)
    1.66  
    1.67  (*Make name of the output ML file for a theory *)
    1.68  fun out_name thy = "." ^ thy ^ ".thy.ML";
    1.69 @@ -60,7 +64,56 @@
    1.70    let val instream = open_in file in close_in instream; true end
    1.71      handle Io _ => false;
    1.72  
    1.73 -exception FILE_NOT_FOUND; (*raised by find_file *)
    1.74 +(*Get thy_info for a loaded theory *)
    1.75 +fun get_thyinfo thy =
    1.76 +  let fun do_search (t :: loaded : thy_info list) =
    1.77 +            let val ThyInfo {name, ...} = t
    1.78 +            in if name = thy then Some t else do_search loaded end
    1.79 +        | do_search [] = None
    1.80 +  in do_search (!loaded_thys) end;
    1.81 +
    1.82 +(*Replace an item by the result of make_change *)
    1.83 +fun change_thyinfo make_change =
    1.84 +  let fun search (t :: loaded) =
    1.85 +            let val ThyInfo {name, path, children, thy_info, ml_info,
    1.86 +                             theory} = t
    1.87 +                val (new_t, continue) = make_change name path children thy_info
    1.88 +                                                    ml_info theory
    1.89 +            in if continue then            
    1.90 +                 new_t :: (search loaded)
    1.91 +               else
    1.92 +                 new_t :: loaded
    1.93 +            end
    1.94 +        | search [] = []
    1.95 +  in loaded_thys := search (!loaded_thys) end;
    1.96 +
    1.97 +(*Check if a theory was already loaded *)
    1.98 +fun already_loaded thy =
    1.99 +  let val t = get_thyinfo thy
   1.100 +  in if is_none t then false
   1.101 +     else let val ThyInfo {thy_info, ml_info, ...} = the t
   1.102 +          in if is_none thy_info orelse is_none ml_info then false 
   1.103 +             else true end
   1.104 +  end;
   1.105 +
   1.106 +(*Check if a theory file has changed since its last use.
   1.107 +  Return a pair of boolean values for .thy and for .ML *)
   1.108 +fun thy_unchanged thy thy_file ml_file = 
   1.109 +  let val t = get_thyinfo thy
   1.110 +  in if is_some t then
   1.111 +       let val ThyInfo {thy_info, ml_info, ...} = the t
   1.112 +           val tn = is_none thy_info;
   1.113 +           val mn = is_none ml_info
   1.114 +       in if not tn andalso not mn then
   1.115 +              ((file_info thy_file = the thy_info), 
   1.116 +               (file_info ml_file = the ml_info))
   1.117 +          else if not tn andalso mn then (true, false)
   1.118 +          else (false, false)
   1.119 +       end
   1.120 +     else (false, false)
   1.121 +  end;
   1.122 +
   1.123 +exception FILE_NOT_FOUND;   (*raised by find_file *)
   1.124  
   1.125  (*Find a file using a list of paths if no absolute or relative path is
   1.126    specified.*)
   1.127 @@ -70,41 +123,85 @@
   1.128                      tack_on curr name
   1.129                  else 
   1.130                      find_it paths
   1.131 -           | find_it [] = raise FILE_NOT_FOUND
   1.132 +           | find_it [] = ""
   1.133        in find_it (!loadpath) end
   1.134    | find_file path name =
   1.135        if file_exists (tack_on path name) then tack_on path name
   1.136 -                                         else raise FILE_NOT_FOUND;
   1.137 +                                         else "";
   1.138 +
   1.139 +(*Get absolute pathnames for a new or already loaded theory *)
   1.140 +fun get_filenames path name =
   1.141 +  let fun new_filename () =
   1.142 +        let val thyl = to_lower name;
   1.143 +            val found = find_file path (thyl ^ ".thy")
   1.144 +                        handle FILE_NOT_FOUND => "";
   1.145 +            val thy_file = if found = "" then "" else tack_on (pwd ()) found;
   1.146 +            val (thy_path, _) = split_filename thy_file;
   1.147 +            val found = find_file path (thyl ^ ".ML");
   1.148 +            val ml_file = if thy_file = ""
   1.149 +                          then if found = "" then "" else tack_on (pwd ()) found
   1.150 +                          else if file_exists (tack_on thy_path (thyl ^ ".ML"))
   1.151 +                          then tack_on thy_path (thyl ^ ".ML")
   1.152 +                          else ""
   1.153 +        in if thy_file = "" andalso ml_file = "" then
   1.154 +             error ("Could find no .thy or .ML file for theory " ^ name)
   1.155 +           else ();
   1.156 +           (thy_file, ml_file) 
   1.157 +        end;
   1.158  
   1.159 -(*Check if a theory was already loaded *)
   1.160 -fun already_loaded thy =
   1.161 -  let fun do_search ((ThyInfo {name, ...}) :: loaded) =
   1.162 -              if name = thy then true else do_search loaded
   1.163 -        | do_search [] = false
   1.164 -  in do_search (!loaded_thys) end;
   1.165 +      val thy = get_thyinfo name
   1.166 +  in if is_some thy then
   1.167 +       let val thyl = to_lower name;
   1.168 +           val ThyInfo {path = abs_path, ...} = the thy;
   1.169 +           val (thy_file, ml_file) = if abs_path = "" then new_filename ()
   1.170 +                                     else (find_file abs_path (thyl ^ ".thy"),
   1.171 +                                           find_file abs_path (thyl ^ ".ML"))
   1.172 +       in if thy_file = "" andalso ml_file = "" then
   1.173 +            (writeln ("Warning: File \"" ^ (tack_on path thyl)
   1.174 +                      ^ ".thy\"\ncontaining theory \"" ^ name
   1.175 +                      ^ "\" no longer exists.");
   1.176 +             new_filename ()
   1.177 +            )
   1.178 +          else (thy_file, ml_file)
   1.179 +       end
   1.180 +     else new_filename ()
   1.181 +  end;
   1.182  
   1.183 -(*Get thy_info for a loaded theory *)
   1.184 -fun get_thyinfo thy =
   1.185 -  let fun do_search (t :: loaded : thy_info list) =
   1.186 +(*Remove theory from all child lists in loaded_thys *)
   1.187 +fun unlink_thy thy =
   1.188 +  let fun remove name path children thy_info ml_info theory =
   1.189 +            (ThyInfo {name = name, path = path, children = children \ thy, 
   1.190 +                      thy_info = thy_info, ml_info = ml_info,
   1.191 +                      theory = theory}, true)
   1.192 +  in change_thyinfo remove end;
   1.193 +
   1.194 +(*Remove a theory from loaded_thys *)
   1.195 +fun remove_thy thy =
   1.196 +  let fun remove (t :: ts) =
   1.197              let val ThyInfo {name, ...} = t
   1.198 -            in if name = thy then t else do_search loaded end
   1.199 -        | do_search [] = error ("Internal error (get_thyinfo): theory " 
   1.200 -                                ^ thy ^ " not found.")
   1.201 -  in do_search (!loaded_thys) end;
   1.202 +            in if name = thy then ts
   1.203 +                             else t :: (remove ts)
   1.204 +            end
   1.205 +        | remove [] = []
   1.206 +  in loaded_thys := remove (!loaded_thys) end;
   1.207  
   1.208 -(*Check if a theory file has changed since its last use.
   1.209 -  Return a pair of boolean values for .thy and for .ML *)
   1.210 -fun thy_unchanged thy thy_file ml_file = 
   1.211 -      if already_loaded thy then 
   1.212 -        let val ThyInfo {thy_info, ml_info, ...} = get_thyinfo thy
   1.213 -        in ((file_info (thy_file) = thy_info), (file_info (ml_file) = ml_info))
   1.214 -        end
   1.215 -      else (false, false);
   1.216 +(*Change thy_info and ml_info for an existent item *)
   1.217 +fun set_info thy_new ml_new thy =
   1.218 +  let fun change name path children thy_info ml_info theory =
   1.219 +        if name = thy then
   1.220 +            (ThyInfo {name = name, path = path, children = children,
   1.221 +                      thy_info = Some thy_new, ml_info = Some ml_new,
   1.222 +                      theory = theory}, false)
   1.223 +        else
   1.224 +            (ThyInfo {name = name, path = path, children = children,
   1.225 +                      thy_info = thy_info, ml_info = ml_info,
   1.226 +                      theory = theory}, true)
   1.227 +  in change_thyinfo change end;
   1.228  
   1.229 -(*Get theory object for a loaded theory *)
   1.230 -fun get_theory name =
   1.231 -  let val ThyInfo {theory, ...} = get_thyinfo name
   1.232 -  in theory end;
   1.233 +(*Mark theory as changed since last read if it has been completly read *)
   1.234 +fun mark_outdated thy =
   1.235 +  if already_loaded thy then set_info "" "" thy
   1.236 +                        else ();
   1.237  
   1.238  (*Read .thy and .ML files that haven't been read yet or have changed since 
   1.239    they were last read;
   1.240 @@ -113,60 +210,34 @@
   1.241    If a theory changed since its last use its children are marked as changed *)
   1.242  fun use_thy name =
   1.243      let val (path, thy_name) = split_filename name;
   1.244 -        val thy = to_lower thy_name;
   1.245 -        val thy_file = (find_file path (thy ^ ".thy")
   1.246 -                        handle FILE_NOT_FOUND => "");
   1.247 -        val (thy_path, _) = split_filename thy_file;
   1.248 -        val ml_file = if thy_file = ""
   1.249 -                      then (find_file path (thy ^ ".ML")
   1.250 -                            handle FILE_NOT_FOUND => 
   1.251 -                             error ("Could find no .thy or .ML file for theory "
   1.252 -                                    ^ thy_name))
   1.253 -                      else if file_exists (thy_path ^ thy ^ ".ML")
   1.254 -                      then thy_path ^ thy ^ ".ML"
   1.255 -                      else ""
   1.256 -        val (thy_uptodate, ml_uptodate) = thy_unchanged thy thy_file ml_file;
   1.257 +        val thyl = to_lower thy_name;
   1.258 +        val (thy_file, ml_file) = get_filenames path thy_name;
   1.259 +        val (abs_path, _) = if thy_file = "" then split_filename ml_file
   1.260 +                            else split_filename thy_file;
   1.261 +        val (thy_uptodate, ml_uptodate) = thy_unchanged thy_name 
   1.262 +                                                        thy_file ml_file;
   1.263  
   1.264 -        (*Remove theory from all child lists in loaded_thys.
   1.265 -          Afterwards add_child should be called for the (new) base theories *)
   1.266 -        fun remove_child thy =
   1.267 -          let fun do_remove (ThyInfo {name, children, thy_info, ml_info, theory}
   1.268 -                            :: loaded) result =
   1.269 -                    do_remove loaded 
   1.270 -                      (ThyInfo {name = name, children = children \ thy, 
   1.271 -                                thy_info = thy_info, ml_info = ml_info,
   1.272 -                                theory = theory} :: result)
   1.273 -                | do_remove [] result = result;
   1.274 -          in loaded_thys := do_remove (!loaded_thys) [] end;
   1.275 -          
   1.276 -         exception THY_NOT_FOUND;  (*Raised by set_info *)
   1.277 +         (*Set absolute path for loaded theory *)
   1.278 +         fun set_path () =
   1.279 +           let fun change name path children thy_info ml_info theory =
   1.280 +                 if name = thy_name then            
   1.281 +                   (ThyInfo {name = name, path = abs_path, children = children,
   1.282 +                             thy_info = thy_info, ml_info = ml_info,
   1.283 +                             theory = theory}, false)
   1.284 +                 else
   1.285 +                   (ThyInfo {name = name, path = path, children = children,
   1.286 +                             thy_info = thy_info, ml_info = ml_info,
   1.287 +                             theory = theory}, true)
   1.288 +           in change_thyinfo change end;
   1.289  
   1.290 -         (*Change thy_info and ml_info for an existent item or create
   1.291 -           a new item with empty child list *)
   1.292 -         fun set_info thy_new ml_new thy =
   1.293 -               let fun make_change (t :: loaded) =
   1.294 -                         let val ThyInfo {name, children, theory, ...} = t
   1.295 -                         in if name = thy then            
   1.296 -                              ThyInfo {name = name, children = children,
   1.297 -                                       thy_info = thy_new, ml_info = ml_new,
   1.298 -                                       theory = theory} :: loaded
   1.299 -                            else
   1.300 -                              t :: (make_change loaded)
   1.301 -                         end
   1.302 -                     | make_change [] = raise THY_NOT_FOUND
   1.303 -               in loaded_thys := make_change (!loaded_thys) end;
   1.304 -
   1.305 -         (*Mark all direct and indirect descendants of a theory as changed *)
   1.306 +         (*Mark all direct descendants of a theory as changed *)
   1.307           fun mark_children thy =
   1.308 -           let val ThyInfo {children, ...} = get_thyinfo thy
   1.309 +           let val ThyInfo {children, ...} = the (get_thyinfo thy)
   1.310             in if children <> [] then
   1.311                    (writeln ("The following children of theory " ^ (quote thy)
   1.312 -                            ^ " are now out-of-date: \""
   1.313 -                            ^ (space_implode "\",\"" children) ^ "\"");
   1.314 -                   seq (set_info "" "") children
   1.315 -                   handle THY_NOT_FOUND => ()
   1.316 -                        (*If this theory was automatically loaded by a child 
   1.317 -                          then the child cannot be found in loaded_thys *)
   1.318 +                            ^ " are now out-of-date: "
   1.319 +                            ^ (quote (space_implode "\",\"" children)));
   1.320 +                   seq mark_outdated children
   1.321                    )
   1.322                else ()
   1.323             end
   1.324 @@ -175,43 +246,32 @@
   1.325         else
   1.326         (
   1.327           writeln ("Loading theory " ^ (quote name));
   1.328 -         if thy_uptodate orelse (thy_file = "") then ()
   1.329 -         else
   1.330 -         (
   1.331 -             (*Allow dependency lists to be rebuild completely *)
   1.332 -             remove_child thy;
   1.333 -                
   1.334 -             read_thy thy thy_file
   1.335 -         );
   1.336 +         if thy_uptodate orelse thy_file = "" then ()
   1.337 +         else (read_thy thyl thy_file;
   1.338 +               use (out_name thyl)
   1.339 +              );
   1.340           
   1.341 -         (*Actually read files!*)
   1.342 -         if thy_uptodate orelse (thy_file = "") then ()
   1.343 -                         else use (out_name thy);
   1.344 -         if (thy_file = "") then          (*theory object created in .ML file*)
   1.345 -             (
   1.346 -                 use ml_file;
   1.347 -                 let val outstream = open_out (".tmp.ML") 
   1.348 -                 in
   1.349 -                    output (outstream, "store_theory " ^ quote thy_name ^ " "
   1.350 -                                       ^ thy_name ^ ".thy;\n");
   1.351 -                    close_out outstream 
   1.352 -                 end;
   1.353 -                 use ".tmp.ML";
   1.354 -                 delete_file ".tmp.ML"
   1.355 -             )
   1.356 -         else if ml_file <> "" then use ml_file
   1.357 -         else ();
   1.358 +         if ml_file = "" then () else use ml_file;
   1.359 +
   1.360 +         let val outstream = open_out ".tmp.ML"
   1.361 +         in
   1.362 +             output (outstream, "store_theory " ^ quote thy_name ^ " "
   1.363 +                                ^ thy_name ^ ".thy;\n");
   1.364 +             close_out outstream 
   1.365 +         end;
   1.366 +         use ".tmp.ML";
   1.367 +         delete_file ".tmp.ML";
   1.368  
   1.369           (*Now set the correct info.*)
   1.370 -         (set_info (file_info thy_file) (file_info ml_file) thy
   1.371 -          handle THY_NOT_FOUND => error ("Could not find theory \"" ^ thy
   1.372 -                                         ^ "\" (wrong filename?)"));
   1.373 +         set_info (file_info thy_file) (file_info ml_file) thy_name;
   1.374 +         set_path ();
   1.375  
   1.376           (*Mark theories that have to be reloaded.*)
   1.377 -         mark_children thy;
   1.378 +         mark_children thy_name;
   1.379  
   1.380 -         delete_file (out_name thy)
   1.381 -       )
   1.382 +         if !delete_tmpfiles then delete_file (out_name thyl)
   1.383 +                            else ()
   1.384 +        )
   1.385      end;
   1.386  
   1.387  fun time_use_thy tname = timeit(fn()=>
   1.388 @@ -227,8 +287,12 @@
   1.389        fun load_order [] result = result
   1.390          | load_order thys result =
   1.391              let fun next_level (t :: ts) =
   1.392 -                      let val ThyInfo {children, ...} = get_thyinfo t
   1.393 -                      in children union (next_level ts)
   1.394 +                      let val thy = get_thyinfo t
   1.395 +                      in if is_some thy then
   1.396 +                             let val ThyInfo {children, ...} = the thy
   1.397 +                             in children union (next_level ts)
   1.398 +                             end
   1.399 +                         else []
   1.400                        end
   1.401                    | next_level [] = [];
   1.402                    
   1.403 @@ -236,123 +300,150 @@
   1.404              in load_order children ((result \\ children) @ children) end;
   1.405  
   1.406        fun reload_changed (t :: ts) =
   1.407 -            let val curr = get_thyinfo t;
   1.408 -                val thy_file = (find_file "" (t ^ ".thy")
   1.409 -                                handle FILE_NOT_FOUND => "");
   1.410 -                val (thy_path, _) = split_filename thy_file;
   1.411 -                val ml_file = if thy_file = ""
   1.412 -                              then (find_file "" (t ^ ".ML")
   1.413 -                                    handle FILE_NOT_FOUND => 
   1.414 -                             error ("Could find no .thy or .ML file for theory "
   1.415 -                                    ^ t))
   1.416 -                              else if file_exists (thy_path ^ t ^ ".ML")
   1.417 -                              then thy_path ^ t ^ ".ML"
   1.418 -                              else ""
   1.419 +            let val thy = get_thyinfo t;
   1.420 +
   1.421 +                fun abspath () =
   1.422 +                  if is_some thy then
   1.423 +                    let val ThyInfo {path, ...} = the thy in path end
   1.424 +                  else "";
   1.425 +
   1.426 +                val (thy_file, ml_file) = get_filenames (abspath ()) t;
   1.427                  val (thy_uptodate, ml_uptodate) =
   1.428 -                      thy_unchanged t thy_file ml_file;
   1.429 - 
   1.430 +                        thy_unchanged t thy_file ml_file;
   1.431              in if thy_uptodate andalso ml_uptodate then ()
   1.432                                                     else use_thy t;
   1.433                 reload_changed ts
   1.434              end
   1.435 -        | reload_changed [] = ()
   1.436 -  in reload_changed (load_order ["pure"] []) end;
   1.437 +        | reload_changed [] = ();
   1.438 +
   1.439 +     (*Remove all theories that are no descendants of Pure.
   1.440 +       If there are still children in the deleted theory's list
   1.441 +       schedule them for reloading *)
   1.442 +     fun collect_garbage not_garbage =
   1.443 +       let fun collect (t :: ts) =
   1.444 +                 let val ThyInfo {name, children, ...} = t
   1.445 +                 in if name mem not_garbage then collect ts
   1.446 +                    else (writeln("Theory \"" ^ name 
   1.447 +                           ^ "\" is no longer linked with Pure - removing it.");
   1.448 +                          remove_thy name;
   1.449 +                          seq mark_outdated children
   1.450 +                         )
   1.451 +                 end
   1.452 +             | collect [] = ()
   1.453 +
   1.454 +       in collect (!loaded_thys) end
   1.455 +
   1.456 +  in collect_garbage ("Pure" :: (load_order ["Pure"] []));
   1.457 +     reload_changed (load_order ["Pure"] [])
   1.458 +  end;
   1.459  
   1.460  (*Merge theories to build a base for a new theory.
   1.461    Base members are only loaded if they are missing. *)
   1.462  fun base_on bases child =
   1.463 -      let val childl = to_lower child;
   1.464 -
   1.465 -          (*List all descendants of a theory list *)
   1.466 +      let (*List all descendants of a theory list *)
   1.467            fun list_descendants (t :: ts) =
   1.468 -                if already_loaded t then
   1.469 -                  let val ThyInfo {children, ...} = get_thyinfo t
   1.470 -                  in children union 
   1.471 -                     (list_descendants (ts union children))
   1.472 -                  end
   1.473 -                else []
   1.474 +                let val tinfo = get_thyinfo t
   1.475 +                in if is_some tinfo then
   1.476 +                     let val ThyInfo {children, ...} = the tinfo
   1.477 +                     in children union (list_descendants (ts union children))
   1.478 +                     end
   1.479 +                   else []
   1.480 +                end
   1.481              | list_descendants [] = [];
   1.482  
   1.483            (*Show the cycle that would be created by add_child *)
   1.484            fun show_cycle base =
   1.485              let fun find_it result curr =
   1.486 -                  if base = curr then 
   1.487 -                      error ("Cyclic dependency of theories: "
   1.488 -                             ^ childl ^ "->" ^ base ^ result)
   1.489 -                  else if already_loaded curr then
   1.490 -                    let val ThyInfo {children, ...} = get_thyinfo curr
   1.491 -                    in seq (find_it ("->" ^ curr ^ result)) children
   1.492 -                    end
   1.493 -                  else ()
   1.494 -            in find_it "" childl end;
   1.495 +                  let val tinfo = get_thyinfo curr
   1.496 +                  in if base = curr then 
   1.497 +                       error ("Cyclic dependency of theories: "
   1.498 +                              ^ child ^ "->" ^ base ^ result)
   1.499 +                     else if is_some tinfo then
   1.500 +                       let val ThyInfo {children, ...} = the tinfo
   1.501 +                       in seq (find_it ("->" ^ curr ^ result)) children
   1.502 +                       end
   1.503 +                     else ()
   1.504 +                  end
   1.505 +            in find_it "" child end;
   1.506          
   1.507            (*Check if a cycle will be created by add_child *)
   1.508            fun find_cycle base =
   1.509 -            if base mem (list_descendants [childl]) then show_cycle base
   1.510 +            if base mem (list_descendants [child]) then show_cycle base
   1.511              else ();
   1.512                     
   1.513            (*Add child to child list of base *)
   1.514 -          fun add_child (t :: loaded) base =
   1.515 -                let val ThyInfo {name, children, thy_info, ml_info, theory} = t
   1.516 -                in if name = base then
   1.517 -                     ThyInfo {name = name, 
   1.518 -                              children = childl ins children,
   1.519 -                              thy_info = thy_info, ml_info = ml_info,
   1.520 -                              theory = theory} :: loaded
   1.521 -                   else
   1.522 -                     t :: (add_child loaded base)
   1.523 -                end
   1.524 -           | add_child [] base =
   1.525 -               [ThyInfo {name = base, children = [childl], 
   1.526 -                         thy_info = "", ml_info = "",
   1.527 -                         theory = Thm.pure_thy}];
   1.528 -                                            (*Thm.pure_thy is used as a dummy *)
   1.529 +          fun add_child base =
   1.530 +            let fun add (t :: loaded) =
   1.531 +                      let val ThyInfo {name, path, children,
   1.532 +                                       thy_info, ml_info, theory} = t
   1.533 +                      in if name = base then
   1.534 +                           ThyInfo {name = name, path = path,
   1.535 +                                    children = child ins children,
   1.536 +                                    thy_info = thy_info, ml_info = ml_info,
   1.537 +                                    theory = theory} :: loaded
   1.538 +                         else
   1.539 +                           t :: (add loaded)
   1.540 +                      end
   1.541 +                  | add [] =
   1.542 +                      [ThyInfo {name = base, path = "", children = [child], 
   1.543 +                                thy_info = None, ml_info = None, theory = None}]
   1.544 +            in loaded_thys := add (!loaded_thys) end;       
   1.545  
   1.546 -          fun do_load thy =
   1.547 -              let val basel = to_lower thy;
   1.548 -
   1.549 -                  val thy_present = already_loaded basel
   1.550 +          (*Load a base theory if not already done
   1.551 +            and no cycle would be created *)
   1.552 +          fun load base =
   1.553 +              let val thy_present = already_loaded base
   1.554                                              (*test this before child is added *)
   1.555                in
   1.556 -                if childl = basel then
   1.557 +                if child = base then
   1.558                      error ("Cyclic dependency of theories: " ^ child
   1.559                             ^ "->" ^ child)
   1.560                  else 
   1.561 -                  (find_cycle thy;
   1.562 -                   loaded_thys := add_child (!loaded_thys) basel;
   1.563 +                  (find_cycle base;
   1.564 +                   add_child base;
   1.565                     if thy_present then ()
   1.566 -                   else (writeln ("Autoloading theory " ^ (quote thy)
   1.567 +                   else (writeln ("Autoloading theory " ^ (quote base)
   1.568                                    ^ " (used by " ^ (quote child) ^ ")");
   1.569 -                         use_thy thy)
   1.570 +                         use_thy base)
   1.571                    )
   1.572                end; 
   1.573  
   1.574 +          (*Load all needed files and make a list of all real theories *)
   1.575            fun load_base (Thy b :: bs) =
   1.576 -               (do_load b;
   1.577 -                (to_lower b) :: (load_base bs))
   1.578 +               (load b;
   1.579 +                b :: (load_base bs))
   1.580              | load_base (File b :: bs) =
   1.581 -               (do_load b;
   1.582 -                load_base bs)     (*don't add it to merge_theories' parameter *)
   1.583 +               (load b;
   1.584 +                load_base bs)    (*don't add it to merge_theories' parameter *)
   1.585              | load_base [] = [];
   1.586 -              
   1.587 -          val (t :: ts) = load_base bases
   1.588 +
   1.589 +          (*Get theory object for a loaded theory *)
   1.590 +          fun get_theory name =
   1.591 +            let val ThyInfo {theory, ...} = the (get_thyinfo name)
   1.592 +            in the theory end;
   1.593 +
   1.594 +          val mergelist = (unlink_thy child;
   1.595 +                           load_base bases);
   1.596 +          val (t :: ts) = if mergelist = [] then ["Pure"] else mergelist
   1.597 +                                               (*we have to return something *)
   1.598       in foldl Thm.merge_theories (get_theory t, map get_theory ts) end;
   1.599  
   1.600  (*Change theory object for an existent item of loaded_thys 
   1.601    or create a new item *)
   1.602  fun store_theory thy_name thy =
   1.603    let fun make_change (t :: loaded) =
   1.604 -            let val ThyInfo {name, children, thy_info, ml_info, ...} = t
   1.605 -            in if name = (to_lower thy_name) then            
   1.606 -                    ThyInfo {name = name, children = children,
   1.607 +            let val ThyInfo {name, path, children, thy_info, ml_info, ...} = t
   1.608 +            in if name = thy_name then            
   1.609 +                    ThyInfo {name = name, path = path, children = children,
   1.610                               thy_info = thy_info, ml_info = ml_info,
   1.611 -                             theory = thy} :: loaded
   1.612 +                             theory = Some thy} :: loaded
   1.613                 else
   1.614                      t :: (make_change loaded)
   1.615              end
   1.616          | make_change [] =
   1.617 -            [ThyInfo {name = (to_lower thy_name), children = [], thy_info = "", 
   1.618 -                      ml_info = "", theory = thy}]
   1.619 +            [ThyInfo {name = thy_name, path = "", children = [],
   1.620 +                      thy_info = Some "", ml_info = Some "",
   1.621 +                      theory = Some thy}]
   1.622    in loaded_thys := make_change (!loaded_thys) end;
   1.623  
   1.624  (*Create a list of all theories loaded by this structure *)
   1.625 @@ -360,22 +451,11 @@
   1.626  
   1.627  (*Change the list of loaded theories *)
   1.628  fun set_loaded [] =
   1.629 -      loaded_thys := [ThyInfo {name = "pure", children = [], thy_info = "",
   1.630 -                      ml_info = "", theory = Thm.pure_thy}]
   1.631 +      loaded_thys := [ThyInfo {name = "Pure", path = "", children = [],
   1.632 +                      thy_info = Some "", ml_info = Some "",
   1.633 +                      theory = Some Thm.pure_thy}]
   1.634    | set_loaded ts =
   1.635        loaded_thys := ts;
   1.636  
   1.637 -(*Change the path list that is to be searched for .thy and .ML files *)
   1.638 -fun set_loadpath new_path =
   1.639 -  loadpath := new_path;
   1.640 +end
   1.641  
   1.642 -(*This function is for debugging purposes only *)
   1.643 -fun relations thy =
   1.644 -  let val ThyInfo {children, ...} = get_thyinfo thy
   1.645 -  in
   1.646 -     writeln (thy ^ ": " ^ (space_implode ", " children));
   1.647 -     seq relations children
   1.648 -  end
   1.649 -
   1.650 -end;
   1.651 -
     2.1 --- a/src/Pure/Thy/syntax.ML	Tue Nov 16 14:13:11 1993 +0100
     2.2 +++ b/src/Pure/Thy/syntax.ML	Tue Nov 16 14:23:19 1993 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  signature THYSYN =
     2.6   sig
     2.7 -  datatype BaseType = Thy  of string
     2.8 +  datatype basetype = Thy  of string
     2.9                      | File of string
    2.10  
    2.11     val read: string list -> string
    2.12 @@ -115,8 +115,7 @@
    2.13      axs ^ "\n\n" ^ vals
    2.14    end;
    2.15  
    2.16 -fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n"
    2.17 -                        ^ "store_theory " ^ quote id ^ " " ^ id ^ ".thy;\n";
    2.18 +fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n";
    2.19  
    2.20  
    2.21  fun mk_sext mfix trans =
    2.22 @@ -164,7 +163,7 @@
    2.23    | mk_structure ((name, base), None) =
    2.24        mk_struct (name, "\nval thy = " ^ base ^ (quote name));
    2.25  
    2.26 -datatype BaseType = Thy  of string
    2.27 +datatype basetype = Thy  of string
    2.28                    | File of string;
    2.29  
    2.30  fun merge thys =