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