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