src/Pure/Thy/thy_read.ML
author wenzelm
Wed Jan 29 15:45:40 1997 +0100 (1997-01-29)
changeset 2564 9d66b758bce5
parent 2406 7becd4dd5ca7
child 3039 bbf4e3738ef0
permissions -rw-r--r--
removed warning for unprintable chars in strings (functionality will
be put into administrative script);
     1 (*  Title:      Pure/Thy/thy_read.ML
     2     ID:         $Id$
     3     Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
     4                 Tobias Nipkow and L C Paulson
     5     Copyright   1994 TU Muenchen
     6 
     7 Functions for reading theory files, and storing and retrieving theories,
     8 theorems and the global simplifier set.
     9 *)
    10 
    11 (*Types for theory storage*)
    12 
    13 (*Functions to handle arbitrary data added by the user; type "exn" is used
    14   to store data*)
    15 datatype thy_methods =
    16   ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
    17 
    18 datatype thy_info =
    19   ThyInfo of {path: string,
    20               children: string list, parents: string list,
    21               thy_time: string option, ml_time: string option,
    22               theory: theory option, thms: thm Symtab.table,
    23               methods: thy_methods Symtab.table,
    24               data: exn Symtab.table * exn Symtab.table};
    25       (*thy_time, ml_time = None     theory file has not been read yet
    26                           = Some ""  theory was read but has either been marked
    27                                      as outdated or there is no such file for
    28                                      this theory (see e.g. 'virtual' theories
    29                                      like Pure or theories without a ML file)
    30         theory = None  theory has not been read yet
    31 
    32         parents: While 'children' contains all theories the theory depends
    33                  on (i.e. also ones quoted in the .thy file),
    34                  'parents' only contains the theories which were used to form
    35                  the base of this theory.
    36 
    37         methods: three methods for each user defined data;
    38                  merge: merges data of ancestor theories
    39                  put: retrieves data from loaded_thys and stores it somewhere
    40                  get: retrieves data from somewhere and stores it
    41                       in loaded_thys
    42                  Warning: If these functions access reference variables inside
    43                           READTHY, they have to be redefined each time
    44                           init_thy_reader is invoked
    45         data: user defined data; exn is used to allow arbitrary types;
    46               first element of pairs contains result that get returned after
    47               thy file was read, second element after ML file was read
    48        *)
    49 
    50 signature READTHY =
    51 sig
    52   datatype basetype = Thy  of string
    53                     | File of string
    54 
    55   val loaded_thys    : thy_info Symtab.table ref
    56   val loadpath       : string list ref
    57   val thy_reader_files: string list ref
    58   val delete_tmpfiles: bool ref
    59 
    60   val use_thy        : string -> unit
    61   val time_use_thy   : string -> unit
    62   val use_dir        : string -> unit
    63   val exit_use_dir   : string -> unit
    64   val update         : unit -> unit
    65   val unlink_thy     : string -> unit
    66   val mk_base        : basetype list -> string -> bool -> theory
    67   val store_theory   : theory * string -> unit
    68 
    69   val theory_of      : string -> theory
    70   val theory_of_sign : Sign.sg -> theory
    71   val theory_of_thm  : thm -> theory
    72   val children_of    : string -> string list
    73   val parents_of_name: string -> string list
    74   val thyname_of_sign: Sign.sg -> string
    75 
    76   val store_thm      : string * thm -> thm
    77   val bind_thm       : string * thm -> unit
    78   val qed            : string -> unit
    79   val qed_thm        : thm ref
    80   val qed_goal       : string -> theory -> string 
    81                        -> (thm list -> tactic list) -> unit
    82   val qed_goalw      : string -> theory -> thm list -> string 
    83                        -> (thm list -> tactic list) -> unit
    84   val get_thm        : theory -> string -> thm
    85   val thms_of        : theory -> (string * thm) list
    86   val delete_thms    : string -> unit
    87 
    88   val add_thydata    : string -> string * thy_methods -> unit
    89   val get_thydata    : string -> string -> exn option
    90   val add_thy_reader_file: string -> unit
    91   val set_thy_reader_file: string -> unit
    92   val read_thy_reader_files: unit -> unit
    93   val set_current_thy: string -> unit
    94 
    95   val print_theory   : theory -> unit
    96 
    97   val base_path      : string ref
    98   val gif_path       : string ref
    99   val index_path     : string ref
   100   val pure_subchart  : string option ref
   101   val make_html      : bool ref
   102   val init_html      : unit -> unit
   103   val finish_html    : unit -> unit
   104   val section        : string -> unit
   105 end;
   106 
   107 
   108 functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
   109 struct
   110 
   111 open ThmDB Simplifier;
   112 
   113 datatype basetype = Thy  of string
   114                   | File of string;
   115 
   116 val loaded_thys =
   117   ref (Symtab.make [("ProtoPure",
   118                      ThyInfo {path = "",
   119                               children = ["Pure", "CPure"], parents = [],
   120                               thy_time = Some "", ml_time = Some "",
   121                               theory = Some proto_pure_thy,
   122                               thms = Symtab.null, methods = Symtab.null,
   123                               data = (Symtab.null, Symtab.null)}),
   124                     ("Pure",
   125                      ThyInfo {path = "", children = [],
   126                               parents = ["ProtoPure"],
   127                               thy_time = Some "", ml_time = Some "",
   128                               theory = Some pure_thy, thms = Symtab.null,
   129                               methods = Symtab.null,
   130                               data = (Symtab.null, Symtab.null)}),
   131                     ("CPure",
   132                      ThyInfo {path = "",
   133                               children = [], parents = ["ProtoPure"],
   134                               thy_time = Some "", ml_time = Some "",
   135                               theory = Some cpure_thy,
   136                               thms = Symtab.null,
   137                               methods = Symtab.null,
   138                               data = (Symtab.null, Symtab.null)})
   139                    ]);
   140 
   141 (*Default search path for theory files*)
   142 val loadpath = ref ["."];
   143 
   144 (*Directory given as parameter to use_thy. This is temporarily added to
   145   loadpath while the theory's ancestors are loaded.*)
   146 val tmp_loadpath = ref [] : string list ref;
   147 
   148 (*ML files to be read by init_thy_reader; they normally contain redefinitions
   149   of functions accessing reference variables inside READTHY*)
   150 val thy_reader_files = ref [] : string list ref;
   151 
   152 (*Remove temporary files after use*)
   153 val delete_tmpfiles = ref true;            
   154 
   155 
   156 (*Set location of graphics for HTML files
   157   (When this is executed for the first time we are in $ISABELLE/Pure/Thy.
   158    This path is converted to $ISABELLE/Tools by removing the last two
   159    directories and appending "Tools". All subsequently made ReadThy
   160    structures inherit this value.)
   161 *)
   162 val gif_path = ref (tack_on ("/" ^
   163   space_implode "/" (rev (tl (tl (rev (space_explode "/" 
   164 				       (OS.FileSys.getDir ())))))))
   165   "Tools");
   166 
   167 (*Path of Isabelle's main directory*)
   168 val base_path = ref (
   169   "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ())))))));
   170 
   171 
   172 (** HTML variables **)
   173 
   174 (*Location of .theory-list.txt and index.html (set by init_html)*)
   175 val index_path = ref "";
   176 
   177 (*Location of .Pure_sub.html and .CPure_sub.html*)
   178 val pure_subchart = ref (None : string option);
   179 
   180 (*Controls whether HTML files should be generated*)
   181 val make_html = ref false;
   182 
   183 (*HTML file of theory currently being read
   184   (Initialized by thyfile2html; used by use_thy and store_thm)*)
   185 val cur_htmlfile = ref None : TextIO.outstream option ref;
   186 
   187 (*Boolean variable which indicates if the title "Theorems proved in foo.ML"
   188   has already been inserted into the current HTML file*)
   189 val cur_has_title = ref false;
   190 
   191 (*Name of theory currently being read*)
   192 val cur_thyname = ref "";
   193 
   194 
   195 
   196 (*Make name of the TextIO.output ML file for a theory *)
   197 fun out_name tname = "." ^ tname ^ ".thy.ML";
   198 
   199 (*Read a file specified by thy_file containing theory thy *)
   200 fun read_thy tname thy_file =
   201   let
   202     val instream  = TextIO.openIn thy_file;
   203     val outstream = TextIO.openOut (out_name tname);
   204   in
   205     TextIO.output (outstream, ThySyn.parse tname (TextIO.inputAll instream));
   206     TextIO.closeOut outstream;
   207     TextIO.closeIn instream
   208   end;
   209 
   210 fun file_exists file = (file_info file <> "");
   211 
   212 (*Get last directory in path (e.g. /usr/proj/isabelle -> isabelle) *)
   213 fun last_path s = case space_explode "/" s of
   214                       [] => ""
   215                     | ds => last_elem ds;
   216 
   217 (*Get thy_info for a loaded theory *)
   218 fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
   219 
   220 (*Check if a theory was completly loaded *)
   221 fun already_loaded thy =
   222   let val t = get_thyinfo thy
   223   in if is_none t then false
   224      else let val ThyInfo {thy_time, ml_time, ...} = the t
   225           in is_some thy_time andalso is_some ml_time end
   226   end;
   227 
   228 (*Check if a theory file has changed since its last use.
   229   Return a pair of boolean values for .thy and for .ML *)
   230 fun thy_unchanged thy thy_file ml_file =
   231   case get_thyinfo thy of
   232       Some (ThyInfo {thy_time, ml_time, ...}) =>
   233        let val tn = is_none thy_time;
   234            val mn = is_none ml_time
   235        in if not tn andalso not mn then
   236             ((file_info thy_file = the thy_time),
   237              (file_info ml_file = the ml_time))
   238           else if not tn andalso mn then
   239             (file_info thy_file = the thy_time, false)
   240           else
   241             (false, false)
   242        end
   243     | None => (false, false)
   244 
   245 (*Get all direct descendants of a theory*)
   246 fun children_of t =
   247   case get_thyinfo t of Some (ThyInfo {children, ...}) => children
   248                       | None => [];
   249 
   250 (*Get all direct ancestors of a theory*)
   251 fun parents_of_name t =
   252   case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
   253                       | None => [];
   254 
   255 (*Get all descendants of a theory list *)
   256 fun get_descendants [] = []
   257   | get_descendants (t :: ts) =
   258       let val children = children_of t
   259       in children union (get_descendants (children union ts)) end;
   260 
   261 (*Get theory object for a loaded theory *)
   262 fun theory_of name =
   263   case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t
   264                          | _ => error ("Theory " ^ name ^
   265                                        " not stored by loader");
   266 
   267 (*Get path where theory's files are located*)
   268 fun path_of tname =
   269   let val ThyInfo {path, ...} = the (get_thyinfo tname)
   270   in path end;
   271 
   272 (*Find a file using a list of paths if no absolute or relative path is
   273   specified.*)
   274 fun find_file "" name =
   275       let fun find_it (cur :: paths) =
   276                 if file_exists (tack_on cur name) then
   277                   (if cur = "." then name else tack_on cur name)
   278                 else
   279                   find_it paths
   280            | find_it [] = ""
   281       in find_it (!tmp_loadpath @ !loadpath) end
   282   | find_file path name =
   283       if file_exists (tack_on path name) then tack_on path name
   284                                          else "";
   285 
   286 (*Get absolute pathnames for a new or already loaded theory *)
   287 fun get_filenames path name =
   288   let fun new_filename () =
   289         let val found = find_file path (name ^ ".thy");
   290             val absolute_path = absolute_path (OS.FileSys.getDir ());
   291             val thy_file = absolute_path found;
   292             val (thy_path, _) = split_filename thy_file;
   293             val found = find_file path (name ^ ".ML");
   294             val ml_file = if thy_file = "" then absolute_path found
   295                           else if file_exists (tack_on thy_path (name ^ ".ML"))
   296                           then tack_on thy_path (name ^ ".ML")
   297                           else "";
   298             val searched_dirs = if path = "" then (!tmp_loadpath @ !loadpath)
   299                                              else [path]
   300         in if thy_file = "" andalso ml_file = "" then
   301              error ("Could not find file \"" ^ name ^ ".thy\" or \""
   302                     ^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n"
   303                     ^ "in the following directories: \"" ^
   304                     (space_implode "\", \"" searched_dirs) ^ "\"")
   305            else ();
   306            (thy_file, ml_file)
   307         end;
   308 
   309       val tinfo = get_thyinfo name;
   310   in if is_some tinfo andalso path = "" then
   311        let val ThyInfo {path = abs_path, ...} = the tinfo;
   312            val (thy_file, ml_file) = if abs_path = "" then new_filename ()
   313                                      else (find_file abs_path (name ^ ".thy"),
   314                                            find_file abs_path (name ^ ".ML"))
   315        in if thy_file = "" andalso ml_file = "" then
   316             (warning ("File \"" ^ (tack_on path name)
   317                       ^ ".thy\"\ncontaining theory \"" ^ name
   318                       ^ "\" no longer exists.");
   319              new_filename ()
   320             )
   321           else (thy_file, ml_file)
   322        end
   323      else new_filename ()
   324   end;
   325 
   326 (*Remove theory from all child lists in loaded_thys *)
   327 fun unlink_thy tname =
   328   let fun remove (ThyInfo {path, children, parents, thy_time, ml_time,
   329                            theory, thms, methods, data}) =
   330         ThyInfo {path = path, children = children \ tname, parents = parents,
   331                  thy_time = thy_time, ml_time = ml_time, theory = theory, 
   332                  thms = thms, methods = methods, data = data}
   333   in loaded_thys := Symtab.map remove (!loaded_thys) end;
   334 
   335 (*Remove a theory from loaded_thys *)
   336 fun remove_thy tname =
   337   loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
   338                  (Symtab.dest (!loaded_thys)));
   339 
   340 (*Change thy_time and ml_time for an existent item *)
   341 fun set_info tname thy_time ml_time =
   342   let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   343           Some (ThyInfo {path, children, parents, theory, thms,
   344                          methods, data, ...}) =>
   345             ThyInfo {path = path, children = children, parents = parents,
   346                      thy_time = thy_time, ml_time = ml_time,
   347                      theory = theory, thms = thms,
   348                      methods = methods, data = data}
   349         | None => error ("set_info: theory " ^ tname ^ " not found");
   350   in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
   351 
   352 (*Mark theory as changed since last read if it has been completly read *)
   353 fun mark_outdated tname =
   354   let val t = get_thyinfo tname;
   355   in if is_none t then ()
   356      else
   357        let val ThyInfo {thy_time, ml_time, ...} = the t
   358        in set_info tname (if is_none thy_time then None else Some "")
   359                          (if is_none ml_time then None else Some "")
   360        end
   361   end;
   362 
   363 (*Remove theorems associated with a theory from theory and theorem database*)
   364 fun delete_thms tname =
   365   let
   366     val tinfo = case get_thyinfo tname of
   367         Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
   368                        methods, data, ...}) =>
   369           ThyInfo {path = path, children = children, parents = parents,
   370                    thy_time = thy_time, ml_time = ml_time,
   371                    theory = theory, thms = Symtab.null,
   372                    methods = methods, data = data}
   373       | None => error ("Theory " ^ tname ^ " not stored by loader");
   374 
   375     val ThyInfo {theory, ...} = tinfo;
   376   in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
   377      case theory of
   378          Some t => delete_thm_db t
   379        | None => ()
   380   end;
   381 
   382 (*Make head of HTML dependency charts
   383   Parameters are:
   384     file: HTML file
   385     tname: theory name
   386     suffix: suffix of complementary chart
   387             (sup if this head is for a sub-chart, sub if it is for a sup-chart;
   388              empty for Pure and CPure sub-charts)
   389     gif_path: relative path to directory containing GIFs
   390     index_path: relative path to directory containing main theory chart
   391 *)
   392 fun mk_charthead file tname title repeats gif_path index_path package =
   393   TextIO.output (file,
   394    "<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^
   395    "</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^
   396    "</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^
   397    "<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
   398    \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
   399    \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
   400    \\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^
   401    (if not repeats then "" else
   402       "<BR><TT>...</TT> stands for repeated subtrees") ^
   403    "<P>\n<A HREF = \"" ^ tack_on index_path "index.html\
   404    \\">Back</A> to the index of " ^ package ^ "\n<HR>\n<PRE>");
   405 
   406 (*Convert .thy file to HTML and make chart of its super-theories*)
   407 fun thyfile2html tpath tname =
   408   let
   409     val gif_path = relative_path tpath (!gif_path);
   410 
   411     (*Determine name of current logic; if index_path is no subdirectory of
   412       base_path then we take the last directory of index_path*)
   413     val package =
   414       if (!index_path) = "" then
   415         error "index_path is empty. Please use 'init_html()' instead of \
   416               \'make_html := true'"
   417       else if (!index_path) subdir_of (!base_path) then
   418         relative_path (!base_path) (!index_path)
   419       else last_path (!index_path);
   420     val rel_index_path = relative_path tpath (!index_path);
   421 
   422     (*Make list of all theories and all theories that own a .thy file*)
   423     fun list_theories [] theories thy_files = (theories, thy_files)
   424       | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)
   425                       theories thy_files =
   426           list_theories ts (tname :: theories)
   427             (if is_some thy_time andalso the thy_time <> "" then
   428                tname :: thy_files
   429              else thy_files);
   430 
   431     val (theories, thy_files) =
   432       list_theories (Symtab.dest (!loaded_thys)) [] [];
   433 
   434     (*Do the conversion*)
   435     fun gettext thy_file  =
   436       let
   437         (*Convert special HTML characters ('&', '>', and '<')*)
   438         val file =
   439           explode (execute ("sed -e 's/\\&/\\&amp;/g' -e 's/>/\\&gt;/g' \
   440                             \-e 's/</\\&lt;/g' " ^ thy_file));
   441 
   442         (*Isolate first (possibly nested) comment;
   443           skip all leading whitespaces*)
   444         val (comment, file') =
   445           let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs)
   446                 | first_comment ("*" :: ")" :: cs) co d =
   447                     first_comment cs (co ^ "*)") (d-1)
   448                 | first_comment ("(" :: "*" :: cs) co d =
   449                     first_comment cs (co ^ "(*") (d+1)
   450                 | first_comment (" "  :: cs) "" 0 = first_comment cs "" 0
   451                 | first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0
   452                 | first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0
   453                 | first_comment cs           "" 0 = ("", cs)
   454                 | first_comment (c :: cs) co d =
   455                     first_comment cs (co ^ implode [c]) d
   456                 | first_comment [] co _ =
   457                     error ("Unexpected end of file " ^ tname ^ ".thy.");
   458           in first_comment file "" 0 end;
   459 
   460         (*Process line defining theory's ancestors;
   461           convert valid theory names to links to their HTML file*)
   462         val (ancestors, body) =
   463           let
   464             fun make_links l result =
   465               let val (pre, letter) = take_prefix (not o is_letter) l;
   466 
   467                   val (id, rest) =
   468                     take_prefix (is_quasi_letter orf is_digit) letter;
   469 
   470                   val id = implode id;
   471 
   472                   (*Make a HTML link out of a theory name*)
   473                   fun make_link t =
   474                     let val path = path_of t;
   475                     in "<A HREF = \"" ^
   476                        tack_on (relative_path tpath path) ("." ^ t) ^
   477                        ".html\">" ^ t ^ "</A>" end;
   478               in if not (id mem theories) then (result, implode l)
   479                  else if id mem thy_files then
   480                    make_links rest (result ^ implode pre ^ make_link id)
   481                  else make_links rest (result ^ implode pre ^ id)
   482               end;
   483 
   484             val (pre, rest) = take_prefix (fn c => c <> "=") file';
   485 
   486             val (ancestors, body) =
   487               if null rest then
   488                 error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\
   489                        \(Make sure that the last line ends with a linebreak.)")
   490               else
   491                 make_links rest "";
   492           in (implode pre ^ ancestors, body) end;
   493       in "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^
   494          "<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^
   495          tack_on rel_index_path "index.html\
   496          \\">Back</A> to the index of " ^ package ^
   497          "\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^
   498          "</PRE>\n"
   499       end;
   500 
   501     (** Make chart of super-theories **)
   502 
   503     val sup_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sup.html"));
   504     val sub_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sub.html"));
   505 
   506     (*Theories that already have been listed in this chart*)
   507     val listed = ref [];
   508 
   509     val wanted_theories =
   510       filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure")
   511              theories;
   512 
   513     (*Make tree of theory dependencies*)
   514     fun list_ancestors tname level continued =
   515       let
   516         fun mk_entry [] = ()
   517           | mk_entry (t::ts) =
   518             let
   519               val is_pure = t = "Pure" orelse t = "CPure";
   520               val path = if is_pure then (the (!pure_subchart))
   521                          else path_of t;
   522               val rel_path = relative_path tpath path;
   523               val repeated = t mem (!listed) andalso
   524                              not (null (parents_of_name t));
   525 
   526               fun mk_offset [] cur =
   527                     if level < cur then error "Error in mk_offset"
   528                     else implode (replicate (level - cur) "    ")
   529                 | mk_offset (l::ls) cur =
   530                     implode (replicate (l - cur) "    ") ^ "|   " ^
   531                     mk_offset ls (l+1);
   532             in TextIO.output (sup_out,
   533                  " " ^ mk_offset continued 0 ^
   534                  "\\__" ^ (if is_pure then t else
   535                              "<A HREF=\"" ^ tack_on rel_path ("." ^ t) ^
   536                              ".html\">" ^ t ^ "</A>") ^
   537                  (if repeated then "..." else " ") ^
   538                  "<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^
   539                  "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   540                  tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^
   541                  (if is_pure then ""
   542                   else "<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^
   543                        "_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   544                        tack_on gif_path "blue_arrow.gif\
   545                        \\" ALT = /\\></A>") ^
   546                  "\n");
   547               if repeated then ()
   548               else (listed := t :: (!listed);
   549                     list_ancestors t (level+1) (if null ts then continued
   550                                                 else continued @ [level]);
   551                     mk_entry ts)
   552             end;
   553 
   554         val relatives =
   555           filter (fn s => s mem wanted_theories) (parents_of_name tname);
   556       in mk_entry relatives end;
   557   in if is_some (!cur_htmlfile) then
   558        (TextIO.closeOut (the (!cur_htmlfile));
   559         warning "Last theory's HTML file has not been closed.")
   560      else ();
   561      cur_htmlfile := Some (TextIO.openOut (tack_on tpath ("." ^ tname ^ ".html")));
   562      cur_has_title := false;
   563      TextIO.output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
   564 
   565      mk_charthead sup_out tname "Ancestors" true gif_path rel_index_path
   566                   package;
   567      TextIO.output(sup_out,
   568        "<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \
   569        \<A HREF = \"." ^ tname ^
   570        "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   571        tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n");
   572      list_ancestors tname 0 [];
   573      TextIO.output (sup_out, "</PRE><HR></BODY></HTML>");
   574      TextIO.closeOut sup_out;
   575 
   576      mk_charthead sub_out tname "Children" false gif_path rel_index_path
   577                   package;
   578      TextIO.output(sub_out,
   579        "<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \
   580        \<A HREF = \"." ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
   581        tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n");
   582      TextIO.closeOut sub_out
   583   end;
   584 
   585 (*Invoke every put method stored in a theory's methods table to initialize
   586   the state of user defined variables*)
   587 fun put_thydata first tname =
   588   let val (methods, data) = 
   589         case get_thyinfo tname of
   590             Some (ThyInfo {methods, data, ...}) => 
   591               (methods, Symtab.dest ((if first then fst else snd) data))
   592           | None => error ("Theory " ^ tname ^ " not stored by loader");
   593 
   594       fun put_data (id, date) =
   595             case Symtab.lookup (methods, id) of
   596                 Some (ThyMethods {put, ...}) => put date
   597               | None => error ("No method defined for theory data \"" ^
   598                                id ^ "\"");
   599   in seq put_data data end;
   600 
   601 val set_current_thy = put_thydata false;
   602 
   603 (*Read .thy and .ML files that haven't been read yet or have changed since
   604   they were last read;
   605   loaded_thys is a thy_info list ref containing all theories that have
   606   completly been read by this and preceeding use_thy calls.
   607   tmp_loadpath is temporarily added to loadpath while the ancestors of a
   608   theory that the user specified as e.g. "ex/Nat" are loaded. Because of
   609   raised exceptions we cannot guarantee that it's value is always valid.
   610   Therefore this has to be assured by the first parameter of use_thy1 which
   611   is "true" if use_thy gets invoked by mk_base and "false" else.
   612 *)
   613 fun use_thy1 tmp_loadpath_valid name =
   614   let
   615     val (path, tname) = split_filename name;
   616     val dummy = (tmp_loadpath :=
   617       (if not tmp_loadpath_valid then (if path = "" then [] else [path])
   618        else !tmp_loadpath));
   619     val (thy_file, ml_file) = get_filenames path tname;
   620     val (abs_path, _) = if thy_file = "" then split_filename ml_file
   621                         else split_filename thy_file;
   622     val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file;
   623     val old_parents = parents_of_name tname;
   624 
   625     (*Set absolute path for loaded theory *)
   626     fun set_path () =
   627       let val ThyInfo {children, parents, thy_time, ml_time, theory, thms,
   628                        methods, data, ...} =
   629             the (Symtab.lookup (!loaded_thys, tname));
   630       in loaded_thys := Symtab.update ((tname,
   631                           ThyInfo {path = abs_path,
   632                                    children = children, parents = parents,
   633                                    thy_time = thy_time, ml_time = ml_time,
   634                                    theory = theory, thms = thms,
   635                                    methods = methods, data = data}),
   636                           !loaded_thys)
   637       end;
   638 
   639     (*Mark all direct descendants of a theory as changed *)
   640     fun mark_children thy =
   641       let val children = children_of thy;
   642           val present = filter (is_some o get_thyinfo) children;
   643           val loaded = filter already_loaded present;
   644       in if loaded <> [] then
   645            writeln ("The following children of theory " ^ (quote thy)
   646                     ^ " are now out-of-date: "
   647                     ^ (quote (space_implode "\",\"" loaded)))
   648          else ();
   649          seq mark_outdated present
   650       end;
   651 
   652     (*Invoke every get method stored in the methods table and store result in
   653       data table*)
   654     fun save_data thy_only =
   655       let val ThyInfo {path, children, parents, thy_time, ml_time,
   656                        theory, thms, methods, data} = the (get_thyinfo tname);
   657 
   658           fun get_data [] data = data
   659             | get_data ((id, ThyMethods {get, ...}) :: ms) data =
   660                 get_data ms (Symtab.update ((id, get ()), data));
   661 
   662           val new_data = get_data (Symtab.dest methods) Symtab.null;
   663 
   664           val data' = if thy_only then (new_data, snd data)
   665                       else (fst data, new_data);
   666       in loaded_thys := Symtab.update
   667            ((tname, ThyInfo {path = path,
   668                              children = children, parents = parents,
   669                              thy_time = thy_time, ml_time = ml_time,
   670                              theory = theory, thms = thms,
   671                              methods = methods, data = data'}),
   672             !loaded_thys)
   673       end;
   674 
   675     (*Add theory to file listing all loaded theories (for index.html)
   676       and to the sub-charts of its parents*)
   677     local exception MK_HTML in
   678     fun mk_html () =
   679       let val new_parents = parents_of_name tname \\ old_parents;
   680 
   681           fun robust_seq (proc: 'a -> unit) : 'a list -> unit =
   682             let fun seqf [] = ()
   683                   | seqf (x :: xs) = (proc x  handle _ => (); seqf xs)
   684             in seqf end;
   685 
   686           (*Add child to parents' sub-theory charts*)
   687           fun add_to_parents t =
   688             let val path = if t = "Pure" orelse t = "CPure" then
   689                              (the (!pure_subchart))
   690                            else path_of t;
   691  
   692                 val gif_path = relative_path path (!gif_path);
   693                 val rel_path = relative_path path abs_path;
   694                 val tpath = tack_on rel_path ("." ^ tname);
   695 
   696                 val fname = tack_on path ("." ^ t ^ "_sub.html");
   697                 val out = if file_exists fname then
   698                             TextIO.openAppend fname  handle e  =>
   699                               (warning ("Unable to write to file " ^
   700                                         fname); raise e)
   701                           else raise MK_HTML;
   702             in TextIO.output (out,
   703                  " |\n \\__<A HREF=\"" ^
   704                  tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^
   705                  "</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\
   706                  \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   707                  tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\
   708                  \<A HREF = \"" ^ tpath ^ "_sup.html\">\
   709                  \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   710                  tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n");
   711                TextIO.closeOut out
   712             end;
   713  
   714           val theory_list =
   715             TextIO.openAppend (tack_on (!index_path) ".theory_list.txt")
   716               handle _ => (make_html := false;
   717                            writeln ("Warning: Cannot write to " ^
   718                                   (!index_path) ^ " while making HTML files.\n\
   719                                   \HTML generation has been switched off.\n\
   720                                   \Call init_html() from within a \
   721                                   \writeable directory to reactivate it.");
   722                            raise MK_HTML)
   723       in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n");
   724          TextIO.closeOut theory_list;
   725  
   726          robust_seq add_to_parents new_parents
   727       end
   728       end;
   729 
   730     (*Make sure that loaded_thys contains an entry for tname*)
   731     fun init_thyinfo () =
   732     let val tinfo = ThyInfo {path = "", children = [], parents = [],
   733                              thy_time = None, ml_time = None,
   734                              theory = None, thms = Symtab.null,
   735                              methods = Symtab.null,
   736                              data = (Symtab.null, Symtab.null)};
   737     in if is_some (get_thyinfo tname) then ()
   738        else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
   739     end;
   740   in if thy_uptodate andalso ml_uptodate then ()
   741      else
   742       (if thy_file = "" then ()
   743        else if thy_uptodate then put_thydata true tname
   744        else
   745          (writeln ("Reading \"" ^ name ^ ".thy\"");
   746 
   747           init_thyinfo ();
   748           delete_thms tname;
   749           read_thy tname thy_file;
   750           SymbolInput.use (out_name tname);
   751           save_data true;
   752 
   753           (*Store axioms of theory
   754             (but only if it's not a copy of an older theory)*)
   755           let val parents = parents_of_name tname;
   756               val this_thy = theory_of tname;
   757               val axioms =
   758                 if length parents = 1
   759                    andalso Sign.eq_sg (sign_of (theory_of (hd parents)),
   760                                        sign_of this_thy) then []
   761                 else axioms_of this_thy;
   762           in map store_thm_db axioms end;
   763 
   764           if not (!delete_tmpfiles) then ()
   765           else OS.FileSys.remove (out_name tname);
   766 
   767           if not (!make_html) then ()
   768           else thyfile2html abs_path tname
   769          );
   770        
   771        set_info tname (Some (file_info thy_file)) None;
   772                                        (*mark thy_file as successfully loaded*)
   773 
   774        if ml_file = "" then ()
   775        else (writeln ("Reading \"" ^ name ^ ".ML\"");
   776              SymbolInput.use ml_file);
   777        save_data false;
   778 
   779        (*Store theory again because it could have been redefined*)
   780        use_string
   781          ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
   782 
   783        (*Add theory to list of all loaded theories (for index.html)
   784          and add it to its parents' sub-charts*)
   785        if !make_html then
   786          let val path = path_of tname;
   787          in if path = "" then               (*first time theory has been read*)
   788               (mk_html()  handle MK_HTML => ())
   789             else ()
   790          end
   791        else ();
   792 
   793        (*Now set the correct info*)
   794        set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
   795        set_path ();
   796 
   797        (*Mark theories that have to be reloaded*)
   798        mark_children tname;
   799 
   800        (*Close HTML file*)
   801        case !cur_htmlfile of
   802            Some out => (TextIO.output (out, "<HR></BODY></HTML>\n");
   803                         TextIO.closeOut out;
   804                         cur_htmlfile := None)
   805          | None => ()
   806       )
   807   end;
   808 
   809 val use_thy = use_thy1 false;
   810 
   811 fun time_use_thy tname = timeit(fn()=>
   812    (writeln("\n**** Starting Theory " ^ tname ^ " ****");
   813     use_thy tname;
   814     writeln("\n**** Finished Theory " ^ tname ^ " ****"))
   815    );
   816 
   817 (*Load all thy or ML files that have been changed and also
   818   all theories that depend on them.*)
   819 fun update () =
   820   let (*List theories in the order they have to be loaded in.*)
   821       fun load_order [] result = result
   822         | load_order thys result =
   823             let fun next_level [] = []
   824                   | next_level (t :: ts) =
   825                       let val children = children_of t
   826                       in children union (next_level ts) end;
   827 
   828                 val descendants = next_level thys;
   829             in load_order descendants ((result \\ descendants) @ descendants)
   830             end;
   831 
   832       fun reload_changed (t :: ts) =
   833             let val abspath = case get_thyinfo t of
   834                                   Some (ThyInfo {path, ...}) => path
   835                                 | None => "";
   836 
   837                 val (thy_file, ml_file) = get_filenames abspath t;
   838                 val (thy_uptodate, ml_uptodate) =
   839                         thy_unchanged t thy_file ml_file;
   840             in if thy_uptodate andalso ml_uptodate then ()
   841                                                    else use_thy t;
   842                reload_changed ts
   843             end
   844         | reload_changed [] = ();
   845 
   846      (*Remove all theories that are no descendants of ProtoPure.
   847        If there are still children in the deleted theory's list
   848        schedule them for reloading *)
   849      fun collect_garbage no_garbage =
   850        let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
   851                  if tname mem no_garbage then collect ts
   852                  else (writeln ("Theory \"" ^ tname ^
   853                        "\" is no longer linked with ProtoPure - removing it.");
   854                        remove_thy tname;
   855                        seq mark_outdated children)
   856              | collect [] = ()
   857        in collect (Symtab.dest (!loaded_thys)) end;
   858   in tmp_loadpath := [];
   859      collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
   860      reload_changed (load_order ["Pure", "CPure"] [])
   861   end;
   862 
   863 (*Merge theories to build a base for a new theory.
   864   Base members are only loaded if they are missing.*)
   865 fun mk_base bases child mk_draft =
   866   let (*Show the cycle that would be created by add_child*)
   867       fun show_cycle base =
   868         let fun find_it result curr =
   869               let val tinfo = get_thyinfo curr
   870               in if base = curr then
   871                    error ("Cyclic dependency of theories: "
   872                           ^ child ^ "->" ^ base ^ result)
   873                  else if is_some tinfo then
   874                    let val ThyInfo {children, ...} = the tinfo
   875                    in seq (find_it ("->" ^ curr ^ result)) children
   876                    end
   877                  else ()
   878               end
   879         in find_it "" child end;
   880 
   881       (*Check if a cycle would be created by add_child*)
   882       fun find_cycle base =
   883         if base mem (get_descendants [child]) then show_cycle base
   884         else ();
   885 
   886       (*Add child to child list of base*)
   887       fun add_child base =
   888         let val tinfo =
   889               case Symtab.lookup (!loaded_thys, base) of
   890                   Some (ThyInfo {path, children, parents, thy_time, ml_time,
   891                            theory, thms, methods, data}) =>
   892                     ThyInfo {path = path,
   893                              children = child ins children, parents = parents,
   894                              thy_time = thy_time, ml_time = ml_time,
   895                              theory = theory, thms = thms,
   896                              methods = methods, data = data}
   897                 | None => ThyInfo {path = "", children = [child], parents = [],
   898                                    thy_time = None, ml_time = None,
   899                                    theory = None, thms = Symtab.null,
   900                                    methods = Symtab.null,
   901                                    data = (Symtab.null, Symtab.null)};
   902         in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
   903 
   904       (*Load a base theory if not already done
   905         and no cycle would be created *)
   906       fun load base =
   907           let val thy_loaded = already_loaded base
   908                                        (*test this before child is added *)
   909           in
   910             if child = base then
   911                 error ("Cyclic dependency of theories: " ^ child
   912                        ^ "->" ^ child)
   913             else
   914               (find_cycle base;
   915                add_child base;
   916                if thy_loaded then ()
   917                else (writeln ("Autoloading theory " ^ (quote base)
   918                               ^ " (used by " ^ (quote child) ^ ")");
   919                      use_thy1 true base)
   920               )
   921           end;
   922 
   923       (*Load all needed files and make a list of all real theories *)
   924       fun load_base (Thy b :: bs) =
   925            (load b;
   926             b :: load_base bs)
   927         | load_base (File b :: bs) =
   928            (load b;
   929             load_base bs)                    (*don't add it to mergelist *)
   930         | load_base [] = [];
   931 
   932       val dummy = unlink_thy child;
   933       val mergelist = load_base bases;
   934 
   935       val base_thy = (writeln ("Loading theory " ^ (quote child));
   936                       merge_thy_list mk_draft (map theory_of mergelist));
   937 
   938       val datas =
   939         let fun get_data t =
   940               let val ThyInfo {data, ...} = the (get_thyinfo t)
   941               in snd data end;
   942         in map (Symtab.dest o get_data) mergelist end;
   943 
   944       val methods =
   945         let fun get_methods t =
   946               let val ThyInfo {methods, ...} = the (get_thyinfo t)
   947               in methods end;
   948 
   949             val ms = map get_methods mergelist;
   950         in if null ms then Symtab.null
   951            else foldl (Symtab.merge (fn (x,y) => true)) (hd ms, tl ms)
   952         end;
   953 
   954       (*merge two sorted association lists*)
   955       fun merge_two ([], d2) = d2
   956         | merge_two (d1, []) = d1
   957         | merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s),
   958                      l2 as ((p2 as (id2, d2)) :: d2s)) =
   959             if id1 < id2 then
   960               p1 :: merge_two (d1s, l2)
   961             else
   962               p2 :: merge_two (l1, d2s);
   963 
   964       (*Merge multiple occurence of data; also call put for each merged list*)
   965       fun merge_multi [] None = []
   966         | merge_multi [] (Some (id, ds)) =
   967             let val ThyMethods {merge, put, ...} =
   968                   the (Symtab.lookup (methods, id));
   969              in put (merge ds); [id] end
   970         | merge_multi ((id, d) :: ds) None = merge_multi ds (Some (id, [d]))
   971         | merge_multi ((id, d) :: ds) (Some (id2, d2s)) =
   972             if id = id2 then
   973               merge_multi ds (Some (id2, d :: d2s))
   974             else
   975               let val ThyMethods {merge, put, ...} =
   976                     the (Symtab.lookup (methods, id2));
   977               in put (merge d2s);
   978                  id2 :: merge_multi ds (Some (id, [d]))
   979               end;
   980 
   981       val merged =
   982         if null datas then []
   983         else merge_multi (foldl merge_two (hd datas, tl datas)) None;
   984 
   985       val dummy =
   986         let val unmerged = map fst (Symtab.dest methods) \\ merged;
   987 
   988             fun put_empty id =
   989               let val ThyMethods {merge, put, ...} =
   990                     the (Symtab.lookup (methods, id));
   991               in put (merge []) end;
   992         in seq put_empty unmerged end;
   993 
   994       val dummy =
   995         let val tinfo = case Symtab.lookup (!loaded_thys, child) of
   996               Some (ThyInfo {path, children, thy_time, ml_time, theory, thms,
   997                              data, ...}) =>
   998                  ThyInfo {path = path,
   999                           children = children, parents = mergelist,
  1000                           thy_time = thy_time, ml_time = ml_time,
  1001                           theory = theory, thms = thms,
  1002                           methods = methods, data = data}
  1003              | None => error ("set_parents: theory " ^ child ^ " not found");
  1004         in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end;
  1005 
  1006  in cur_thyname := child;
  1007     base_thy
  1008  end;
  1009 
  1010 (*Change theory object for an existent item of loaded_thys*)
  1011 fun store_theory (thy, tname) =
  1012   let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
  1013                Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,
  1014                               methods, data, ...}) =>
  1015                  ThyInfo {path = path, children = children, parents = parents,
  1016                           thy_time = thy_time, ml_time = ml_time,
  1017                           theory = Some thy, thms = thms,
  1018                           methods = methods, data = data}
  1019              | None => error ("store_theory: theory " ^ tname ^ " not found");
  1020   in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
  1021 
  1022 
  1023 (*** Store and retrieve theorems ***)
  1024 (*Guess the name of a theory object
  1025   (First the quick way by looking at the stamps; if that doesn't work,
  1026    we search loaded_thys for the first theory which fits.)
  1027 *)
  1028 fun thyname_of_sign sg =
  1029   let val ref xname = hd (#stamps (Sign.rep_sg sg));
  1030       val opt_info = get_thyinfo xname;
  1031 
  1032     fun eq_sg (ThyInfo {theory = None, ...}) = false
  1033       | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);
  1034 
  1035     val show_sg = Pretty.str_of o Sign.pretty_sg;
  1036   in
  1037     if is_some opt_info andalso eq_sg (the opt_info) then xname
  1038     else
  1039       (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of
  1040         Some (name, _) => name
  1041       | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))
  1042   end;
  1043 
  1044 (*Guess to which theory a signature belongs and return it's thy_info*)
  1045 fun thyinfo_of_sign sg =
  1046   let val name = thyname_of_sign sg;
  1047   in (name, the (get_thyinfo name)) end;
  1048 
  1049 
  1050 (*Try to get the theory object corresponding to a given signature*)
  1051 fun theory_of_sign sg =
  1052   (case thyinfo_of_sign sg of
  1053     (_, ThyInfo {theory = Some thy, ...}) => thy
  1054   | _ => sys_error "theory_of_sign");
  1055 
  1056 (*Try to get the theory object corresponding to a given theorem*)
  1057 val theory_of_thm = theory_of_sign o #sign o rep_thm;
  1058 
  1059 
  1060 (** Store theorems **)
  1061 
  1062 (*Makes HTML title for list of theorems; as this list may be empty and we
  1063   don't want a title in that case, mk_theorems_title is only invoked when
  1064   something is added to the list*)
  1065 fun mk_theorems_title out =
  1066   if not (!cur_has_title) then
  1067     (cur_has_title := true;
  1068      TextIO.output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^
  1069                   (!cur_thyname) ^ ".ML\">" ^ (!cur_thyname) ^
  1070                   ".ML</A>:</H2>\n"))
  1071   else ();
  1072 
  1073 (*Store a theorem in the thy_info of its theory,
  1074   and in the theory's HTML file*)
  1075 fun store_thm (name, thm) =
  1076   let
  1077     val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time,
  1078                             theory, thms, methods, data}) =
  1079       thyinfo_of_sign (#sign (rep_thm thm))
  1080 
  1081     val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
  1082       handle Symtab.DUPLICATE s => 
  1083         (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
  1084            (warning ("Theory database already contains copy of\
  1085                      \ theorem " ^ quote name);
  1086             (thms, true))
  1087          else error ("Duplicate theorem name " ^ quote s
  1088                      ^ " used in theory database"));
  1089 
  1090     fun thm_to_html () =
  1091       let fun escape []       = ""
  1092             | escape ("<"::s) = "&lt;" ^ escape s
  1093             | escape (">"::s) = "&gt;" ^ escape s
  1094             | escape ("&"::s) = "&amp;" ^ escape s
  1095             | escape (c::s)   = c ^ escape s;
  1096       in case !cur_htmlfile of
  1097              Some out =>
  1098                (mk_theorems_title out;
  1099                 TextIO.output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
  1100                              escape 
  1101                               (explode 
  1102                                (string_of_thm (#1 (freeze_thaw thm)))) ^
  1103                              "</PRE><P>\n")
  1104                )
  1105            | None => ()
  1106       end;
  1107 
  1108     (*Label this theorem*)
  1109     val thm' = Thm.name_thm (name, thm)
  1110   in
  1111     loaded_thys := Symtab.update
  1112      ((thy_name, ThyInfo {path = path, children = children, parents = parents,
  1113                           thy_time = thy_time, ml_time = ml_time,
  1114                           theory = theory, thms = thms',
  1115                           methods = methods, data = data}),
  1116       !loaded_thys);
  1117     thm_to_html ();
  1118     if duplicate then thm' else store_thm_db (name, thm')
  1119   end;
  1120 
  1121 (*Store result of proof in loaded_thys and as ML value*)
  1122 
  1123 val qed_thm = ref flexpair_def(*dummy*);
  1124 
  1125 fun bind_thm (name, thm) =
  1126  (qed_thm := store_thm (name, (standard thm));
  1127   use_string ["val " ^ name ^ " = !qed_thm;"]);
  1128 
  1129 fun qed name =
  1130  (qed_thm := store_thm (name, result ());
  1131   use_string ["val " ^ name ^ " = !qed_thm;"]);
  1132 
  1133 fun qed_goal name thy agoal tacsf =
  1134  (qed_thm := store_thm (name, prove_goal thy agoal tacsf);
  1135   use_string ["val " ^ name ^ " = !qed_thm;"]);
  1136 
  1137 fun qed_goalw name thy rths agoal tacsf =
  1138  (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf);
  1139   use_string ["val " ^ name ^ " = !qed_thm;"]);
  1140 
  1141 
  1142 (** Retrieve theorems **)
  1143 
  1144 (*Get all theorems belonging to a given theory*)
  1145 fun thmtab_of_thy thy =
  1146   let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
  1147   in thms end;
  1148 
  1149 fun thmtab_of_name name =
  1150   let val ThyInfo {thms, ...} = the (get_thyinfo name);
  1151   in thms end;
  1152 
  1153 (*Get a stored theorem specified by theory and name. *)
  1154 fun get_thm thy name =
  1155   let fun get [] [] searched =
  1156            raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
  1157         | get [] ng searched =
  1158             get (ng \\ searched) [] searched
  1159         | get (t::ts) ng searched =
  1160             (case Symtab.lookup (thmtab_of_name t, name) of
  1161                  Some thm => thm
  1162                | None => get ts (ng union (parents_of_name t)) (t::searched));
  1163 
  1164       val (tname, _) = thyinfo_of_sign (sign_of thy);
  1165   in get [tname] [] [] end;
  1166 
  1167 (*Get stored theorems of a theory (original derivations) *)
  1168 val thms_of = Symtab.dest o thmtab_of_thy;
  1169 
  1170 
  1171 
  1172 
  1173 (*** Misc HTML functions ***)
  1174 
  1175 (*Init HTML generator by setting paths and creating new files*)
  1176 fun init_html () =
  1177   let val cwd = OS.FileSys.getDir();
  1178 
  1179       val theory_list = TextIO.closeOut (TextIO.openOut ".theory_list.txt");
  1180 
  1181       val rel_gif_path = relative_path cwd (!gif_path);
  1182 
  1183       (*Make new HTML files for Pure and CPure*)
  1184       fun init_pure_html () =
  1185         let val pure_out = TextIO.openOut ".Pure_sub.html";
  1186             val cpure_out = TextIO.openOut ".CPure_sub.html";
  1187             val package =
  1188               if cwd subdir_of (!base_path) then
  1189                 relative_path (!base_path) cwd
  1190               else last_path cwd;
  1191         in mk_charthead pure_out "Pure" "Children" false rel_gif_path ""
  1192                         package;
  1193            mk_charthead cpure_out "CPure" "Children" false rel_gif_path ""
  1194                         package;
  1195            TextIO.output (pure_out, "Pure\n");
  1196            TextIO.output (cpure_out, "CPure\n");
  1197            TextIO.closeOut pure_out;
  1198            TextIO.closeOut cpure_out;
  1199            pure_subchart := Some cwd
  1200         end;
  1201   in make_html := true;
  1202      index_path := cwd;
  1203 
  1204      (*Make sure that base_path contains the physical path and no
  1205        symbolic links*)
  1206      OS.FileSys.chDir (!base_path);
  1207      base_path := OS.FileSys.getDir();
  1208      OS.FileSys.chDir cwd;
  1209 
  1210      if cwd subdir_of (!base_path) then ()
  1211      else warning "The current working directory seems to be no \
  1212                   \subdirectory of\nIsabelle's main directory. \
  1213                   \Please ensure that base_path's value is correct.\n";
  1214 
  1215      writeln ("Setting path for index.html to " ^ quote cwd ^
  1216               "\nGIF path has been set to " ^ quote (!gif_path));
  1217 
  1218      if is_none (!pure_subchart) then init_pure_html()
  1219      else ()
  1220   end;
  1221 
  1222 (*Generate index.html*)
  1223 fun finish_html () = if not (!make_html) then () else
  1224   let val tlist_path = tack_on (!index_path) ".theory_list.txt";
  1225       val theory_list = TextIO.openIn tlist_path;
  1226       val theories = space_explode "\n" (TextIO.inputAll theory_list);
  1227       val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path);
  1228 
  1229       val gif_path = relative_path (!index_path) (!gif_path);
  1230 
  1231       (*Make entry for main chart of all theories.*)
  1232       fun main_entry t =
  1233         let
  1234           val (name, path) = take_prefix (not_equal " ") (explode t);
  1235 
  1236           val tname = implode name
  1237           val tpath = tack_on (relative_path (!index_path) (implode (tl path)))
  1238                               ("." ^ tname);
  1239         in "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^
  1240            tack_on gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^
  1241            "<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^
  1242            tack_on gif_path "blue_arrow.gif\
  1243            \\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^
  1244            ".html\">" ^ tname ^ "</A><BR>\n"
  1245         end;
  1246 
  1247       val out = TextIO.openOut (tack_on (!index_path) "index.html");
  1248 
  1249       (*Find out in which subdirectory of Isabelle's main directory the
  1250         index.html is placed; if index_path is no subdirectory of base_path
  1251         then take the last directory of index_path*)
  1252       val inside_isabelle = (!index_path) subdir_of (!base_path);
  1253       val subdir =
  1254         if inside_isabelle then relative_path (!base_path) (!index_path)
  1255         else last_path (!index_path);
  1256       val subdirs = space_explode "/" subdir;
  1257 
  1258       (*Look for index.html in superdirectories; stop when Isabelle's
  1259         main directory is reached*)
  1260       fun find_super_index [] n = ("", n)
  1261         | find_super_index (p::ps) n =
  1262           let val index_path = "/" ^ space_implode "/" (rev ps);
  1263           in if file_exists (index_path ^ "/index.html") then (index_path, n)
  1264              else if length subdirs - n >= 0 then find_super_index ps (n+1)
  1265              else ("", n)
  1266           end;
  1267       val (super_index, level_diff) =
  1268         find_super_index (rev (space_explode "/" (!index_path))) 1;
  1269       val level = length subdirs - level_diff;
  1270 
  1271       (*Add link to current directory to 'super' index.html*)
  1272       fun link_directory () =
  1273         let val old_index = TextIO.openIn (super_index ^ "/index.html");
  1274             val content = rev (explode (TextIO.inputAll old_index));
  1275             val dummy = TextIO.closeIn old_index;
  1276 
  1277             val out = TextIO.openAppend (super_index ^ "/index.html");
  1278             val rel_path = space_implode "/" (drop (level, subdirs));
  1279         in 
  1280            TextIO.output (out,
  1281              (if nth_elem (3, content) <> "!" then ""
  1282               else "\n<HR><H3>Subdirectories:</H3>\n") ^
  1283              "<H3><A HREF = \"" ^ rel_path ^ "/index.html\">" ^ rel_path ^
  1284              "</A></H3>\n");
  1285            TextIO.closeOut out
  1286         end;
  1287 
  1288      (*If index_path is no subdirectory of base_path then the title should
  1289        not contain the string "Isabelle/"*)
  1290      val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir;
  1291   in TextIO.output (out,
  1292        "<HTML><HEAD><TITLE>" ^ title ^ "</TITLE></HEAD>\n\
  1293        \<BODY><H2>" ^ title ^ "</H2>\n\
  1294        \The name of every theory is linked to its theory file<BR>\n\
  1295        \<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
  1296        \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
  1297        \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
  1298        \\" ALT = /\\></A> stands for supertheories (parent theories)" ^
  1299        (if super_index = "" then "" else
  1300         ("<P>\n<A HREF = \"" ^ relative_path (!index_path) super_index ^ 
  1301          "/index.html\">Back</A> to the index of " ^
  1302          (if not inside_isabelle then
  1303             hd (tl (rev (space_explode "/" (!index_path))))
  1304           else if level = 0 then "Isabelle logics"
  1305           else space_implode "/" (take (level, subdirs))))) ^
  1306        "\n" ^
  1307        (if file_exists (tack_on (!index_path) "README.html") then
  1308           "<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n"
  1309         else if file_exists (tack_on (!index_path) "README") then
  1310           "<BR>View the <A HREF = \"README\">ReadMe</A> file.\n"
  1311         else "") ^
  1312        "<HR>" ^ implode (map main_entry theories) ^ "<!-->");
  1313      TextIO.closeOut out;
  1314      if super_index = "" orelse (inside_isabelle andalso level = 0) then ()
  1315         else link_directory ()
  1316   end;
  1317 
  1318 (*Append section heading to HTML file*)
  1319 fun section s =
  1320   case !cur_htmlfile of
  1321       Some out => (mk_theorems_title out;
  1322                    TextIO.output (out, "<H3>" ^ s ^ "</H3>\n"))
  1323     | None => ();
  1324 
  1325 
  1326 (*** Print theory ***)
  1327 
  1328 fun print_thms thy =
  1329   let
  1330     val thms = thms_of thy;
  1331     fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
  1332       Pretty.quote (pretty_thm th)];
  1333   in
  1334     Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
  1335   end;
  1336 
  1337 fun print_theory thy = (Display.print_theory thy; print_thms thy);
  1338 
  1339 
  1340 (*** Misc functions ***)
  1341 
  1342 (*Add data handling methods to theory*)
  1343 fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
  1344   let val ThyInfo {path, children, parents, thy_time, ml_time, theory,
  1345                    thms, methods, data} =
  1346         case get_thyinfo tname of
  1347             Some ti => ti
  1348           | None => error ("Theory " ^ tname ^ " not stored by loader");
  1349   in loaded_thys := Symtab.update ((tname, ThyInfo {path = path,
  1350        children = children, parents = parents, thy_time = thy_time,
  1351        ml_time = ml_time, theory = theory, thms = thms,
  1352        methods = Symtab.update (new_methods, methods), data = data}),
  1353        !loaded_thys)
  1354   end;
  1355 
  1356 (*Add file to thy_reader_files list*)
  1357 fun set_thy_reader_file file =
  1358   let val file' = absolute_path (OS.FileSys.getDir ()) file;
  1359   in thy_reader_files := file' :: (!thy_reader_files) end;
  1360 
  1361 (*Add file and also 'use' it*)
  1362 fun add_thy_reader_file file = (set_thy_reader_file file; use file);
  1363 
  1364 (*Read all files contained in thy_reader_files list*)
  1365 fun read_thy_reader_files () = seq use (!thy_reader_files);
  1366 
  1367 
  1368 (*Retrieve data associated with theory*)
  1369 fun get_thydata tname id =
  1370   let val d2 = case get_thyinfo tname of
  1371                    Some (ThyInfo {data, ...}) => snd data
  1372                  | None => error ("Theory " ^ tname ^ " not stored by loader");
  1373   in Symtab.lookup (d2, id) end;
  1374 
  1375 
  1376 (*Temporarily enter a directory and load its ROOT.ML file;
  1377   also do some work for HTML generation*)
  1378 local
  1379 
  1380   fun gen_use_dir use_cmd dirname =
  1381     let val old_dir = OS.FileSys.getDir ();
  1382     in OS.FileSys.chDir dirname;
  1383        if !make_html then init_html() else ();
  1384        use_cmd "ROOT.ML";
  1385        finish_html();
  1386        OS.FileSys.chDir old_dir
  1387     end;
  1388 
  1389 in
  1390 
  1391   val use_dir = gen_use_dir use;
  1392   val exit_use_dir = gen_use_dir exit_use;
  1393 
  1394 end
  1395 
  1396 end;