src/Pure/Thy/thy_read.ML
author wenzelm
Mon, 29 Jun 1998 10:32:06 +0200
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5209 a69fe5a61b6c
permissions -rw-r--r--
use_text: verbose flag;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thy_read.ML
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
     3
    Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
     4
                Tobias Nipkow and L C Paulson
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
     5
    Copyright   1994 TU Muenchen
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     6
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
     7
Functions for reading theory files.
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     8
*)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     9
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3602
diff changeset
    10
signature THY_READ =
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    11
sig
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    12
  datatype basetype = Thy  of string
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    13
                    | File of string
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    14
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    15
  val loadpath       : string list ref
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    16
  val delete_tmpfiles: bool ref
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    17
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    18
  val use_thy        : string -> unit
1348
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1332
diff changeset
    19
  val time_use_thy   : string -> unit
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1332
diff changeset
    20
  val use_dir        : string -> unit
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1332
diff changeset
    21
  val exit_use_dir   : string -> unit
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    22
  val update         : unit -> unit
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    23
  val unlink_thy     : string -> unit
3876
wenzelm
parents: 3765
diff changeset
    24
  val mk_base        : basetype list -> string -> theory
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    25
end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    26
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    27
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3602
diff changeset
    28
structure ThyRead: THY_READ =
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    29
struct
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
    30
3626
wenzelm
parents: 3619
diff changeset
    31
open ThmDatabase ThyInfo BrowserInfo;
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
    32
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    33
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    34
datatype basetype = Thy  of string
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    35
                  | File of string;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    36
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
    37
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
    38
(*Default search path for theory files*)
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
    39
val loadpath = ref ["."];
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
    40
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
    41
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
    42
(*Directory given as parameter to use_thy. This is temporarily added to
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
    43
  loadpath while the theory's ancestors are loaded.*)
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
    44
val tmp_loadpath = ref [] : string list ref;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    45
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
    46
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
    47
(*Remove temporary files after use*)
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
    48
val delete_tmpfiles = ref true;
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
    49
       
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    50
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
    51
(*Make name of the TextIO.output ML file for a theory *)
4429
4bc296026b22 tuned tmp file name;
wenzelm
parents: 4367
diff changeset
    52
fun out_name tname = File.tmp_name (tname ^ "_thy.ML");
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    53
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
    54
3626
wenzelm
parents: 3619
diff changeset
    55
(*Read a file specified by thy_file containing theory tname*)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
    56
fun read_thy tname thy_file =
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
    57
  let
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
    58
    val intext = File.read thy_file;
3619
0fc67ad6d62a eliminated ThySynData and ThySynFun;
wenzelm
parents: 3602
diff changeset
    59
    val outext = ThySyn.parse tname intext;
3626
wenzelm
parents: 3619
diff changeset
    60
  in
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
    61
    File.write (out_name tname) outext
3626
wenzelm
parents: 3619
diff changeset
    62
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    63
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    64
971
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
    65
(*Check if a theory was completly loaded *)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    66
fun already_loaded thy =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    67
  let val t = get_thyinfo thy
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    68
  in if is_none t then false
3976
wenzelm
parents: 3966
diff changeset
    69
     else let val {thy_time, ml_time, ...} = the t
971
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
    70
          in is_some thy_time andalso is_some ml_time end
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    71
  end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    72
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
    73
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    74
(*Check if a theory file has changed since its last use.
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    75
  Return a pair of boolean values for .thy and for .ML *)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
    76
fun thy_unchanged thy thy_file ml_file =
1098
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    77
  case get_thyinfo thy of
3976
wenzelm
parents: 3966
diff changeset
    78
      Some {thy_time, ml_time, ...} =>
1098
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    79
       let val tn = is_none thy_time;
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
    80
           val mn = is_none ml_time
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    81
       in if not tn andalso not mn then
1098
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    82
            ((file_info thy_file = the thy_time),
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    83
             (file_info ml_file = the ml_time))
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    84
          else if not tn andalso mn then
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    85
            (file_info thy_file = the thy_time, false)
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    86
          else
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    87
            (false, false)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    88
       end
1098
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
    89
    | None => (false, false)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    90
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
    91
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
    92
(*Get all descendants of a theory list *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
    93
fun get_descendants [] = []
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
    94
  | get_descendants (t :: ts) =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    95
      let val children = children_of t
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    96
      in children union (get_descendants (children union ts)) end;
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
    97
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    98
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    99
(*Find a file using a list of paths if no absolute or relative path is
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   100
  specified.*)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   101
fun find_file "" name =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   102
      let fun find_it (cur :: paths) =
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   103
                if File.exists (tack_on cur name) then
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   104
                  (if cur = "." then name else tack_on cur name)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   105
                else
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   106
                  find_it paths
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   107
           | find_it [] = ""
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   108
      in find_it (!tmp_loadpath @ !loadpath) end
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   109
  | find_file path name =
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   110
      if File.exists (tack_on path name) then tack_on path name
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   111
                                         else "";
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   112
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   113
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   114
(*Get absolute pathnames for a new or already loaded theory *)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   115
fun get_filenames path name =
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
   116
  let fun new_filename () =
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
   117
        let val found = find_file path (name ^ ".thy");
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
   118
            val absolute_path = absolute_path (OS.FileSys.getDir ());
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
   119
            val thy_file = absolute_path found;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   120
            val (thy_path, _) = split_filename thy_file;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   121
            val found = find_file path (name ^ ".ML");
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
   122
            val ml_file = if thy_file = "" then absolute_path found
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   123
                          else if File.exists (tack_on thy_path (name ^ ".ML"))
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   124
                          then tack_on thy_path (name ^ ".ML")
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   125
                          else "";
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   126
            val searched_dirs = if path = "" then (!tmp_loadpath @ !loadpath)
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   127
                                             else [path]
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   128
        in if thy_file = "" andalso ml_file = "" then
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   129
             error ("Could not find file \"" ^ name ^ ".thy\" or \""
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   130
                    ^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n"
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   131
                    ^ "in the following directories: \"" ^
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   132
                    (space_implode "\", \"" searched_dirs) ^ "\"")
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   133
           else ();
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   134
           (thy_file, ml_file)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   135
        end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   136
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   137
      val tinfo = get_thyinfo name;
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   138
  in if is_some tinfo andalso path = "" then
3976
wenzelm
parents: 3966
diff changeset
   139
       let val {path = abs_path, ...} = the tinfo;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   140
           val (thy_file, ml_file) = if abs_path = "" then new_filename ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   141
                                     else (find_file abs_path (name ^ ".thy"),
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   142
                                           find_file abs_path (name ^ ".ML"))
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   143
       in if thy_file = "" andalso ml_file = "" then
1580
e3fd931e6095 Added some functions which allow redirection of Isabelle's output
berghofe
parents: 1554
diff changeset
   144
            (warning ("File \"" ^ (tack_on path name)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   145
                      ^ ".thy\"\ncontaining theory \"" ^ name
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   146
                      ^ "\" no longer exists.");
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   147
             new_filename ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   148
            )
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   149
          else (thy_file, ml_file)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   150
       end
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   151
     else new_filename ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   152
  end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   153
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   154
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   155
(*Remove theory from all child lists in loaded_thys *)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   156
fun unlink_thy tname =
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   157
  let fun remove ({path, children, parents, thy_time, ml_time, theory}) =
3976
wenzelm
parents: 3966
diff changeset
   158
        {path = path, children = children \ tname, parents = parents,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   159
                 thy_time = thy_time, ml_time = ml_time, theory = theory}
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   160
  in loaded_thys := Symtab.map remove (!loaded_thys) end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   161
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   162
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   163
(*Remove a theory from loaded_thys *)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   164
fun remove_thy tname =
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   165
  loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   166
                 (Symtab.dest (!loaded_thys)));
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   167
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   168
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   169
(*Change thy_time and ml_time for an existent item *)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   170
fun set_info tname thy_time ml_time =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   171
  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   172
          Some ({path, children, parents, theory, thy_time = _, ml_time = _}) =>
3976
wenzelm
parents: 3966
diff changeset
   173
            {path = path, children = children, parents = parents,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   174
                     thy_time = thy_time, ml_time = ml_time, theory = theory}
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   175
        | None => error ("set_info: theory " ^ tname ^ " not found");
1359
71124bd19b40 added functions for storing and retrieving information about datatypes
clasohm
parents: 1348
diff changeset
   176
  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   177
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   178
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   179
(*Mark theory as changed since last read if it has been completly read *)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   180
fun mark_outdated tname =
971
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   181
  let val t = get_thyinfo tname;
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   182
  in if is_none t then ()
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   183
     else
3976
wenzelm
parents: 3966
diff changeset
   184
       let val {thy_time, ml_time, ...} = the t
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   185
       in set_info tname (if is_none thy_time then None else Some "")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   186
                         (if is_none ml_time then None else Some "")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   187
       end
971
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   188
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   189
1656
cbba49da5139 fixed bug in set_current_thy
clasohm
parents: 1603
diff changeset
   190
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   191
(*Read .thy and .ML files that haven't been read yet or have changed since
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   192
  they were last read;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   193
  loaded_thys is a thy_info list ref containing all theories that have
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   194
  completly been read by this and preceeding use_thy calls.
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   195
  tmp_loadpath is temporarily added to loadpath while the ancestors of a
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   196
  theory that the user specified as e.g. "ex/Nat" are loaded. Because of
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   197
  raised exceptions we cannot guarantee that it's value is always valid.
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   198
  Therefore this has to be assured by the first parameter of use_thy1 which
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   199
  is "true" if use_thy gets invoked by mk_base and "false" else.
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   200
*)
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   201
fun use_thy1 tmp_loadpath_valid name =
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   202
  let
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   203
    val (path, tname) = split_filename name;
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   204
    val dummy = (tmp_loadpath :=
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   205
      (if not tmp_loadpath_valid then (if path = "" then [] else [path])
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   206
       else !tmp_loadpath));
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   207
    val (thy_file, ml_file) = get_filenames path tname;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   208
    val (abs_path, _) = if thy_file = "" then split_filename ml_file
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   209
                        else split_filename thy_file;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   210
    val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file;
1403
cdfa3ffcead2 renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents: 1386
diff changeset
   211
    val old_parents = parents_of_name tname;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   212
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   213
    (*Set absolute path for loaded theory *)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   214
    fun set_path () =
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   215
      let val {path = _, children, parents, thy_time, ml_time, theory} =
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   216
            the (Symtab.lookup (!loaded_thys, tname));
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   217
      in loaded_thys := Symtab.update ((tname,
3976
wenzelm
parents: 3966
diff changeset
   218
                          {path = abs_path,
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   219
                                   children = children, parents = parents,
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   220
                                   thy_time = thy_time, ml_time = ml_time,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   221
                                   theory = theory}),
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   222
                          !loaded_thys)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   223
      end;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   224
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   225
    (*Mark all direct descendants of a theory as changed *)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   226
    fun mark_children thy =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   227
      let val children = children_of thy;
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   228
          val present = filter (is_some o get_thyinfo) children;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   229
          val loaded = filter already_loaded present;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   230
      in if loaded <> [] then
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   231
           writeln ("The following children of theory " ^ (quote thy)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   232
                    ^ " are now out-of-date: "
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   233
                    ^ (quote (space_implode "\",\"" loaded)))
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   234
         else ();
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   235
         seq mark_outdated present
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   236
      end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   237
1554
4ee99a973be4 moved part of delete_thms into init_thyinfo
clasohm
parents: 1538
diff changeset
   238
    (*Make sure that loaded_thys contains an entry for tname*)
4ee99a973be4 moved part of delete_thms into init_thyinfo
clasohm
parents: 1538
diff changeset
   239
    fun init_thyinfo () =
3976
wenzelm
parents: 3966
diff changeset
   240
    let val tinfo = {path = "", children = [], parents = [],
1554
4ee99a973be4 moved part of delete_thms into init_thyinfo
clasohm
parents: 1538
diff changeset
   241
                             thy_time = None, ml_time = None,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   242
                             theory = None};
1554
4ee99a973be4 moved part of delete_thms into init_thyinfo
clasohm
parents: 1538
diff changeset
   243
    in if is_some (get_thyinfo tname) then ()
4ee99a973be4 moved part of delete_thms into init_thyinfo
clasohm
parents: 1538
diff changeset
   244
       else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
4ee99a973be4 moved part of delete_thms into init_thyinfo
clasohm
parents: 1538
diff changeset
   245
    end;
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   246
  in if thy_uptodate andalso ml_uptodate then ()
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   247
     else
1386
cf066d9b4c4f fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents: 1378
diff changeset
   248
      (if thy_file = "" then ()
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   249
       else
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   250
         (writeln ("Reading \"" ^ name ^ ".thy\"");
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   251
1554
4ee99a973be4 moved part of delete_thms into init_thyinfo
clasohm
parents: 1538
diff changeset
   252
          init_thyinfo ();
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   253
          read_thy tname thy_file;
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   254
          Use.use (out_name tname);
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   255
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   256
          if not (!delete_tmpfiles) then ()
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
   257
          else OS.FileSys.remove (out_name tname);
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   258
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   259
          thyfile2html tname abs_path
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   260
         );
1386
cf066d9b4c4f fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents: 1378
diff changeset
   261
       
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   262
       set_info tname (Some (file_info thy_file)) None;
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   263
                                       (*mark thy_file as successfully loaded*)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   264
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   265
       if ml_file = "" then ()
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   266
       else (writeln ("Reading \"" ^ name ^ ".ML\"");
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   267
             Use.use ml_file);
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   268
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   269
       (*Store theory again because it could have been redefined*)
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
   270
       use_text false ("val _ = store_theory " ^ tname ^ ".thy;");
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   271
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   272
       (*Add theory to list of all loaded theories (for index.html)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   273
         and add it to its parents' sub-charts*)
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   274
       let val path = path_of tname;
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   275
       in if path = "" then               (*first time theory has been read*)
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   276
          (
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   277
            (*Add theory to list of all loaded theories (for index.html)
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   278
              and add it to its parents' sub-charts*)
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   279
            mk_html tname abs_path old_parents;
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   280
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   281
            (*Add theory to graph definition file*)
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   282
            mk_graph tname abs_path
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   283
          )
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   284
          else ()
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   285
       end;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   286
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   287
       (*Now set the correct info*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   288
       set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   289
       set_path ();
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   290
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   291
       (*Mark theories that have to be reloaded*)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   292
       mark_children tname;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   293
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   294
       (*Close HTML file*)
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   295
       close_html ()
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   296
      )
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   297
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   298
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   299
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   300
val use_thy = use_thy1 false;
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   301
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   302
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   303
fun time_use_thy tname = timeit(fn()=>
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   304
   (writeln("\n**** Starting Theory " ^ tname ^ " ****");
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   305
    use_thy tname;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   306
    writeln("\n**** Finished Theory " ^ tname ^ " ****"))
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   307
   );
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   308
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   309
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   310
(*Load all thy or ML files that have been changed and also
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   311
  all theories that depend on them.*)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   312
fun update () =
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   313
  let (*List theories in the order they have to be loaded in.*)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   314
      fun load_order [] result = result
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   315
        | load_order thys result =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   316
            let fun next_level [] = []
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   317
                  | next_level (t :: ts) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   318
                      let val children = children_of t
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   319
                      in children union (next_level ts) end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   320
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   321
                val descendants = next_level thys;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   322
            in load_order descendants ((result \\ descendants) @ descendants)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   323
            end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   324
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   325
      fun reload_changed (t :: ts) =
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   326
            let val abspath = case get_thyinfo t of
3976
wenzelm
parents: 3966
diff changeset
   327
                                  Some ({path, ...}) => path
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   328
                                | None => "";
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   329
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   330
                val (thy_file, ml_file) = get_filenames abspath t;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   331
                val (thy_uptodate, ml_uptodate) =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   332
                        thy_unchanged t thy_file ml_file;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   333
            in if thy_uptodate andalso ml_uptodate then ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   334
                                                   else use_thy t;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   335
               reload_changed ts
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   336
            end
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   337
        | reload_changed [] = ();
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   338
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   339
     (*Remove all theories that are no descendants of ProtoPure.
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   340
       If there are still children in the deleted theory's list
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   341
       schedule them for reloading *)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   342
     fun collect_garbage no_garbage =
3976
wenzelm
parents: 3966
diff changeset
   343
       let fun collect ((tname, {children, ...}: thy_info) :: ts) =
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   344
                 if tname mem no_garbage then collect ts
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   345
                 else (writeln ("Theory \"" ^ tname ^
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   346
                       "\" is no longer linked with ProtoPure - removing it.");
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   347
                       remove_thy tname;
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   348
                       seq mark_outdated children)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   349
             | collect [] = ()
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   350
       in collect (Symtab.dest (!loaded_thys)) end;
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   351
  in tmp_loadpath := [];
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   352
     collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   353
     reload_changed (load_order ["Pure", "CPure"] [])
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   354
  end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   355
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   356
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   357
(*Merge theories to build a base for a new theory.
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   358
  Base members are only loaded if they are missing.*)
3876
wenzelm
parents: 3765
diff changeset
   359
fun mk_base bases child =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   360
  let (*Show the cycle that would be created by add_child*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   361
      fun show_cycle base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   362
        let fun find_it result curr =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   363
              let val tinfo = get_thyinfo curr
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   364
              in if base = curr then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   365
                   error ("Cyclic dependency of theories: "
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   366
                          ^ child ^ "->" ^ base ^ result)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   367
                 else if is_some tinfo then
3976
wenzelm
parents: 3966
diff changeset
   368
                   let val {children, ...} = the tinfo
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   369
                   in seq (find_it ("->" ^ curr ^ result)) children
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   370
                   end
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   371
                 else ()
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   372
              end
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   373
        in find_it "" child end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   374
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   375
      (*Check if a cycle would be created by add_child*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   376
      fun find_cycle base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   377
        if base mem (get_descendants [child]) then show_cycle base
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   378
        else ();
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   379
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   380
      (*Add child to child list of base*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   381
      fun add_child base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   382
        let val tinfo =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   383
              case Symtab.lookup (!loaded_thys, base) of
3976
wenzelm
parents: 3966
diff changeset
   384
                  Some ({path, children, parents, thy_time, ml_time,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   385
                           theory}) =>
3976
wenzelm
parents: 3966
diff changeset
   386
                    {path = path,
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   387
                             children = child ins children, parents = parents,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   388
                             thy_time = thy_time, ml_time = ml_time,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   389
                             theory = theory}
3976
wenzelm
parents: 3966
diff changeset
   390
                | None => {path = "", children = [child], parents = [],
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   391
                                   thy_time = None, ml_time = None,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   392
                                   theory = None};
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   393
        in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   394
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   395
      (*Load a base theory if not already done
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   396
        and no cycle would be created *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   397
      fun load base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   398
          let val thy_loaded = already_loaded base
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   399
                                       (*test this before child is added *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   400
          in
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   401
            if child = base then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   402
                error ("Cyclic dependency of theories: " ^ child
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   403
                       ^ "->" ^ child)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   404
            else
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   405
              (find_cycle base;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   406
               add_child base;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   407
               if thy_loaded then ()
3876
wenzelm
parents: 3765
diff changeset
   408
               else (writeln ("Autoloading theory " ^ quote base
wenzelm
parents: 3765
diff changeset
   409
                              ^ " (required by " ^ quote child ^ ")");
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   410
                     use_thy1 true base)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   411
              )
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   412
          end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   413
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   414
      (*Load all needed files and make a list of all real theories *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   415
      fun load_base (Thy b :: bs) =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   416
           (load b;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   417
            b :: load_base bs)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   418
        | load_base (File b :: bs) =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   419
           (load b;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   420
            load_base bs)                    (*don't add it to mergelist *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   421
        | load_base [] = [];
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   422
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   423
      val dummy = unlink_thy child;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   424
      val mergelist = load_base bases;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   425
3876
wenzelm
parents: 3765
diff changeset
   426
      val base_thy =
wenzelm
parents: 3765
diff changeset
   427
       (writeln ("Loading theory " ^ quote child);
3998
6ec8d42082f1 merge: default to ProtoPure.thy;
wenzelm
parents: 3976
diff changeset
   428
         if null mergelist then ProtoPure.thy
6ec8d42082f1 merge: default to ProtoPure.thy;
wenzelm
parents: 3976
diff changeset
   429
         else Theory.prep_ext_merge (map theory_of mergelist));
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
   430
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   431
      val dummy =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   432
        let val tinfo = case Symtab.lookup (!loaded_thys, child) of
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   433
              Some ({path, children, parents = _, thy_time, ml_time, theory}) =>
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   434
                 {path = path, children = children, parents = mergelist,
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   435
                   thy_time = thy_time, ml_time = ml_time, theory = theory}
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   436
             | None => sys_error ("set_parents: theory " ^ child ^ " not found");
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   437
        in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   438
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   439
 in
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   440
    cur_thyname := child;
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   441
    base_thy
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   442
 end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   443
1359
71124bd19b40 added functions for storing and retrieving information about datatypes
clasohm
parents: 1348
diff changeset
   444
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   445
(*Temporarily enter a directory and load its ROOT.ML file;
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   446
  also do some work for HTML and graph generation*)
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   447
local
1348
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1332
diff changeset
   448
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   449
  fun gen_use_dir use_cmd dirname =
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
   450
    let val old_dir = OS.FileSys.getDir ();
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
   451
    in OS.FileSys.chDir dirname;
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   452
       if !make_html then init_html() else ();
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   453
       if !make_graph then init_graph dirname else ();
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   454
       use_cmd "ROOT.ML";
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   455
       finish_html();
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
   456
       OS.FileSys.chDir old_dir
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   457
    end;
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   458
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   459
in
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   460
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   461
  val use_dir = gen_use_dir Use.use;
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   462
  val exit_use_dir = gen_use_dir Use.exit_use;
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   463
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   464
end
1348
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1332
diff changeset
   465
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   466
end;