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