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