src/Pure/Thy/read.ML
author clasohm
Tue, 16 Nov 1993 14:23:19 +0100
changeset 123 0a2f744e008a
parent 81 4cc5a34292a9
child 126 0b0055b3ccfe
permissions -rw-r--r--
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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/read
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
     4
    Copyright   1993  TU Muenchen
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Reading and writing the theory definition files.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
For theory XXX, the  input file is called XXX.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
                the output file is called .XXX.thy.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
                and it then tries to read XXX.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    13
datatype thy_info = ThyInfo of {name: string, path: string,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    14
                                children: string list,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    15
                                thy_info: string option, ml_info: string option,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    16
                                theory: Thm.theory option};
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    17
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
signature READTHY =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
sig
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    20
  datatype basetype = Thy  of string
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
    21
                    | File of string
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    22
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    23
  val loadpath       : string list ref
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    24
  val delete_tmpfiles: bool ref
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    25
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    26
  val use_thy        : string -> unit
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    27
  val update         : unit -> unit
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val time_use_thy   : string -> unit
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    29
  val unlink_thy     : string -> unit
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    30
  val base_on        : basetype list -> string -> Thm.theory
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    31
  val store_theory   : string -> Thm.theory -> unit
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    32
  val list_loaded    : unit -> thy_info list
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    33
  val set_loaded     : thy_info list -> unit
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    37
functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    40
datatype basetype = Thy  of string
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
    41
                  | File of string;
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
    42
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    43
val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [], 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    44
                                thy_info = Some "", ml_info = Some "", 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    45
                                theory = Some Thm.pure_thy}];
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    46
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    47
val loadpath = ref ["."];           (*default search path for theory files *)
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    48
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    49
val delete_tmpfiles = ref true;         (*remove temporary files after use *)
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    50
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    51
(*Make name of the output ML file for a theory *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
fun out_name thy = "." ^ thy ^ ".thy.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    54
(*Read a file specified by thy_file containing theory thy *)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    55
fun read_thy thy thy_file =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    56
    let val instream  = open_in thy_file;
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
    57
        val outstream = open_out (out_name thy)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
    in  output (outstream, ThySyn.read (explode(input(instream, 999999))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
        close_out outstream;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
        close_in instream
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
fun file_exists file =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
  let val instream = open_in file in close_in instream; true end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
    handle Io _ => false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    67
(*Get thy_info for a loaded theory *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    68
fun get_thyinfo thy =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    69
  let fun do_search (t :: loaded : thy_info list) =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    70
            let val ThyInfo {name, ...} = t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    71
            in if name = thy then Some t else do_search loaded end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    72
        | do_search [] = None
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    73
  in do_search (!loaded_thys) end;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    74
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    75
(*Replace an item by the result of make_change *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    76
fun change_thyinfo make_change =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    77
  let fun search (t :: loaded) =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    78
            let val ThyInfo {name, path, children, thy_info, ml_info,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    79
                             theory} = t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    80
                val (new_t, continue) = make_change name path children thy_info
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    81
                                                    ml_info theory
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    82
            in if continue then            
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    83
                 new_t :: (search loaded)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    84
               else
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    85
                 new_t :: loaded
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    86
            end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    87
        | search [] = []
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    88
  in loaded_thys := search (!loaded_thys) end;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    89
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    90
(*Check if a theory was already loaded *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    91
fun already_loaded thy =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    92
  let val t = get_thyinfo thy
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    93
  in if is_none t then false
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    94
     else let val ThyInfo {thy_info, ml_info, ...} = the t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    95
          in if is_none thy_info orelse is_none ml_info then false 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    96
             else true end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    97
  end;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    98
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
    99
(*Check if a theory file has changed since its last use.
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   100
  Return a pair of boolean values for .thy and for .ML *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   101
fun thy_unchanged thy thy_file ml_file = 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   102
  let val t = get_thyinfo thy
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   103
  in if is_some t then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   104
       let val ThyInfo {thy_info, ml_info, ...} = the t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   105
           val tn = is_none thy_info;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   106
           val mn = is_none ml_info
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   107
       in if not tn andalso not mn then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   108
              ((file_info thy_file = the thy_info), 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   109
               (file_info ml_file = the ml_info))
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   110
          else if not tn andalso mn then (true, false)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   111
          else (false, false)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   112
       end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   113
     else (false, false)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   114
  end;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   115
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   116
exception FILE_NOT_FOUND;   (*raised by find_file *)
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   117
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   118
(*Find a file using a list of paths if no absolute or relative path is
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   119
  specified.*)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   120
fun find_file "" name =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   121
      let fun find_it (curr :: paths) =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   122
                if file_exists (tack_on curr name) then
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   123
                    tack_on curr name
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   124
                else 
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   125
                    find_it paths
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   126
           | find_it [] = ""
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   127
      in find_it (!loadpath) end
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   128
  | find_file path name =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   129
      if file_exists (tack_on path name) then tack_on path name
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   130
                                         else "";
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   131
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   132
(*Get absolute pathnames for a new or already loaded theory *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   133
fun get_filenames path name =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   134
  let fun new_filename () =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   135
        let val thyl = to_lower name;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   136
            val found = find_file path (thyl ^ ".thy")
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   137
                        handle FILE_NOT_FOUND => "";
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   138
            val thy_file = if found = "" then "" else tack_on (pwd ()) found;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   139
            val (thy_path, _) = split_filename thy_file;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   140
            val found = find_file path (thyl ^ ".ML");
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   141
            val ml_file = if thy_file = ""
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   142
                          then if found = "" then "" else tack_on (pwd ()) found
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   143
                          else if file_exists (tack_on thy_path (thyl ^ ".ML"))
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   144
                          then tack_on thy_path (thyl ^ ".ML")
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   145
                          else ""
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   146
        in if thy_file = "" andalso ml_file = "" then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   147
             error ("Could find no .thy or .ML file for theory " ^ name)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   148
           else ();
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   149
           (thy_file, ml_file) 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   150
        end;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   151
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   152
      val thy = get_thyinfo name
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   153
  in if is_some thy then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   154
       let val thyl = to_lower name;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   155
           val ThyInfo {path = abs_path, ...} = the thy;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   156
           val (thy_file, ml_file) = if abs_path = "" then new_filename ()
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   157
                                     else (find_file abs_path (thyl ^ ".thy"),
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   158
                                           find_file abs_path (thyl ^ ".ML"))
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   159
       in if thy_file = "" andalso ml_file = "" then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   160
            (writeln ("Warning: File \"" ^ (tack_on path thyl)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   161
                      ^ ".thy\"\ncontaining theory \"" ^ name
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   162
                      ^ "\" no longer exists.");
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   163
             new_filename ()
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   164
            )
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   165
          else (thy_file, ml_file)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   166
       end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   167
     else new_filename ()
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   168
  end;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   169
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   170
(*Remove theory from all child lists in loaded_thys *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   171
fun unlink_thy thy =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   172
  let fun remove name path children thy_info ml_info theory =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   173
            (ThyInfo {name = name, path = path, children = children \ thy, 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   174
                      thy_info = thy_info, ml_info = ml_info,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   175
                      theory = theory}, true)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   176
  in change_thyinfo remove end;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   177
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   178
(*Remove a theory from loaded_thys *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   179
fun remove_thy thy =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   180
  let fun remove (t :: ts) =
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   181
            let val ThyInfo {name, ...} = t
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   182
            in if name = thy then ts
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   183
                             else t :: (remove ts)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   184
            end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   185
        | remove [] = []
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   186
  in loaded_thys := remove (!loaded_thys) end;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   187
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   188
(*Change thy_info and ml_info for an existent item *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   189
fun set_info thy_new ml_new thy =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   190
  let fun change name path children thy_info ml_info theory =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   191
        if name = thy then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   192
            (ThyInfo {name = name, path = path, children = children,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   193
                      thy_info = Some thy_new, ml_info = Some ml_new,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   194
                      theory = theory}, false)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   195
        else
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   196
            (ThyInfo {name = name, path = path, children = children,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   197
                      thy_info = thy_info, ml_info = ml_info,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   198
                      theory = theory}, true)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   199
  in change_thyinfo change end;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   200
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   201
(*Mark theory as changed since last read if it has been completly read *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   202
fun mark_outdated thy =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   203
  if already_loaded thy then set_info "" "" thy
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   204
                        else ();
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   205
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   206
(*Read .thy and .ML files that haven't been read yet or have changed since 
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   207
  they were last read;
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   208
  loaded_thys is a thy_info list ref containing all theories that have 
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   209
  completly been read by this and preceeding use_thy calls.
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   210
  If a theory changed since its last use its children are marked as changed *)
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   211
fun use_thy name =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   212
    let val (path, thy_name) = split_filename name;
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   213
        val thyl = to_lower thy_name;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   214
        val (thy_file, ml_file) = get_filenames path thy_name;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   215
        val (abs_path, _) = if thy_file = "" then split_filename ml_file
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   216
                            else split_filename thy_file;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   217
        val (thy_uptodate, ml_uptodate) = thy_unchanged thy_name 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   218
                                                        thy_file ml_file;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   220
         (*Set absolute path for loaded theory *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   221
         fun set_path () =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   222
           let fun change name path children thy_info ml_info theory =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   223
                 if name = thy_name then            
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   224
                   (ThyInfo {name = name, path = abs_path, children = children,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   225
                             thy_info = thy_info, ml_info = ml_info,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   226
                             theory = theory}, false)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   227
                 else
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   228
                   (ThyInfo {name = name, path = path, children = children,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   229
                             thy_info = thy_info, ml_info = ml_info,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   230
                             theory = theory}, true)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   231
           in change_thyinfo change end;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   232
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   233
         (*Mark all direct descendants of a theory as changed *)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   234
         fun mark_children thy =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   235
           let val ThyInfo {children, ...} = the (get_thyinfo thy)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   236
           in if children <> [] then
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   237
                  (writeln ("The following children of theory " ^ (quote thy)
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   238
                            ^ " are now out-of-date: "
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   239
                            ^ (quote (space_implode "\",\"" children)));
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   240
                   seq mark_outdated children
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   241
                  )
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   242
              else ()
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   243
           end
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   244
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   245
    in if thy_uptodate andalso ml_uptodate then ()
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   246
       else
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   247
       (
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   248
         writeln ("Loading theory " ^ (quote name));
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   249
         if thy_uptodate orelse thy_file = "" then ()
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   250
         else (read_thy thyl thy_file;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   251
               use (out_name thyl)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   252
              );
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   253
         
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   254
         if ml_file = "" then () else use ml_file;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   255
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   256
         let val outstream = open_out ".tmp.ML"
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   257
         in
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   258
             output (outstream, "store_theory " ^ quote thy_name ^ " "
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   259
                                ^ thy_name ^ ".thy;\n");
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   260
             close_out outstream 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   261
         end;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   262
         use ".tmp.ML";
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   263
         delete_file ".tmp.ML";
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   264
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   265
         (*Now set the correct info.*)
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   266
         set_info (file_info thy_file) (file_info ml_file) thy_name;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   267
         set_path ();
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   268
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   269
         (*Mark theories that have to be reloaded.*)
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   270
         mark_children thy_name;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   271
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   272
         if !delete_tmpfiles then delete_file (out_name thyl)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   273
                            else ()
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   274
        )
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
fun time_use_thy tname = timeit(fn()=>
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   278
   (writeln("\n**** Starting Theory " ^ tname ^ " ****");  
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   279
    use_thy tname;
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   280
    writeln("\n**** Finished Theory " ^ tname ^ " ****"))
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   281
   );
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   282
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   283
(*Load all thy or ML files that have been changed and also
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   284
  all theories that depend on them *)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   285
fun update () =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   286
  let (*List theories in the order they have to be loaded *)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   287
      fun load_order [] result = result
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   288
        | load_order thys result =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   289
            let fun next_level (t :: ts) =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   290
                      let val thy = get_thyinfo t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   291
                      in if is_some thy then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   292
                             let val ThyInfo {children, ...} = the thy
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   293
                             in children union (next_level ts)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   294
                             end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   295
                         else []
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   296
                      end
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   297
                  | next_level [] = [];
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   298
                  
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   299
                val children = next_level thys
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   300
            in load_order children ((result \\ children) @ children) end;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   301
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   302
      fun reload_changed (t :: ts) =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   303
            let val thy = get_thyinfo t;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   304
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   305
                fun abspath () =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   306
                  if is_some thy then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   307
                    let val ThyInfo {path, ...} = the thy in path end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   308
                  else "";
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   309
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   310
                val (thy_file, ml_file) = get_filenames (abspath ()) t;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   311
                val (thy_uptodate, ml_uptodate) =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   312
                        thy_unchanged t thy_file ml_file;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   313
            in if thy_uptodate andalso ml_uptodate then ()
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   314
                                                   else use_thy t;
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   315
               reload_changed ts
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   316
            end
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   317
        | reload_changed [] = ();
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   318
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   319
     (*Remove all theories that are no descendants of Pure.
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   320
       If there are still children in the deleted theory's list
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   321
       schedule them for reloading *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   322
     fun collect_garbage not_garbage =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   323
       let fun collect (t :: ts) =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   324
                 let val ThyInfo {name, children, ...} = t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   325
                 in if name mem not_garbage then collect ts
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   326
                    else (writeln("Theory \"" ^ name 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   327
                           ^ "\" is no longer linked with Pure - removing it.");
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   328
                          remove_thy name;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   329
                          seq mark_outdated children
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   330
                         )
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   331
                 end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   332
             | collect [] = ()
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   333
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   334
       in collect (!loaded_thys) end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   335
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   336
  in collect_garbage ("Pure" :: (load_order ["Pure"] []));
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   337
     reload_changed (load_order ["Pure"] [])
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   338
  end;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   339
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   340
(*Merge theories to build a base for a new theory.
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   341
  Base members are only loaded if they are missing. *)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   342
fun base_on bases child =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   343
      let (*List all descendants of a theory list *)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   344
          fun list_descendants (t :: ts) =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   345
                let val tinfo = get_thyinfo t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   346
                in if is_some tinfo then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   347
                     let val ThyInfo {children, ...} = the tinfo
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   348
                     in children union (list_descendants (ts union children))
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   349
                     end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   350
                   else []
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   351
                end
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   352
            | list_descendants [] = [];
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   353
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   354
          (*Show the cycle that would be created by add_child *)
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   355
          fun show_cycle base =
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   356
            let fun find_it result curr =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   357
                  let val tinfo = get_thyinfo curr
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   358
                  in if base = curr then 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   359
                       error ("Cyclic dependency of theories: "
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   360
                              ^ child ^ "->" ^ base ^ result)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   361
                     else if is_some tinfo then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   362
                       let val ThyInfo {children, ...} = the tinfo
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   363
                       in seq (find_it ("->" ^ curr ^ result)) children
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   364
                       end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   365
                     else ()
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   366
                  end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   367
            in find_it "" child end;
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   368
        
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   369
          (*Check if a cycle will be created by add_child *)
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   370
          fun find_cycle base =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   371
            if base mem (list_descendants [child]) then show_cycle base
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   372
            else ();
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   373
                   
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   374
          (*Add child to child list of base *)
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   375
          fun add_child base =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   376
            let fun add (t :: loaded) =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   377
                      let val ThyInfo {name, path, children,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   378
                                       thy_info, ml_info, theory} = t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   379
                      in if name = base then
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   380
                           ThyInfo {name = name, path = path,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   381
                                    children = child ins children,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   382
                                    thy_info = thy_info, ml_info = ml_info,
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   383
                                    theory = theory} :: loaded
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   384
                         else
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   385
                           t :: (add loaded)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   386
                      end
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   387
                  | add [] =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   388
                      [ThyInfo {name = base, path = "", children = [child], 
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   389
                                thy_info = None, ml_info = None, theory = None}]
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   390
            in loaded_thys := add (!loaded_thys) end;       
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   391
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   392
          (*Load a base theory if not already done
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   393
            and no cycle would be created *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   394
          fun load base =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   395
              let val thy_present = already_loaded base
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   396
                                            (*test this before child is added *)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   397
              in
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   398
                if child = base then
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   399
                    error ("Cyclic dependency of theories: " ^ child
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   400
                           ^ "->" ^ child)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   401
                else 
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   402
                  (find_cycle base;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   403
                   add_child base;
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   404
                   if thy_present then ()
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   405
                   else (writeln ("Autoloading theory " ^ (quote base)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   406
                                  ^ " (used by " ^ (quote child) ^ ")");
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   407
                         use_thy base)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   408
                  )
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   409
              end; 
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   410
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   411
          (*Load all needed files and make a list of all real theories *)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   412
          fun load_base (Thy b :: bs) =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   413
               (load b;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   414
                b :: (load_base bs))
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   415
            | load_base (File b :: bs) =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   416
               (load b;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   417
                load_base bs)    (*don't add it to merge_theories' parameter *)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   418
            | load_base [] = [];
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   419
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   420
          (*Get theory object for a loaded theory *)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   421
          fun get_theory name =
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   422
            let val ThyInfo {theory, ...} = the (get_thyinfo name)
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   423
            in the theory end;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   424
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   425
          val mergelist = (unlink_thy child;
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   426
                           load_base bases);
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   427
          val (t :: ts) = if mergelist = [] then ["Pure"] else mergelist
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   428
                                               (*we have to return something *)
81
4cc5a34292a9 corrected some spelling mistakes;
clasohm
parents: 78
diff changeset
   429
     in foldl Thm.merge_theories (get_theory t, map get_theory ts) end;
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   430
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   431
(*Change theory object for an existent item of loaded_thys 
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   432
  or create a new item *)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   433
fun store_theory thy_name thy =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   434
  let fun make_change (t :: loaded) =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   435
            let val ThyInfo {name, path, children, thy_info, ml_info, ...} = t
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   436
            in if name = thy_name then            
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   437
                    ThyInfo {name = name, path = path, children = children,
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   438
                             thy_info = thy_info, ml_info = ml_info,
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   439
                             theory = Some thy} :: loaded
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   440
               else
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   441
                    t :: (make_change loaded)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   442
            end
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   443
        | make_change [] =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   444
            [ThyInfo {name = thy_name, path = "", children = [],
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   445
                      thy_info = Some "", ml_info = Some "",
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   446
                      theory = Some thy}]
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   447
  in loaded_thys := make_change (!loaded_thys) end;
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   448
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   449
(*Create a list of all theories loaded by this structure *)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   450
fun list_loaded () = (!loaded_thys);
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   451
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   452
(*Change the list of loaded theories *)
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   453
fun set_loaded [] =
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   454
      loaded_thys := [ThyInfo {name = "Pure", path = "", children = [],
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   455
                      thy_info = Some "", ml_info = Some "",
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   456
                      theory = Some Thm.pure_thy}]
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   457
  | set_loaded ts =
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   458
      loaded_thys := ts;
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   459
123
0a2f744e008a moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents: 81
diff changeset
   460
end
74
208ab8773a73 changes in Readthy:
clasohm
parents: 0
diff changeset
   461