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