added check for concistency of filename and theory name;
authorclasohm
Fri Jul 15 13:30:42 1994 +0200 (1994-07-15)
changeset 476836cad329311
parent 475 bf2f285aa316
child 477 53fc8ad84b33
added check for concistency of filename and theory name;
made loaded_thys a symtab instead of an association list;
added store_thm, qed, get_thm, get_thms
src/Pure/Thy/thy_parse.ML
src/Pure/Thy/thy_read.ML
src/Pure/Thy/thy_syn.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Jul 15 12:24:05 1994 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Jul 15 13:30:42 1994 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4    type syntax
     1.5    val make_syntax: string list ->
     1.6      (string * (token list -> (string * string) * token list)) list -> syntax
     1.7 -  val parse_thy: syntax -> string -> string
     1.8 +  val parse_thy: syntax -> string -> string -> string
     1.9    val section: string -> string -> (token list -> string * token list)
    1.10      -> (string * (token list -> (string * string) * token list))
    1.11    val axm_section: string -> string
    1.12 @@ -388,43 +388,49 @@
    1.13  
    1.14  (* theory definition *)
    1.15  
    1.16 -fun mk_structure ((thy_name, old_thys), Some (extxt, postxt, mltxt)) =
    1.17 -      "structure " ^ thy_name ^ " =\n\
    1.18 -      \struct\n\
    1.19 -      \\n\
    1.20 -      \local\n"
    1.21 -      ^ trfun_defs ^ "\n\
    1.22 -      \in\n\
    1.23 -      \\n"
    1.24 -      ^ mltxt ^ "\n\
    1.25 -      \\n\
    1.26 -      \val thy = (" ^ old_thys ^ " true)\n\n\
    1.27 -      \|> add_trfuns\n"
    1.28 -      ^ trfun_args ^ "\n\
    1.29 -      \\n"
    1.30 -      ^ extxt ^ "\n\
    1.31 -      \\n\
    1.32 -      \|> add_thyname " ^ quote thy_name ^ ";\n\
    1.33 -      \\n\
    1.34 -      \\n"
    1.35 -      ^ postxt ^ "\n\
    1.36 -      \\n\
    1.37 -      \end;\n\
    1.38 -      \end;\n"
    1.39 -  | mk_structure ((thy_name, old_thys), None) =
    1.40 -      "structure " ^ thy_name ^ " =\n\
    1.41 -      \struct\n\
    1.42 -      \\n\
    1.43 -      \val thy = (" ^ old_thys ^ " false);\n\
    1.44 -      \\n\
    1.45 -      \end;\n";
    1.46 +fun mk_structure tname ((thy_name, old_thys), Some (extxt, postxt, mltxt)) =
    1.47 +      if (thy_name = tname) then
    1.48 +        "structure " ^ thy_name ^ " =\n\
    1.49 +        \struct\n\
    1.50 +        \\n\
    1.51 +        \local\n"
    1.52 +        ^ trfun_defs ^ "\n\
    1.53 +        \in\n\
    1.54 +        \\n"
    1.55 +        ^ mltxt ^ "\n\
    1.56 +        \\n\
    1.57 +        \val thy = (" ^ old_thys ^ " true)\n\n\
    1.58 +        \|> add_trfuns\n"
    1.59 +        ^ trfun_args ^ "\n\
    1.60 +        \\n"
    1.61 +        ^ extxt ^ "\n\
    1.62 +        \\n\
    1.63 +        \|> add_thyname " ^ quote thy_name ^ ";\n\
    1.64 +        \\n\
    1.65 +        \\n"
    1.66 +        ^ postxt ^ "\n\
    1.67 +        \\n\
    1.68 +        \end;\n\
    1.69 +        \end;\n"
    1.70 +      else error ("use_thy: Filename \"" ^ tname ^ ".thy\" and theory name \""
    1.71 +                  ^ thy_name ^ "\" are different")
    1.72 +  | mk_structure tname ((thy_name, old_thys), None) =
    1.73 +      if (thy_name = tname) then
    1.74 +        "structure " ^ thy_name ^ " =\n\
    1.75 +        \struct\n\
    1.76 +        \\n\
    1.77 +        \val thy = (" ^ old_thys ^ " false);\n\
    1.78 +        \\n\
    1.79 +        \end;\n"
    1.80 +      else error ("use_thy: Filename \"" ^ tname ^ ".thy\" and theory name \""
    1.81 +                  ^ thy_name ^ "\" are different");
    1.82  
    1.83 -fun theory_defn sectab =
    1.84 +fun theory_defn sectab tname =
    1.85    header -- optional (extension sectab >> Some) None -- eof
    1.86 -  >> (mk_structure o #1);
    1.87 +  >> (mk_structure tname o #1);
    1.88  
    1.89 -fun parse_thy (lex, sectab) str =
    1.90 -  #1 (!! (theory_defn sectab) (tokenize lex str));
    1.91 +fun parse_thy (lex, sectab) tname str =
    1.92 +  #1 (!! (theory_defn sectab tname) (tokenize lex str));
    1.93  
    1.94  
    1.95  (* standard sections *)
     2.1 --- a/src/Pure/Thy/thy_read.ML	Fri Jul 15 12:24:05 1994 +0200
     2.2 +++ b/src/Pure/Thy/thy_read.ML	Fri Jul 15 13:30:42 1994 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      Pure/Thy/thy_read.ML
     2.5      ID:         $Id$
     2.6      Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson / Carsten Clasohm
     2.7 -    Copyright   1993  TU Muenchen
     2.8 +    Copyright   1994  TU Muenchen
     2.9  
    2.10  Reading and writing the theory definition files.
    2.11  
    2.12 @@ -10,17 +10,19 @@
    2.13                  and it then tries to read XXX.ML
    2.14  *)
    2.15  
    2.16 -datatype thy_info = ThyInfo of {name: string, path: string,
    2.17 +datatype thy_info = ThyInfo of {path: string,
    2.18                                  children: string list,
    2.19 -                                thy_info: string option, ml_info: string option,
    2.20 -                                theory: Thm.theory option};
    2.21 +                                thy_time: string option,
    2.22 +                                ml_time: string option,
    2.23 +                                theory: Thm.theory option,
    2.24 +                                thms: thm Symtab.table};
    2.25  
    2.26  signature READTHY =
    2.27  sig
    2.28    datatype basetype = Thy  of string
    2.29                      | File of string
    2.30  
    2.31 -  val loaded_thys    : thy_info list ref
    2.32 +  val loaded_thys    : thy_info Symtab.table ref
    2.33    val loadpath       : string list ref
    2.34    val delete_tmpfiles: bool ref
    2.35  
    2.36 @@ -28,35 +30,42 @@
    2.37    val update         : unit -> unit
    2.38    val time_use_thy   : string -> unit
    2.39    val unlink_thy     : string -> unit
    2.40 -  val base_on        : basetype list -> string -> bool -> Thm.theory
    2.41 -  val store_theory   : string -> Thm.theory -> unit
    2.42 +  val base_on        : basetype list -> string -> bool -> theory
    2.43 +  val store_theory   : theory * string -> unit
    2.44 +
    2.45 +  val store_thm      : thm * string -> thm
    2.46 +  val qed            : string -> unit
    2.47 +  val get_thm        : theory -> string -> thm
    2.48 +  val get_thms       : theory -> (string * thm) list
    2.49  end;
    2.50  
    2.51  
    2.52  functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY =
    2.53  struct
    2.54 +open Symtab;
    2.55  
    2.56  datatype basetype = Thy  of string
    2.57                    | File of string;
    2.58  
    2.59 -val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [], 
    2.60 -                                thy_info = Some "", ml_info = Some "", 
    2.61 -                                theory = Some Thm.pure_thy}];
    2.62 +val loaded_thys = ref (make [("Pure", ThyInfo {path = "", children = [], 
    2.63 +                                       thy_time = Some "", ml_time = Some "", 
    2.64 +                                       theory = Some pure_thy,
    2.65 +                                       thms = null})]);
    2.66  
    2.67  val loadpath = ref ["."];           (*default search path for theory files *)
    2.68  
    2.69  val delete_tmpfiles = ref true;         (*remove temporary files after use *)
    2.70  
    2.71  (*Make name of the output ML file for a theory *)
    2.72 -fun out_name thy = "." ^ thy ^ ".thy.ML";
    2.73 +fun out_name tname = "." ^ tname ^ ".thy.ML";
    2.74  
    2.75  (*Read a file specified by thy_file containing theory thy *)
    2.76 -fun read_thy thy thy_file =
    2.77 +fun read_thy tname thy_file =
    2.78    let 
    2.79      val instream  = open_in thy_file;
    2.80 -    val outstream = open_out (out_name thy);
    2.81 +    val outstream = open_out (out_name tname);
    2.82    in  
    2.83 -    output (outstream, ThySyn.parse (input (instream, 999999)));
    2.84 +    output (outstream, ThySyn.parse tname (input (instream, 999999)));
    2.85      close_out outstream;
    2.86      close_in instream
    2.87    end;
    2.88 @@ -66,35 +75,16 @@
    2.89      handle Io _ => false;
    2.90  
    2.91  (*Get thy_info for a loaded theory *)
    2.92 -fun get_thyinfo thy =
    2.93 -  let fun do_search (t :: loaded : thy_info list) =
    2.94 -            let val ThyInfo {name, ...} = t
    2.95 -            in if name = thy then Some t else do_search loaded end
    2.96 -        | do_search [] = None
    2.97 -  in do_search (!loaded_thys) end;
    2.98 -
    2.99 -(*Replace an item by the result of make_change *)
   2.100 -fun change_thyinfo make_change =
   2.101 -  let fun search (t :: loaded) =
   2.102 -            let val ThyInfo {name, path, children, thy_info, ml_info,
   2.103 -                             theory} = t
   2.104 -                val (new_t, continue) = make_change name path children thy_info
   2.105 -                                                    ml_info theory
   2.106 -            in if continue then            
   2.107 -                 new_t :: (search loaded)
   2.108 -               else
   2.109 -                 new_t :: loaded
   2.110 -            end
   2.111 -        | search [] = []
   2.112 -  in loaded_thys := search (!loaded_thys) end;
   2.113 +fun get_thyinfo tname = lookup (!loaded_thys, tname);
   2.114  
   2.115  (*Check if a theory was already loaded *)
   2.116  fun already_loaded thy =
   2.117    let val t = get_thyinfo thy
   2.118    in if is_none t then false
   2.119 -     else let val ThyInfo {thy_info, ml_info, ...} = the t
   2.120 -          in if is_none thy_info orelse is_none ml_info then false 
   2.121 -             else true end
   2.122 +     else let val ThyInfo {thy_time, ml_time, ...} = the t
   2.123 +          in if is_none thy_time orelse is_none ml_time then false 
   2.124 +             else true 
   2.125 +          end
   2.126    end;
   2.127  
   2.128  (*Check if a theory file has changed since its last use.
   2.129 @@ -102,12 +92,12 @@
   2.130  fun thy_unchanged thy thy_file ml_file = 
   2.131    let val t = get_thyinfo thy
   2.132    in if is_some t then
   2.133 -       let val ThyInfo {thy_info, ml_info, ...} = the t
   2.134 -           val tn = is_none thy_info;
   2.135 -           val mn = is_none ml_info
   2.136 +       let val ThyInfo {thy_time, ml_time, ...} = the t
   2.137 +           val tn = is_none thy_time;
   2.138 +           val mn = is_none ml_time
   2.139         in if not tn andalso not mn then
   2.140 -              ((file_info thy_file = the thy_info), 
   2.141 -               (file_info ml_file = the ml_info))
   2.142 +              ((file_info thy_file = the thy_time), 
   2.143 +               (file_info ml_file = the ml_time))
   2.144            else if not tn andalso mn then (true, false)
   2.145            else (false, false)
   2.146         end
   2.147 @@ -156,9 +146,9 @@
   2.148             (thy_file, ml_file) 
   2.149          end;
   2.150  
   2.151 -      val thy = get_thyinfo name
   2.152 -  in if is_some thy andalso path = "" then
   2.153 -       let val ThyInfo {path = abs_path, ...} = the thy;
   2.154 +      val tinfo = get_thyinfo name;
   2.155 +  in if is_some tinfo andalso path = "" then
   2.156 +       let val ThyInfo {path = abs_path, ...} = the tinfo;
   2.157             val (thy_file, ml_file) = if abs_path = "" then new_filename ()
   2.158                                       else (find_file abs_path (name ^ ".thy"),
   2.159                                             find_file abs_path (name ^ ".ML"))
   2.160 @@ -174,40 +164,31 @@
   2.161    end;
   2.162  
   2.163  (*Remove theory from all child lists in loaded_thys *)
   2.164 -fun unlink_thy thy =
   2.165 -  let fun remove name path children thy_info ml_info theory =
   2.166 -            (ThyInfo {name = name, path = path, children = children \ thy, 
   2.167 -                      thy_info = thy_info, ml_info = ml_info,
   2.168 -                      theory = theory}, true)
   2.169 -  in change_thyinfo remove end;
   2.170 +fun unlink_thy tname =
   2.171 +  let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms}) =
   2.172 +        ThyInfo {path = path, children = children \ tname, 
   2.173 +                 thy_time = thy_time, ml_time = ml_time,
   2.174 +                 theory = theory, thms = thms}
   2.175 +  in loaded_thys := mapst remove (!loaded_thys) end;
   2.176  
   2.177  (*Remove a theory from loaded_thys *)
   2.178 -fun remove_thy thy =
   2.179 -  let fun remove (t :: ts) =
   2.180 -            let val ThyInfo {name, ...} = t
   2.181 -            in if name = thy then ts
   2.182 -                             else t :: (remove ts)
   2.183 -            end
   2.184 -        | remove [] = []
   2.185 -  in loaded_thys := remove (!loaded_thys) end;
   2.186 +fun remove_thy tname =
   2.187 +  loaded_thys := make (filter_out (fn (id, _) => id = tname)
   2.188 +                 (alist_of (!loaded_thys)));
   2.189  
   2.190 -(*Change thy_info and ml_info for an existent item *)
   2.191 -fun set_info thy_new ml_new thy =
   2.192 -  let fun change name path children thy_info ml_info theory =
   2.193 -        if name = thy then
   2.194 -            (ThyInfo {name = name, path = path, children = children,
   2.195 -                      thy_info = Some thy_new, ml_info = Some ml_new,
   2.196 -                      theory = theory}, false)
   2.197 -        else
   2.198 -            (ThyInfo {name = name, path = path, children = children,
   2.199 -                      thy_info = thy_info, ml_info = ml_info,
   2.200 -                      theory = theory}, true)
   2.201 -  in change_thyinfo change end;
   2.202 +(*Change thy_time and ml_time for an existent item *)
   2.203 +fun set_info thy_time ml_time tname =
   2.204 +  let val ThyInfo {path, children, theory, thms, ...} = 
   2.205 +        the (lookup (!loaded_thys, tname));
   2.206 +  in loaded_thys := update ((tname, 
   2.207 +       ThyInfo {path = path, children = children,
   2.208 +                thy_time = Some thy_time, ml_time = Some ml_time,
   2.209 +                theory = theory, thms = thms}), !loaded_thys)
   2.210 +  end;
   2.211  
   2.212  (*Mark theory as changed since last read if it has been completly read *)
   2.213 -fun mark_outdated thy =
   2.214 -  if already_loaded thy then set_info "" "" thy
   2.215 -                        else ();
   2.216 +fun mark_outdated tname = 
   2.217 +  if already_loaded tname then set_info "" "" tname else ();
   2.218  
   2.219  (*Read .thy and .ML files that haven't been read yet or have changed since 
   2.220    they were last read;
   2.221 @@ -215,25 +196,23 @@
   2.222    completly been read by this and preceeding use_thy calls.
   2.223    If a theory changed since its last use its children are marked as changed *)
   2.224  fun use_thy name =
   2.225 -    let val (path, thy_name) = split_filename name;
   2.226 -        val (thy_file, ml_file) = get_filenames path thy_name;
   2.227 +    let val (path, tname) = split_filename name;
   2.228 +        val (thy_file, ml_file) = get_filenames path tname;
   2.229          val (abs_path, _) = if thy_file = "" then split_filename ml_file
   2.230                              else split_filename thy_file;
   2.231 -        val (thy_uptodate, ml_uptodate) = thy_unchanged thy_name 
   2.232 +        val (thy_uptodate, ml_uptodate) = thy_unchanged tname 
   2.233                                                          thy_file ml_file;
   2.234  
   2.235           (*Set absolute path for loaded theory *)
   2.236           fun set_path () =
   2.237 -           let fun change name path children thy_info ml_info theory =
   2.238 -                 if name = thy_name then            
   2.239 -                   (ThyInfo {name = name, path = abs_path, children = children,
   2.240 -                             thy_info = thy_info, ml_info = ml_info,
   2.241 -                             theory = theory}, false)
   2.242 -                 else
   2.243 -                   (ThyInfo {name = name, path = path, children = children,
   2.244 -                             thy_info = thy_info, ml_info = ml_info,
   2.245 -                             theory = theory}, true)
   2.246 -           in change_thyinfo change end;
   2.247 +           let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} = 
   2.248 +                 the (lookup (!loaded_thys, tname));
   2.249 +           in loaded_thys := update ((tname, 
   2.250 +                               ThyInfo {path = abs_path, children = children,
   2.251 +                                        thy_time = thy_time, ml_time = ml_time,
   2.252 +                                        theory = theory, thms = thms}),
   2.253 +                               !loaded_thys)
   2.254 +           end;
   2.255  
   2.256           (*Mark all direct descendants of a theory as changed *)
   2.257           fun mark_children thy =
   2.258 @@ -246,35 +225,47 @@
   2.259                     seq mark_outdated loaded
   2.260                    )
   2.261                else ()
   2.262 -           end
   2.263 +           end;
   2.264  
   2.265 +        (*Remove all theorems associated with a theory*)
   2.266 +        fun delete_thms () =
   2.267 +          let val tinfo = case lookup (!loaded_thys, tname) of 
   2.268 +             Some (ThyInfo {path, children, thy_time, ml_time, theory, ...}) =>
   2.269 +                 ThyInfo {path = path, children = children,
   2.270 +                          thy_time = thy_time, ml_time = ml_time,
   2.271 +                          theory = theory, thms = null}
   2.272 +           | None => ThyInfo {path = "", children = [],
   2.273 +                              thy_time = None, ml_time = None,
   2.274 +                              theory = None, thms = null};
   2.275 +         in loaded_thys := update ((tname, tinfo), !loaded_thys) end;
   2.276      in if thy_uptodate andalso ml_uptodate then ()
   2.277         else
   2.278         (
   2.279 +         delete_thms ();
   2.280 +
   2.281           if thy_uptodate orelse thy_file = "" then ()
   2.282           else (writeln ("Reading \"" ^ name ^ ".thy\"");
   2.283 -               read_thy thy_name thy_file;
   2.284 -               use (out_name thy_name)
   2.285 +               read_thy tname thy_file;
   2.286 +               use (out_name tname)
   2.287                );
   2.288  
   2.289           if ml_file = "" then () 
   2.290           else (writeln ("Reading \"" ^ name ^ ".ML\"");
   2.291                 use ml_file);
   2.292  
   2.293 -         use_string ["store_theory " ^ quote thy_name ^ " " ^ thy_name 
   2.294 -                     ^ ".thy;"];
   2.295 +         use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
   2.296  
   2.297           (*Now set the correct info*)
   2.298 -         set_info (file_info thy_file) (file_info ml_file) thy_name;
   2.299 +         set_info (file_info thy_file) (file_info ml_file) tname;
   2.300           set_path ();
   2.301  
   2.302           (*Mark theories that have to be reloaded*)
   2.303 -         mark_children thy_name;
   2.304 +         mark_children tname;
   2.305  
   2.306           (*Remove temporary files*)
   2.307           if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate 
   2.308             then ()
   2.309 -         else delete_file (out_name thy_name)
   2.310 +         else delete_file (out_name tname)
   2.311          )
   2.312      end;
   2.313  
   2.314 @@ -294,13 +285,12 @@
   2.315                        let val thy = get_thyinfo t
   2.316                        in if is_some thy then
   2.317                               let val ThyInfo {children, ...} = the thy
   2.318 -                             in children union (next_level ts)
   2.319 -                             end
   2.320 +                             in children union (next_level ts) end
   2.321                           else next_level ts
   2.322                        end
   2.323                    | next_level [] = [];
   2.324                    
   2.325 -                val children = next_level thys
   2.326 +                val children = next_level thys;
   2.327              in load_order children ((result \\ children) @ children) end;
   2.328  
   2.329        fun reload_changed (t :: ts) =
   2.330 @@ -324,19 +314,15 @@
   2.331         If there are still children in the deleted theory's list
   2.332         schedule them for reloading *)
   2.333       fun collect_garbage not_garbage =
   2.334 -       let fun collect (t :: ts) =
   2.335 -                 let val ThyInfo {name, children, ...} = t
   2.336 -                 in if name mem not_garbage then collect ts
   2.337 -                    else (writeln("Theory \"" ^ name 
   2.338 -                           ^ "\" is no longer linked with Pure - removing it.");
   2.339 -                          remove_thy name;
   2.340 -                          seq mark_outdated children
   2.341 -                         )
   2.342 -                 end
   2.343 +       let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
   2.344 +                 if tname mem not_garbage then collect ts
   2.345 +                 else (writeln ("Theory \"" ^ tname 
   2.346 +                         ^ "\" is no longer linked with Pure - removing it.");
   2.347 +                       remove_thy tname;
   2.348 +                       seq mark_outdated children)
   2.349               | collect [] = ()
   2.350  
   2.351 -       in collect (!loaded_thys) end
   2.352 -
   2.353 +       in collect (alist_of (!loaded_thys)) end;
   2.354    in collect_garbage ("Pure" :: (load_order ["Pure"] []));
   2.355       reload_changed (load_order ["Pure"] [])
   2.356    end;
   2.357 @@ -370,28 +356,24 @@
   2.358                    end
   2.359              in find_it "" child end;
   2.360          
   2.361 -          (*Check if a cycle will be created by add_child *)
   2.362 +          (*Check if a cycle would be created by add_child *)
   2.363            fun find_cycle base =
   2.364              if base mem (list_descendants [child]) then show_cycle base
   2.365              else ();
   2.366                     
   2.367            (*Add child to child list of base *)
   2.368            fun add_child base =
   2.369 -            let fun add (t :: loaded) =
   2.370 -                      let val ThyInfo {name, path, children,
   2.371 -                                       thy_info, ml_info, theory} = t
   2.372 -                      in if name = base then
   2.373 -                           ThyInfo {name = name, path = path,
   2.374 -                                    children = child ins children,
   2.375 -                                    thy_info = thy_info, ml_info = ml_info,
   2.376 -                                    theory = theory} :: loaded
   2.377 -                         else
   2.378 -                           t :: (add loaded)
   2.379 -                      end
   2.380 -                  | add [] =
   2.381 -                      [ThyInfo {name = base, path = "", children = [child], 
   2.382 -                               thy_info = None, ml_info = None, theory = None}]
   2.383 -            in loaded_thys := add (!loaded_thys) end;       
   2.384 +            let val tinfo =
   2.385 +                  case lookup (!loaded_thys, base) of
   2.386 +                      Some (ThyInfo {path, children, thy_time, ml_time, 
   2.387 +                                     theory, thms}) =>
   2.388 +                        ThyInfo {path = path, children = child ins children,
   2.389 +                                 thy_time = thy_time, ml_time = ml_time,
   2.390 +                                 theory = theory, thms = thms}
   2.391 +                    | None => ThyInfo {path = "", children = [child],
   2.392 +                                       thy_time = None, ml_time = None, 
   2.393 +                                       theory = None, thms = null};
   2.394 +            in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
   2.395  
   2.396            (*Load a base theory if not already done
   2.397              and no cycle would be created *)
   2.398 @@ -433,21 +415,60 @@
   2.399  
   2.400  (*Change theory object for an existent item of loaded_thys 
   2.401    or create a new item *)
   2.402 -fun store_theory thy_name thy =
   2.403 -  let fun make_change (t :: loaded) =
   2.404 -            let val ThyInfo {name, path, children, thy_info, ml_info, ...} = t
   2.405 -            in if name = thy_name then            
   2.406 -                    ThyInfo {name = name, path = path, children = children,
   2.407 -                             thy_info = thy_info, ml_info = ml_info,
   2.408 -                             theory = Some thy} :: loaded
   2.409 -               else
   2.410 -                    t :: (make_change loaded)
   2.411 -            end
   2.412 -        | make_change [] =
   2.413 -            [ThyInfo {name = thy_name, path = "", children = [],
   2.414 -                      thy_info = Some "", ml_info = Some "",
   2.415 -                      theory = Some thy}]
   2.416 -  in loaded_thys := make_change (!loaded_thys) end;
   2.417 +fun store_theory (thy, tname) =
   2.418 +  let val tinfo = case lookup (!loaded_thys, tname) of 
   2.419 +               Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) =>
   2.420 +                 ThyInfo {path = path, children = children,
   2.421 +                          thy_time = thy_time, ml_time = ml_time,
   2.422 +                          theory = Some thy, thms = thms}
   2.423 +             | None => ThyInfo {path = "", children = [],
   2.424 +                                thy_time = Some "", ml_time = Some "",
   2.425 +                                theory = Some thy, thms = null};
   2.426 +  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
   2.427 +
   2.428 +(*Store a theorem in the ThyInfo of the theory it is associated with*)
   2.429 +fun store_thm (thm, tname) =
   2.430 +  let val thy_name = !(hd (stamps_of_thm thm));
   2.431 +
   2.432 +      val ThyInfo {path, children, thy_time, ml_time, theory, thms} =
   2.433 +        case get_thyinfo thy_name of
   2.434 +            Some tinfo => tinfo
   2.435 +          | None => error ("store_thm: Theory \"" ^ thy_name 
   2.436 +                           ^ "\" is not stored in loaded_thys");
   2.437 +  in loaded_thys := 
   2.438 +       Symtab.update ((thy_name, ThyInfo {path = path, children = children,
   2.439 +                                   thy_time = thy_time, ml_time = ml_time,
   2.440 +                                   theory = theory, 
   2.441 +                                   thms = Symtab.update ((tname, thm), thms)}),
   2.442 +                      !loaded_thys);
   2.443 +     thm
   2.444 +  end;
   2.445  
   2.446 +(*Store theorem in loaded_thys and a ML variable*)
   2.447 +fun qed name = use_string ["val " ^ name ^ " = store_thm (result(), "
   2.448 +                           ^ quote name ^ ");"];
   2.449 +
   2.450 +fun name_of_thy thy = !(hd (stamps_of_thy thy));
   2.451 +
   2.452 +(*Retrieve a theorem specified by theory and name*)
   2.453 +fun get_thm thy tname =
   2.454 +  let val thy_name = name_of_thy thy;
   2.455 +
   2.456 +      val ThyInfo {thms, ...} = 
   2.457 +        case get_thyinfo thy_name of
   2.458 +            Some tinfo => tinfo
   2.459 +          | None => error ("get_thm: Theory \"" ^ thy_name
   2.460 +                           ^ "\" is not stored in loaded_thys");
   2.461 +  in the (lookup (thms, tname)) end;
   2.462 +
   2.463 +(*Retrieve all theorems belonging to the specified theory*)
   2.464 +fun get_thms thy =
   2.465 +  let val thy_name = name_of_thy thy;
   2.466 +
   2.467 +      val ThyInfo {thms, ...} = 
   2.468 +        case get_thyinfo thy_name of
   2.469 +            Some tinfo => tinfo
   2.470 +          | None => error ("get_thms: Theory \"" ^ thy_name
   2.471 +                           ^ "\" is not stored in loaded_thys");
   2.472 +  in alist_of thms end;
   2.473  end;
   2.474 -
     3.1 --- a/src/Pure/Thy/thy_syn.ML	Fri Jul 15 12:24:05 1994 +0200
     3.2 +++ b/src/Pure/Thy/thy_syn.ML	Fri Jul 15 13:30:42 1994 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4  
     3.5  signature THY_SYN =
     3.6  sig
     3.7 -  val parse: string -> string
     3.8 +  val parse: string -> string -> string
     3.9  end;
    3.10  
    3.11  functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN =