tuned;
authorwenzelm
Thu Oct 23 12:43:07 1997 +0200 (1997-10-23)
changeset 39761030dd79720b
parent 3975 ddeb5a0fd08d
child 3977 9b3cbfd6a936
tuned;
src/Pure/Thy/browser_info.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_read.ML
     1.1 --- a/src/Pure/Thy/browser_info.ML	Thu Oct 23 12:13:15 1997 +0200
     1.2 +++ b/src/Pure/Thy/browser_info.ML	Thu Oct 23 12:43:07 1997 +0200
     1.3 @@ -173,7 +173,7 @@
     1.4  
     1.5      (*Make list of all theories and all theories that own a .thy file*)
     1.6      fun list_theories [] theories thy_files = (theories, thy_files)
     1.7 -      | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)
     1.8 +      | list_theories ((tname, {thy_time, ...}: thy_info) :: ts)
     1.9                        theories thy_files =
    1.10            list_theories ts (tname :: theories)
    1.11              (if is_some thy_time andalso the thy_time <> "" then
    1.12 @@ -741,7 +741,7 @@
    1.13  fun mk_graph tname abs_path = if not (!make_graph) then () else
    1.14    let val parents =
    1.15          map (fn (t, _) => tack_on (path_of t) t)
    1.16 -          (filter (fn (_, ThyInfo {children,...}) => tname mem children)
    1.17 +          (filter (fn (_, {children,...}) => tname mem children)
    1.18               (Symtab.dest(!loaded_thys)));
    1.19  
    1.20        val dir_name = relative_path
     2.1 --- a/src/Pure/Thy/thm_database.ML	Thu Oct 23 12:13:15 1997 +0200
     2.2 +++ b/src/Pure/Thy/thm_database.ML	Thu Oct 23 12:43:07 1997 +0200
     2.3 @@ -273,7 +273,7 @@
     2.4    and in the theory's HTML file*)
     2.5  fun store_thm (name, thm) =
     2.6    let
     2.7 -    val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time,
     2.8 +    val (thy_name, {path, children, parents, thy_time, ml_time,
     2.9                              theory, thms, methods, data}) =
    2.10        thyinfo_of_sign (#sign (rep_thm thm))
    2.11  
    2.12 @@ -290,7 +290,7 @@
    2.13      val thm' = Thm.name_thm (name, thm)
    2.14    in
    2.15      loaded_thys := Symtab.update
    2.16 -     ((thy_name, ThyInfo {path = path, children = children, parents = parents,
    2.17 +     ((thy_name, {path = path, children = children, parents = parents,
    2.18                            thy_time = thy_time, ml_time = ml_time,
    2.19                            theory = theory, thms = thms',
    2.20                            methods = methods, data = data}),
    2.21 @@ -329,12 +329,12 @@
    2.22  
    2.23  (*Get all theorems belonging to a given theory*)
    2.24  fun thmtab_of_thy thy =
    2.25 -  let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
    2.26 +  let val (_, {thms, ...}) = thyinfo_of_sign (sign_of thy);
    2.27    in thms end;
    2.28  
    2.29  
    2.30  fun thmtab_of_name name =
    2.31 -  let val ThyInfo {thms, ...} = the (get_thyinfo name);
    2.32 +  let val {thms, ...} = the (get_thyinfo name);
    2.33    in thms end;
    2.34  
    2.35  
    2.36 @@ -361,15 +361,15 @@
    2.37  fun delete_thms tname =
    2.38    let
    2.39      val tinfo = case get_thyinfo tname of
    2.40 -        Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
    2.41 +        Some ({path, children, parents, thy_time, ml_time, theory,
    2.42                         methods, data, ...}) =>
    2.43 -          ThyInfo {path = path, children = children, parents = parents,
    2.44 +          {path = path, children = children, parents = parents,
    2.45                     thy_time = thy_time, ml_time = ml_time,
    2.46                     theory = theory, thms = Symtab.null,
    2.47                     methods = methods, data = data}
    2.48        | None => error ("Theory " ^ tname ^ " not stored by loader");
    2.49  
    2.50 -    val ThyInfo {theory, ...} = tinfo;
    2.51 +    val {theory, ...} = tinfo;
    2.52    in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
    2.53       case theory of
    2.54           Some t => delete_thm_db t
     3.1 --- a/src/Pure/Thy/thy_info.ML	Thu Oct 23 12:13:15 1997 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Oct 23 12:43:07 1997 +0200
     3.3 @@ -1,27 +1,29 @@
     3.4  (*  Title:      Pure/Thy/thy_info.ML
     3.5      ID:         $Id$
     3.6 -    Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
     3.7 -                Tobias Nipkow and L C Paulson
     3.8 -    Copyright   1994 TU Muenchen
     3.9 +    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    3.10  
    3.11 -Functions for storing and retrieving arbitrary theory information.
    3.12 +Theory loader info database.
    3.13  *)
    3.14  
    3.15 -(*Types for theory storage*)
    3.16 -
    3.17 +(* FIXME wipe out! *)
    3.18  (*Functions to handle arbitrary data added by the user; type "exn" is used
    3.19    to store data*)
    3.20  datatype thy_methods =
    3.21    ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
    3.22  
    3.23 -datatype thy_info =
    3.24 -  ThyInfo of {path: string,
    3.25 -              children: string list, parents: string list,
    3.26 -              thy_time: string option, ml_time: string option,
    3.27 -              theory: theory option, thms: thm Symtab.table,
    3.28 -              methods: thy_methods Symtab.table,
    3.29 -              data: exn Symtab.table * exn Symtab.table};
    3.30 -      (*thy_time, ml_time = None     theory file has not been read yet
    3.31 +
    3.32 +type thy_info =
    3.33 +  {path: string,
    3.34 +    children: string list, parents: string list,
    3.35 +    thy_time: string option, ml_time: string option,
    3.36 +    theory: theory option, thms: thm Symtab.table,
    3.37 +    methods: thy_methods Symtab.table,
    3.38 +    data: exn Symtab.table * exn Symtab.table};
    3.39 +
    3.40 +(*
    3.41 +        path: directory where theory's files are located
    3.42 +
    3.43 +        thy_time, ml_time = None     theory file has not been read yet
    3.44                            = Some ""  theory was read but has either been marked
    3.45                                       as outdated or there is no such file for
    3.46                                       this theory (see e.g. 'virtual' theories
    3.47 @@ -44,8 +46,7 @@
    3.48                if ML files has not been read, second element is identical to
    3.49                first one because get_thydata, which is meant to return the
    3.50                latest data, always accesses the 2nd element
    3.51 -       *)
    3.52 -
    3.53 +*)
    3.54  
    3.55  signature THY_INFO =
    3.56  sig
    3.57 @@ -57,7 +58,6 @@
    3.58    val theory_of_thm  : thm -> theory
    3.59    val children_of    : string -> string list
    3.60    val parents_of_name: string -> string list
    3.61 -  val thyname_of_sign: Sign.sg -> string
    3.62    val thyinfo_of_sign: Sign.sg -> string * thy_info
    3.63  
    3.64    val add_thydata    : string -> string * thy_methods -> unit
    3.65 @@ -70,111 +70,82 @@
    3.66  end;
    3.67  
    3.68  
    3.69 -
    3.70  structure ThyInfo: THY_INFO =
    3.71  struct
    3.72  
    3.73 +(* loaded theories *)
    3.74  
    3.75 +fun mk_info (name, children, parents, theory) =
    3.76 +  (name,
    3.77 +    {path = "", children = children, parents = parents, thy_time = Some "",
    3.78 +      ml_time = Some "", theory = Some theory, thms = Symtab.null,
    3.79 +      methods = Symtab.null, data = (Symtab.null, Symtab.null)}: thy_info);
    3.80 +
    3.81 +(*preloaded theories*)
    3.82  val loaded_thys =
    3.83 -  ref (Symtab.make [("ProtoPure",
    3.84 -                     ThyInfo {path = "",
    3.85 -                              children = ["Pure", "CPure"], parents = [],
    3.86 -                              thy_time = Some "", ml_time = Some "",
    3.87 -                              theory = Some proto_pure_thy,
    3.88 -                              thms = Symtab.null, methods = Symtab.null,
    3.89 -                              data = (Symtab.null, Symtab.null)}),
    3.90 -                    ("Pure",
    3.91 -                     ThyInfo {path = "", children = [],
    3.92 -                              parents = ["ProtoPure"],
    3.93 -                              thy_time = Some "", ml_time = Some "",
    3.94 -                              theory = Some pure_thy, thms = Symtab.null,
    3.95 -                              methods = Symtab.null,
    3.96 -                              data = (Symtab.null, Symtab.null)}),
    3.97 -                    ("CPure",
    3.98 -                     ThyInfo {path = "",
    3.99 -                              children = [], parents = ["ProtoPure"],
   3.100 -                              thy_time = Some "", ml_time = Some "",
   3.101 -                              theory = Some cpure_thy,
   3.102 -                              thms = Symtab.null,
   3.103 -                              methods = Symtab.null,
   3.104 -                              data = (Symtab.null, Symtab.null)})
   3.105 -                   ]);
   3.106 +  ref (Symtab.make (map mk_info
   3.107 +    [("ProtoPure", ["Pure", "CPure"], [], Theory.proto_pure),
   3.108 +     ("Pure", [], ["ProtoPure"], Theory.pure),
   3.109 +     ("CPure", [], ["ProtoPure"], Theory.cpure)]));
   3.110  
   3.111  
   3.112 -(*Get thy_info for a loaded theory *)
   3.113 -fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
   3.114 +(* retrieve info *)
   3.115 +
   3.116 +fun err_not_stored name =
   3.117 +  error ("Theory " ^ name ^ " not stored by loader");
   3.118 +
   3.119 +fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
   3.120  
   3.121 -(*Get path where theory's files are located*)
   3.122 -fun path_of tname =
   3.123 -  let val ThyInfo {path, ...} = the (get_thyinfo tname)
   3.124 -  in path end;
   3.125 +fun the_thyinfo name =
   3.126 +  (case get_thyinfo name of
   3.127 +    Some info => info
   3.128 +  | None => err_not_stored name);
   3.129 +
   3.130 +fun thyinfo_of_sign sg =
   3.131 +  let val name = Sign.name_of sg
   3.132 +  in (name, the_thyinfo name) end;
   3.133  
   3.134  
   3.135 -(*Guess the name of a theory object
   3.136 -  (First the quick way by looking at the stamps; if that doesn't work,
   3.137 -   we search loaded_thys for the first theory which fits.)
   3.138 -*)
   3.139 -fun thyname_of_sign sg =
   3.140 -  let val ref xname = hd (#stamps (Sign.rep_sg sg));
   3.141 -      val opt_info = get_thyinfo xname;
   3.142 -
   3.143 -    fun eq_sg (ThyInfo {theory = None, ...}) = false
   3.144 -      | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);
   3.145 -
   3.146 -    val show_sg = Pretty.str_of o Sign.pretty_sg;
   3.147 -  in
   3.148 -    if is_some opt_info andalso eq_sg (the opt_info) then xname
   3.149 -    else
   3.150 -      (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of
   3.151 -        Some (name, _) => name
   3.152 -      | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))
   3.153 -  end;
   3.154 -
   3.155 -
   3.156 -(*Guess to which theory a signature belongs and return it's thy_info*)
   3.157 -fun thyinfo_of_sign sg =
   3.158 -  let val name = thyname_of_sign sg;
   3.159 -  in (name, the (get_thyinfo name)) end;
   3.160 +(*path where theory's files are located*)
   3.161 +val path_of = #path o the_thyinfo;
   3.162  
   3.163  
   3.164 -(*Try to get the theory object corresponding to a given signature*)
   3.165 +(*try to get the theory object corresponding to a given signature*)
   3.166  fun theory_of_sign sg =
   3.167    (case thyinfo_of_sign sg of
   3.168 -    (_, ThyInfo {theory = Some thy, ...}) => thy
   3.169 +    (_, {theory = Some thy, ...}) => thy
   3.170    | _ => sys_error "theory_of_sign");
   3.171  
   3.172 +(*try to get the theory object corresponding to a given theorem*)
   3.173 +val theory_of_thm = theory_of_sign o #sign o rep_thm;
   3.174  
   3.175 -(*Try to get the theory object corresponding to a given theorem*)
   3.176 -val theory_of_thm = theory_of_sign o #sign o rep_thm;
   3.177 +(*get all direct descendants of a theory*)
   3.178 +fun children_of t =
   3.179 +  (case get_thyinfo t of
   3.180 +    Some ({children, ...}) => children
   3.181 +  | None => []);
   3.182 +
   3.183 +(*get all direct ancestors of a theory*)
   3.184 +fun parents_of_name t =
   3.185 +  (case get_thyinfo t of
   3.186 +    Some ({parents, ...}) => parents
   3.187 +  | None => []);
   3.188 +
   3.189 +(*get theory object for a loaded theory*)
   3.190 +fun theory_of name =
   3.191 +  (case get_thyinfo name of
   3.192 +    Some ({theory = Some t, ...}) => t
   3.193 +  | _ => err_not_stored name);
   3.194  
   3.195  
   3.196 -(*Get all direct descendants of a theory*)
   3.197 -fun children_of t =
   3.198 -  case get_thyinfo t of Some (ThyInfo {children, ...}) => children
   3.199 -                      | None => [];
   3.200 -
   3.201 -
   3.202 -(*Get all direct ancestors of a theory*)
   3.203 -fun parents_of_name t =
   3.204 -  case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
   3.205 -                      | None => [];
   3.206 -
   3.207 -
   3.208 -(*Get theory object for a loaded theory *)
   3.209 -fun theory_of name =
   3.210 -  case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t
   3.211 -                         | _ => error ("Theory " ^ name ^
   3.212 -                                       " not stored by loader");
   3.213 -
   3.214 -
   3.215 -(*Invoke every put method stored in a theory's methods table to initialize
   3.216 +(*invoke every put method stored in a theory's methods table to initialize
   3.217    the state of user defined variables*)
   3.218  fun put_thydata first tname =
   3.219    let val (methods, data) = 
   3.220          case get_thyinfo tname of
   3.221 -            Some (ThyInfo {methods, data, ...}) => 
   3.222 +            Some ({methods, data, ...}) =>
   3.223                (methods, Symtab.dest ((if first then fst else snd) data))
   3.224 -          | None => error ("Theory " ^ tname ^ " not stored by loader");
   3.225 +          | None => err_not_stored tname;
   3.226  
   3.227        fun put_data (id, date) =
   3.228              case Symtab.lookup (methods, id) of
   3.229 @@ -190,9 +161,9 @@
   3.230  (*Change theory object for an existent item of loaded_thys*)
   3.231  fun store_theory (thy, tname) =
   3.232    let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   3.233 -               Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,
   3.234 +               Some ({path, children, parents, thy_time, ml_time, thms,
   3.235                                methods, data, ...}) =>
   3.236 -                 ThyInfo {path = path, children = children, parents = parents,
   3.237 +                 {path = path, children = children, parents = parents,
   3.238                            thy_time = thy_time, ml_time = ml_time,
   3.239                            theory = Some thy, thms = thms,
   3.240                            methods = methods, data = data}
   3.241 @@ -204,12 +175,9 @@
   3.242  
   3.243  (*Add data handling methods to theory*)
   3.244  fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
   3.245 -  let val ThyInfo {path, children, parents, thy_time, ml_time, theory,
   3.246 -                   thms, methods, data} =
   3.247 -        case get_thyinfo tname of
   3.248 -            Some ti => ti
   3.249 -          | None => error ("Theory " ^ tname ^ " not stored by loader");
   3.250 -  in loaded_thys := Symtab.update ((tname, ThyInfo {path = path,
   3.251 +  let val {path, children, parents, thy_time, ml_time, theory,
   3.252 +                   thms, methods, data} = the_thyinfo tname;
   3.253 +  in loaded_thys := Symtab.update ((tname, {path = path,
   3.254         children = children, parents = parents, thy_time = thy_time,
   3.255         ml_time = ml_time, theory = theory, thms = thms,
   3.256         methods = Symtab.update (new_methods, methods), data = data}),
   3.257 @@ -217,11 +185,9 @@
   3.258    end;
   3.259  
   3.260  
   3.261 -(*Retrieve data associated with theory*)
   3.262 -fun get_thydata tname id =
   3.263 -  let val d2 = case get_thyinfo tname of
   3.264 -                   Some (ThyInfo {data, ...}) => snd data
   3.265 -                 | None => error ("Theory " ^ tname ^ " not stored by loader");
   3.266 -  in Symtab.lookup (d2, id) end;
   3.267 +(*retrieve data associated with theory*)
   3.268 +fun get_thydata name id =
   3.269 +  Symtab.lookup (snd (#data (the_thyinfo name)), id);
   3.270 +
   3.271  
   3.272  end;
     4.1 --- a/src/Pure/Thy/thy_read.ML	Thu Oct 23 12:13:15 1997 +0200
     4.2 +++ b/src/Pure/Thy/thy_read.ML	Thu Oct 23 12:43:07 1997 +0200
     4.3 @@ -66,7 +66,7 @@
     4.4  fun already_loaded thy =
     4.5    let val t = get_thyinfo thy
     4.6    in if is_none t then false
     4.7 -     else let val ThyInfo {thy_time, ml_time, ...} = the t
     4.8 +     else let val {thy_time, ml_time, ...} = the t
     4.9            in is_some thy_time andalso is_some ml_time end
    4.10    end;
    4.11  
    4.12 @@ -75,7 +75,7 @@
    4.13    Return a pair of boolean values for .thy and for .ML *)
    4.14  fun thy_unchanged thy thy_file ml_file =
    4.15    case get_thyinfo thy of
    4.16 -      Some (ThyInfo {thy_time, ml_time, ...}) =>
    4.17 +      Some {thy_time, ml_time, ...} =>
    4.18         let val tn = is_none thy_time;
    4.19             val mn = is_none ml_time
    4.20         in if not tn andalso not mn then
    4.21 @@ -136,7 +136,7 @@
    4.22  
    4.23        val tinfo = get_thyinfo name;
    4.24    in if is_some tinfo andalso path = "" then
    4.25 -       let val ThyInfo {path = abs_path, ...} = the tinfo;
    4.26 +       let val {path = abs_path, ...} = the tinfo;
    4.27             val (thy_file, ml_file) = if abs_path = "" then new_filename ()
    4.28                                       else (find_file abs_path (name ^ ".thy"),
    4.29                                             find_file abs_path (name ^ ".ML"))
    4.30 @@ -154,9 +154,9 @@
    4.31  
    4.32  (*Remove theory from all child lists in loaded_thys *)
    4.33  fun unlink_thy tname =
    4.34 -  let fun remove (ThyInfo {path, children, parents, thy_time, ml_time,
    4.35 +  let fun remove ({path, children, parents, thy_time, ml_time,
    4.36                             theory, thms, methods, data}) =
    4.37 -        ThyInfo {path = path, children = children \ tname, parents = parents,
    4.38 +        {path = path, children = children \ tname, parents = parents,
    4.39                   thy_time = thy_time, ml_time = ml_time, theory = theory, 
    4.40                   thms = thms, methods = methods, data = data}
    4.41    in loaded_thys := Symtab.map remove (!loaded_thys) end;
    4.42 @@ -171,9 +171,9 @@
    4.43  (*Change thy_time and ml_time for an existent item *)
    4.44  fun set_info tname thy_time ml_time =
    4.45    let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
    4.46 -          Some (ThyInfo {path, children, parents, theory, thms,
    4.47 +          Some ({path, children, parents, theory, thms,
    4.48                           methods, data, ...}) =>
    4.49 -            ThyInfo {path = path, children = children, parents = parents,
    4.50 +            {path = path, children = children, parents = parents,
    4.51                       thy_time = thy_time, ml_time = ml_time,
    4.52                       theory = theory, thms = thms,
    4.53                       methods = methods, data = data}
    4.54 @@ -186,7 +186,7 @@
    4.55    let val t = get_thyinfo tname;
    4.56    in if is_none t then ()
    4.57       else
    4.58 -       let val ThyInfo {thy_time, ml_time, ...} = the t
    4.59 +       let val {thy_time, ml_time, ...} = the t
    4.60         in set_info tname (if is_none thy_time then None else Some "")
    4.61                           (if is_none ml_time then None else Some "")
    4.62         end
    4.63 @@ -217,11 +217,11 @@
    4.64  
    4.65      (*Set absolute path for loaded theory *)
    4.66      fun set_path () =
    4.67 -      let val ThyInfo {children, parents, thy_time, ml_time, theory, thms,
    4.68 +      let val {children, parents, thy_time, ml_time, theory, thms,
    4.69                         methods, data, ...} =
    4.70              the (Symtab.lookup (!loaded_thys, tname));
    4.71        in loaded_thys := Symtab.update ((tname,
    4.72 -                          ThyInfo {path = abs_path,
    4.73 +                          {path = abs_path,
    4.74                                     children = children, parents = parents,
    4.75                                     thy_time = thy_time, ml_time = ml_time,
    4.76                                     theory = theory, thms = thms,
    4.77 @@ -245,7 +245,7 @@
    4.78      (*Invoke every get method stored in the methods table and store result in
    4.79        data table*)
    4.80      fun save_data thy_only =
    4.81 -      let val ThyInfo {path, children, parents, thy_time, ml_time,
    4.82 +      let val {path, children, parents, thy_time, ml_time,
    4.83                         theory, thms, methods, data} = the (get_thyinfo tname);
    4.84  
    4.85            fun get_data [] data = data
    4.86 @@ -257,7 +257,7 @@
    4.87            val data' = (if thy_only then new_data else fst data, new_data)
    4.88                        (* 2nd component must be up to date *)
    4.89        in loaded_thys := Symtab.update
    4.90 -           ((tname, ThyInfo {path = path,
    4.91 +           ((tname, {path = path,
    4.92                               children = children, parents = parents,
    4.93                               thy_time = thy_time, ml_time = ml_time,
    4.94                               theory = theory, thms = thms,
    4.95 @@ -267,7 +267,7 @@
    4.96  
    4.97      (*Make sure that loaded_thys contains an entry for tname*)
    4.98      fun init_thyinfo () =
    4.99 -    let val tinfo = ThyInfo {path = "", children = [], parents = [],
   4.100 +    let val tinfo = {path = "", children = [], parents = [],
   4.101                               thy_time = None, ml_time = None,
   4.102                               theory = None, thms = Symtab.null,
   4.103                               methods = Symtab.null,
   4.104 @@ -372,7 +372,7 @@
   4.105  
   4.106        fun reload_changed (t :: ts) =
   4.107              let val abspath = case get_thyinfo t of
   4.108 -                                  Some (ThyInfo {path, ...}) => path
   4.109 +                                  Some ({path, ...}) => path
   4.110                                  | None => "";
   4.111  
   4.112                  val (thy_file, ml_file) = get_filenames abspath t;
   4.113 @@ -388,7 +388,7 @@
   4.114         If there are still children in the deleted theory's list
   4.115         schedule them for reloading *)
   4.116       fun collect_garbage no_garbage =
   4.117 -       let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
   4.118 +       let fun collect ((tname, {children, ...}: thy_info) :: ts) =
   4.119                   if tname mem no_garbage then collect ts
   4.120                   else (writeln ("Theory \"" ^ tname ^
   4.121                         "\" is no longer linked with ProtoPure - removing it.");
   4.122 @@ -413,7 +413,7 @@
   4.123                     error ("Cyclic dependency of theories: "
   4.124                            ^ child ^ "->" ^ base ^ result)
   4.125                   else if is_some tinfo then
   4.126 -                   let val ThyInfo {children, ...} = the tinfo
   4.127 +                   let val {children, ...} = the tinfo
   4.128                     in seq (find_it ("->" ^ curr ^ result)) children
   4.129                     end
   4.130                   else ()
   4.131 @@ -429,14 +429,14 @@
   4.132        fun add_child base =
   4.133          let val tinfo =
   4.134                case Symtab.lookup (!loaded_thys, base) of
   4.135 -                  Some (ThyInfo {path, children, parents, thy_time, ml_time,
   4.136 +                  Some ({path, children, parents, thy_time, ml_time,
   4.137                             theory, thms, methods, data}) =>
   4.138 -                    ThyInfo {path = path,
   4.139 +                    {path = path,
   4.140                               children = child ins children, parents = parents,
   4.141                               thy_time = thy_time, ml_time = ml_time,
   4.142                               theory = theory, thms = thms,
   4.143                               methods = methods, data = data}
   4.144 -                | None => ThyInfo {path = "", children = [child], parents = [],
   4.145 +                | None => {path = "", children = [child], parents = [],
   4.146                                     thy_time = None, ml_time = None,
   4.147                                     theory = None, thms = Symtab.null,
   4.148                                     methods = Symtab.null,
   4.149 @@ -480,13 +480,13 @@
   4.150  
   4.151        val datas =
   4.152          let fun get_data t =
   4.153 -              let val ThyInfo {data, ...} = the (get_thyinfo t)
   4.154 +              let val {data, ...} = the (get_thyinfo t)
   4.155                in snd data end;
   4.156          in map (Symtab.dest o get_data) mergelist end;
   4.157  
   4.158        val methods =
   4.159          let fun get_methods t =
   4.160 -              let val ThyInfo {methods, ...} = the (get_thyinfo t)
   4.161 +              let val {methods, ...} = the (get_thyinfo t)
   4.162                in methods end;
   4.163  
   4.164              val ms = map get_methods mergelist;
   4.165 @@ -536,9 +536,9 @@
   4.166  
   4.167        val dummy =
   4.168          let val tinfo = case Symtab.lookup (!loaded_thys, child) of
   4.169 -              Some (ThyInfo {path, children, thy_time, ml_time, theory, thms,
   4.170 +              Some ({path, children, thy_time, ml_time, theory, thms,
   4.171                               data, ...}) =>
   4.172 -                 ThyInfo {path = path,
   4.173 +                 {path = path,
   4.174                            children = children, parents = mergelist,
   4.175                            thy_time = thy_time, ml_time = ml_time,
   4.176                            theory = theory, thms = thms,