src/Pure/Thy/thy_read.ML
author paulson
Mon, 05 Oct 1998 10:33:34 +0200
changeset 5615 9ea709aa275c
parent 5495 48036910ab7e
child 5730 82a7aa74a631
permissions -rw-r--r--
deleted incorrect code that set Goals.proof_timing:=false Also causes time_use_thy to set proof_timing:=true
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)
5495
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   223
      end
1242
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
5495
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
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 () =
5495
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   240
      let val tinfo = {path = "", children = [], parents = [],
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   241
			       thy_time = None, ml_time = None,
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   242
			       theory = None};
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   243
      in if is_some (get_thyinfo tname) then ()
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   244
	 else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   245
      end
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   246
    fun read_thy_file() =
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   247
	   if thy_file = "" then ()
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   248
	   else
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   249
	     (writeln ("Reading \"" ^ name ^ ".thy\"");
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   250
	      init_thyinfo ();
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   251
	      read_thy tname thy_file;
5615
9ea709aa275c deleted incorrect code that set Goals.proof_timing:=false
paulson
parents: 5495
diff changeset
   252
	      Use.use (out_name tname);
5495
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   253
	      if not (!delete_tmpfiles) then ()
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   254
	      else OS.FileSys.remove (out_name tname);
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   255
	      thyfile2html tname abs_path)
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   256
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   257
       (*Add theory to list of all loaded theories (for index.html)
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   258
         and it to its parents' sub-charts*)
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   259
    fun add_theory path = 
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   260
	   if path = "" then               (*first time theory has been read*)
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   261
	       (mk_html tname abs_path old_parents;
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   262
		mk_graph tname abs_path)   (*Add it to graph definition file*)
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   263
	   else ()
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   264
  in if thy_uptodate andalso ml_uptodate then ()
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   265
     else
5495
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   266
      (read_thy_file();       
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   267
       set_info tname (Some (file_info thy_file)) None;
5495
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   268
            (*mark thy_file as successfully loaded*)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   269
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   270
       if ml_file = "" then ()
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   271
       else (writeln ("Reading \"" ^ name ^ ".ML\"");
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   272
             Use.use ml_file);
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   273
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   274
       (*Store theory again because it could have been redefined*)
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
   275
       use_text false ("val _ = store_theory " ^ tname ^ ".thy;");
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   276
5495
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   277
       add_theory (path_of tname);
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   278
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   279
       (*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
   280
       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
   281
       set_path ();
5495
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   282
       mark_children tname;  (*Mark theories that have to be reloaded*)
48036910ab7e Suppress timing messages for theorems proved in theory sections
paulson
parents: 5209
diff changeset
   283
       close_html () )
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   284
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   285
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   286
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   287
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
   288
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   289
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   290
fun time_use_thy tname = timeit(fn()=>
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   291
   (writeln("\n**** Starting Theory " ^ tname ^ " ****");
5615
9ea709aa275c deleted incorrect code that set Goals.proof_timing:=false
paulson
parents: 5495
diff changeset
   292
    setmp Goals.proof_timing true use_thy tname;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   293
    writeln("\n**** Finished Theory " ^ tname ^ " ****"))
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   294
   );
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   295
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   296
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   297
(*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
   298
  all theories that depend on them.*)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   299
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
   300
  let (*List theories in the order they have to be loaded in.*)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   301
      fun load_order [] result = result
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   302
        | load_order thys result =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   303
            let fun next_level [] = []
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   304
                  | next_level (t :: ts) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   305
                      let val children = children_of t
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   306
                      in children union (next_level ts) end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   307
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   308
                val descendants = next_level thys;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   309
            in load_order descendants ((result \\ descendants) @ descendants)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   310
            end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   311
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   312
      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
   313
            let val abspath = case get_thyinfo t of
3976
wenzelm
parents: 3966
diff changeset
   314
                                  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
   315
                                | None => "";
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   316
1704
35045774bc1e changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents: 1670
diff changeset
   317
                val (thy_file, ml_file) = get_filenames abspath t;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   318
                val (thy_uptodate, ml_uptodate) =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   319
                        thy_unchanged t thy_file ml_file;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   320
            in if thy_uptodate andalso ml_uptodate then ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   321
                                                   else use_thy t;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   322
               reload_changed ts
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   323
            end
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   324
        | reload_changed [] = ();
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   325
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   326
     (*Remove all theories that are no descendants of ProtoPure.
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   327
       If there are still children in the deleted theory's list
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   328
       schedule them for reloading *)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   329
     fun collect_garbage no_garbage =
3976
wenzelm
parents: 3966
diff changeset
   330
       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
   331
                 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
   332
                 else (writeln ("Theory \"" ^ tname ^
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   333
                       "\" is no longer linked with ProtoPure - removing it.");
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   334
                       remove_thy tname;
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   335
                       seq mark_outdated children)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   336
             | collect [] = ()
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   337
       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
   338
  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
   339
     collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   340
     reload_changed (load_order ["Pure", "CPure"] [])
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   341
  end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   342
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   343
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   344
(*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
   345
  Base members are only loaded if they are missing.*)
3876
wenzelm
parents: 3765
diff changeset
   346
fun mk_base bases child =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   347
  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
   348
      fun show_cycle base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   349
        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
   350
              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
   351
              in if base = curr then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   352
                   error ("Cyclic dependency of theories: "
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   353
                          ^ child ^ "->" ^ base ^ result)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   354
                 else if is_some tinfo then
3976
wenzelm
parents: 3966
diff changeset
   355
                   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
   356
                   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
   357
                   end
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   358
                 else ()
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   359
              end
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   360
        in find_it "" child end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   361
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   362
      (*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
   363
      fun find_cycle base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   364
        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
   365
        else ();
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   366
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   367
      (*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
   368
      fun add_child base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   369
        let val tinfo =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   370
              case Symtab.lookup (!loaded_thys, base) of
3976
wenzelm
parents: 3966
diff changeset
   371
                  Some ({path, children, parents, thy_time, ml_time,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   372
                           theory}) =>
3976
wenzelm
parents: 3966
diff changeset
   373
                    {path = path,
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   374
                             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
   375
                             thy_time = thy_time, ml_time = ml_time,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   376
                             theory = theory}
3976
wenzelm
parents: 3966
diff changeset
   377
                | 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
   378
                                   thy_time = None, ml_time = None,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   379
                                   theory = None};
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   380
        in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   381
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   382
      (*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
   383
        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
   384
      fun load base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   385
          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
   386
                                       (*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
   387
          in
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   388
            if child = base then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   389
                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
   390
                       ^ "->" ^ child)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   391
            else
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   392
              (find_cycle base;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   393
               add_child base;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   394
               if thy_loaded then ()
3876
wenzelm
parents: 3765
diff changeset
   395
               else (writeln ("Autoloading theory " ^ quote base
wenzelm
parents: 3765
diff changeset
   396
                              ^ " (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
   397
                     use_thy1 true base)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   398
              )
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   399
          end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   400
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   401
      (*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
   402
      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
   403
           (load b;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   404
            b :: load_base bs)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   405
        | load_base (File b :: bs) =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   406
           (load b;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   407
            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
   408
        | load_base [] = [];
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   409
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   410
      val dummy = unlink_thy child;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   411
      val mergelist = load_base bases;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   412
3876
wenzelm
parents: 3765
diff changeset
   413
      val base_thy =
wenzelm
parents: 3765
diff changeset
   414
       (writeln ("Loading theory " ^ quote child);
3998
6ec8d42082f1 merge: default to ProtoPure.thy;
wenzelm
parents: 3976
diff changeset
   415
         if null mergelist then ProtoPure.thy
5209
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 5090
diff changeset
   416
         else Theory.prep_ext_merge (map ThyInfo.theory mergelist));
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1408
diff changeset
   417
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   418
      val dummy =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   419
        let val tinfo = case Symtab.lookup (!loaded_thys, child) of
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   420
              Some ({path, children, parents = _, thy_time, ml_time, theory}) =>
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   421
                 {path = path, children = children, parents = mergelist,
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   422
                   thy_time = thy_time, ml_time = ml_time, theory = theory}
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   423
             | 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
   424
        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
   425
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   426
 in
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 4021
diff changeset
   427
    cur_thyname := child;
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   428
    base_thy
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   429
 end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   430
1359
71124bd19b40 added functions for storing and retrieving information about datatypes
clasohm
parents: 1348
diff changeset
   431
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   432
(*Temporarily enter a directory and load its ROOT.ML file;
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   433
  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
   434
local
1348
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1332
diff changeset
   435
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   436
  fun gen_use_dir use_cmd dirname =
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
   437
    let val old_dir = OS.FileSys.getDir ();
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
   438
    in OS.FileSys.chDir dirname;
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   439
       if !make_html then init_html() else ();
3602
cdfb8b7e60fa Moved several functions:
berghofe
parents: 3576
diff changeset
   440
       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
   441
       use_cmd "ROOT.ML";
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   442
       finish_html();
2244
dacee519738a Converted I/O operatios for Basis Library compatibility
paulson
parents: 2188
diff changeset
   443
       OS.FileSys.chDir old_dir
1670
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   444
    end;
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   445
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   446
in
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   447
4218
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   448
  val use_dir = gen_use_dir Use.use;
eff39c3ce72f adapted to new Use, File structs;
wenzelm
parents: 4111
diff changeset
   449
  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
   450
d706a6dce930 use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents: 1664
diff changeset
   451
end
1348
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1332
diff changeset
   452
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   453
end;