src/Pure/Thy/thy_read.ML
author clasohm
Thu, 26 Oct 1995 13:53:04 +0100
changeset 1313 9fb65f3db319
parent 1308 396ef8aa37b7
child 1317 83ce32aa4e9b
permissions -rw-r--r--
renamed chart00 and 00-chart to "index"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thy_read.ML
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
     3
    Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
     4
                Tobias Nipkow and L C Paulson
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
     5
    Copyright   1994 TU Muenchen
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     6
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
     7
Functions for reading theory files, and storing and retrieving theories,
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
     8
theorems and the global simplifier set.
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
     9
*)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    10
1157
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    11
(*Type for theory storage*)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    12
datatype thy_info =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    13
  ThyInfo of {path: string,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    14
              children: string list, parents: string list,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    15
              thy_time: string option, ml_time: string option,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    16
              theory: theory option, thms: thm Symtab.table,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    17
              thy_ss: Simplifier.simpset option,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    18
              simpset: Simplifier.simpset option};
1157
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    19
      (*meaning of special values:
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    20
        thy_time, ml_time = None     theory file has not been read yet
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    21
                          = Some ""  theory was read but has either been marked
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    22
                                     as outdated or there is no such file for
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    23
                                     this theory (see e.g. 'virtual' theories
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    24
                                     like Pure or theories without a ML file)
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    25
        theory = None  theory has not been read yet
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    26
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    27
        parents: While 'children' contains all theories the theory depends
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    28
                 on (i.e. also ones quoted in the .thy file),
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    29
                 'parents' only contains the theories which were used to form
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    30
                 the base of this theory.
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    31
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    32
        origin of the simpsets:
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    33
        thy_ss: snapshot of !Simpset.simpset after .thy file was read
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    34
        simpset: snapshot of !Simpset.simpset after .ML file was read
1157
da78c293e8dc added a few comments on ThyInfo
clasohm
parents: 1154
diff changeset
    35
       *)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    36
412
216624270b80 restored old functor name;
wenzelm
parents: 397
diff changeset
    37
signature READTHY =
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    38
sig
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    39
  datatype basetype = Thy  of string
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    40
                    | File of string
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    41
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
    42
  val loaded_thys    : thy_info Symtab.table ref
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    43
  val loadpath       : string list ref
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    44
  val delete_tmpfiles: bool ref
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    45
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    46
  val use_thy        : string -> unit
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    47
  val update         : unit -> unit
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    48
  val time_use_thy   : string -> unit
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    49
  val unlink_thy     : string -> unit
586
201e115d8031 renamed base_on into mk_base and moved it to the beginning of the generated
clasohm
parents: 559
diff changeset
    50
  val mk_base        : basetype list -> string -> bool -> theory
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
    51
  val store_theory   : theory * string -> unit
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
    52
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
    53
  val theory_of_sign: Sign.sg -> theory
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
    54
  val theory_of_thm: thm -> theory
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    55
  val children_of: string -> string list
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    56
  val parents_of: string -> string list
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    57
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
    58
  val store_thm: string * thm -> thm
758
c2b210bda710 added bind_thm
clasohm
parents: 746
diff changeset
    59
  val bind_thm: string * thm -> unit
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
    60
  val qed: string -> unit
758
c2b210bda710 added bind_thm
clasohm
parents: 746
diff changeset
    61
  val qed_thm: thm ref
746
6e815617d79f added qed_goal[w]
clasohm
parents: 715
diff changeset
    62
  val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
6e815617d79f added qed_goal[w]
clasohm
parents: 715
diff changeset
    63
  val qed_goalw: string -> theory->thm list->string->(thm list->tactic list)
6e815617d79f added qed_goal[w]
clasohm
parents: 715
diff changeset
    64
                 -> unit
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
    65
  val get_thm: theory -> string -> thm
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
    66
  val thms_of: theory -> (string * thm) list
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
    67
  val simpset_of: string -> Simplifier.simpset
778
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
    68
  val print_theory: theory -> unit
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    69
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    70
  val gif_path       : string ref
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
    71
  val index_path   : string ref
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    72
  val make_html      : bool ref
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    73
  val init_html: unit -> unit
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    74
  val make_chart: unit -> unit
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    75
end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    76
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    77
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
    78
functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    79
struct
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
    80
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
    81
open ThmDB Simplifier;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    82
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    83
datatype basetype = Thy  of string
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    84
                  | File of string;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
    85
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    86
val loaded_thys =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    87
  ref (Symtab.make [("ProtoPure",
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    88
                     ThyInfo {path = "",
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    89
                              children = ["Pure", "CPure"], parents = [],
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    90
                              thy_time = Some "", ml_time = Some "",
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    91
                              theory = Some proto_pure_thy, thms = Symtab.null,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    92
                              thy_ss = None, simpset = None}),
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    93
                    ("Pure",
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    94
                     ThyInfo {path = "", children = [],
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    95
                              parents = ["ProtoPure"],
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    96
                              thy_time = Some "", ml_time = Some "",
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    97
                              theory = Some pure_thy, thms = Symtab.null,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    98
                              thy_ss = None, simpset = None}),
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
    99
                    ("CPure",
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   100
                     ThyInfo {path = "",
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   101
                              children = [], parents = ["ProtoPure"],
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   102
                              thy_time = Some "", ml_time = Some "",
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   103
                              theory = Some cpure_thy,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   104
                              thms = Symtab.null,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   105
                              thy_ss = None, simpset = None})
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   106
                   ]);
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   107
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   108
val loadpath = ref ["."];              (*default search path for theory files*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   109
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   110
val delete_tmpfiles = ref true;            (*remove temporary files after use*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   111
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   112
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   113
(*Set location of graphics for HTML files
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   114
  (When this is executed for the first time we are in $ISABELLE/Pure/Thy.
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   115
   This path is converted to $ISABELLE/Tools by removing the last two
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   116
   directories and appending "Tools". All subsequently made ReadThy
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   117
   structures inherit this value.)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   118
*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   119
val gif_path = ref (tack_on ("/" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   120
  space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ())))))))
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   121
  "Tools");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   122
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   123
(*Location of theory-list.txt and index.html (normally set by init_html)*)
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   124
val index_path = ref "";     
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   125
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   126
val make_html = ref false;      (*don't make HTML versions of loaded theories*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   127
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   128
(*HTML file of theory currently being read
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   129
  (Initialized by thyfile2html; used by use_thy and store_thm)*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   130
val cur_htmlfile = ref None : outstream option ref;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   131
                                   
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   132
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   133
(*Make name of the output ML file for a theory *)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   134
fun out_name tname = "." ^ tname ^ ".thy.ML";
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   135
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   136
(*Read a file specified by thy_file containing theory thy *)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   137
fun read_thy tname thy_file =
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   138
  let
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   139
    val instream  = open_in thy_file;
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   140
    val outstream = open_out (out_name tname);
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   141
  in
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   142
    output (outstream, ThySyn.parse tname (input (instream, 999999)));
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   143
    close_out outstream;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   144
    close_in instream
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   145
  end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   146
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   147
fun file_exists file =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   148
  let val instream = open_in file in close_in instream; true end
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   149
    handle Io _ => false;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   150
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   151
(*Get thy_info for a loaded theory *)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   152
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   153
971
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   154
(*Check if a theory was completly loaded *)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   155
fun already_loaded thy =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   156
  let val t = get_thyinfo thy
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   157
  in if is_none t then false
971
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   158
     else let val ThyInfo {thy_time, ml_time, ...} = the t
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   159
          in is_some thy_time andalso is_some ml_time end
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   160
  end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   161
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   162
(*Check if a theory file has changed since its last use.
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   163
  Return a pair of boolean values for .thy and for .ML *)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   164
fun thy_unchanged thy thy_file ml_file =
1098
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   165
  case get_thyinfo thy of
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   166
      Some (ThyInfo {thy_time, ml_time, ...}) =>
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   167
       let val tn = is_none thy_time;
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   168
           val mn = is_none ml_time
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   169
       in if not tn andalso not mn then
1098
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   170
            ((file_info thy_file = the thy_time),
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   171
             (file_info ml_file = the ml_time))
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   172
          else if not tn andalso mn then
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   173
            (file_info thy_file = the thy_time, false)
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   174
          else
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   175
            (false, false)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   176
       end
1098
487089cb173e fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents: 971
diff changeset
   177
    | None => (false, false)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   178
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   179
(*Get all direct descendants of a theory*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   180
fun children_of t =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   181
  case get_thyinfo t of Some (ThyInfo {children, ...}) => children
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   182
                      | _ => [];
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   183
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   184
(*Get all direct ancestors of a theory*)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   185
fun parents_of t =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   186
  case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   187
                      | _ => [];
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   188
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   189
(*Get all descendants of a theory list *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   190
fun get_descendants [] = []
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   191
  | get_descendants (t :: ts) =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   192
      let val children = children_of t
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   193
      in children union (get_descendants (children union ts)) end;
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   194
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   195
(*Get theory object for a loaded theory *)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   196
fun theory_of name =
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   197
  let val ThyInfo {theory, ...} = the (get_thyinfo name)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   198
  in the theory end;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   199
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   200
(*Get path where theory's files are located*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   201
fun path_of tname =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   202
  let val ThyInfo {path, ...} = the (get_thyinfo tname)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   203
  in path end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   204
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   205
exception FILE_NOT_FOUND;   (*raised by find_file *)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   206
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   207
(*Find a file using a list of paths if no absolute or relative path is
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   208
  specified.*)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   209
fun find_file "" name =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   210
      let fun find_it (cur :: paths) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   211
                if file_exists (tack_on cur name) then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   212
                  (if cur = "." then name else tack_on cur name)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   213
                else
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   214
                  find_it paths
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   215
           | find_it [] = ""
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   216
      in find_it (!loadpath) end
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   217
  | find_file path name =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   218
      if file_exists (tack_on path name) then tack_on path name
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   219
                                         else "";
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   220
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   221
(*Get absolute pathnames for a new or already loaded theory *)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   222
fun get_filenames path name =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   223
  let fun make_absolute file =
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   224
        if file = "" then "" else
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   225
            if hd (explode file) = "/" then file else tack_on (pwd ()) file;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   226
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   227
      fun new_filename () =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   228
        let val found = find_file path (name ^ ".thy")
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   229
                        handle FILE_NOT_FOUND => "";
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   230
            val thy_file = make_absolute found;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   231
            val (thy_path, _) = split_filename thy_file;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   232
            val found = find_file path (name ^ ".ML");
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   233
            val ml_file = if thy_file = "" then make_absolute found
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   234
                          else if file_exists (tack_on thy_path (name ^ ".ML"))
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   235
                          then tack_on thy_path (name ^ ".ML")
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   236
                          else "";
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   237
            val searched_dirs = if path = "" then (!loadpath) else [path]
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   238
        in if thy_file = "" andalso ml_file = "" then
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   239
             error ("Could not find file \"" ^ name ^ ".thy\" or \""
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   240
                    ^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n"
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   241
                    ^ "in the following directories: \"" ^
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   242
                    (space_implode "\", \"" searched_dirs) ^ "\"")
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   243
           else ();
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   244
           (thy_file, ml_file)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   245
        end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   246
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   247
      val tinfo = get_thyinfo name;
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   248
  in if is_some tinfo andalso path = "" then
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   249
       let val ThyInfo {path = abs_path, ...} = the tinfo;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   250
           val (thy_file, ml_file) = if abs_path = "" then new_filename ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   251
                                     else (find_file abs_path (name ^ ".thy"),
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   252
                                           find_file abs_path (name ^ ".ML"))
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   253
       in if thy_file = "" andalso ml_file = "" then
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   254
            (writeln ("Warning: File \"" ^ (tack_on path name)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   255
                      ^ ".thy\"\ncontaining theory \"" ^ name
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   256
                      ^ "\" no longer exists.");
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   257
             new_filename ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   258
            )
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   259
          else (thy_file, ml_file)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   260
       end
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   261
     else new_filename ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   262
  end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   263
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   264
(*Remove theory from all child lists in loaded_thys *)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   265
fun unlink_thy tname =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   266
  let fun remove (ThyInfo {path, children, parents, thy_time, ml_time,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   267
                           theory, thms, thy_ss, simpset}) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   268
        ThyInfo {path = path, children = children \ tname, parents = parents,
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   269
                 thy_time = thy_time, ml_time = ml_time, theory = theory, 
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   270
                 thms = thms, thy_ss = thy_ss, simpset = simpset}
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   271
  in loaded_thys := Symtab.map remove (!loaded_thys) end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   272
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   273
(*Remove a theory from loaded_thys *)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   274
fun remove_thy tname =
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   275
  loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   276
                 (Symtab.dest (!loaded_thys)));
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   277
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   278
(*Change thy_time and ml_time for an existent item *)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   279
fun set_info tname thy_time ml_time =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   280
  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   281
          Some (ThyInfo {path, children, parents, theory, thms,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   282
                         thy_ss, simpset,...}) =>
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   283
            ThyInfo {path = path, children = children, parents = parents,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   284
                     thy_time = thy_time, ml_time = ml_time,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   285
                     theory = theory, thms = thms,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   286
                     thy_ss = thy_ss, simpset = simpset}
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   287
        | None => error ("set_info: theory " ^ tname ^ " not found");
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   288
  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   289
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   290
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   291
(*Mark theory as changed since last read if it has been completly read *)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   292
fun mark_outdated tname =
971
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   293
  let val t = get_thyinfo tname;
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   294
  in if is_none t then ()
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   295
     else
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   296
       let val ThyInfo {thy_time, ml_time, ...} = the t
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   297
       in set_info tname (if is_none thy_time then None else Some "")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   298
                         (if is_none ml_time then None else Some "")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   299
       end
971
f4815812665b fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents: 922
diff changeset
   300
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   301
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   302
(*Make head of HTML dependency charts
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   303
  Parameters are:
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   304
    file: HTML file
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   305
    tname: theory name
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   306
    suffix: suffix of complementary chart
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   307
            (sup if this head is for a sub-chart, sub if it is for a sup-chart;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   308
             empty for Pure and CPure sub-charts)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   309
    gif_path: relative path to directory containing GIFs
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   310
    index_path: relative path to directory containing main theory chart
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   311
*)
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   312
fun mk_charthead file tname title green_arrow gif_path index_path package =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   313
  output (file,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   314
   "<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   315
   "</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   316
   "</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   317
   "<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   318
   \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   319
   \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   320
   \\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   321
   (if not green_arrow then "" else
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   322
      "<BR><IMG SRC = \"" ^ tack_on gif_path "green_arrow.gif\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   323
      \\" ALT = &gt;></A> stands for repeated subtrees") ^
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   324
   "<P><A HREF = \"" ^ tack_on index_path "index.html\
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   325
   \\">Back</A> to the main theory chart of " ^ package ^ ".\n<HR>\n<PRE>");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   326
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   327
(*Convert .thy file to HTML and make chart of its super-theories*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   328
fun thyfile2html tpath tname =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   329
  let
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   330
    val gif_path = relative_path tpath (!gif_path);
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   331
    val package = hd (rev (space_explode "/" (!index_path)));
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   332
    val index_path = relative_path tpath (!index_path);
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   333
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   334
    (*Make list of all theories and all theories that own a .thy file*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   335
    fun list_theories [] theories thy_files = (theories, thy_files)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   336
      | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   337
                      theories thy_files =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   338
          list_theories ts (tname :: theories)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   339
            (if is_some thy_time andalso the thy_time <> "" then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   340
               tname :: thy_files
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   341
             else thy_files);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   342
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   343
    val (theories, thy_files) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   344
      list_theories (Symtab.dest (!loaded_thys)) [] [];
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   345
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   346
    (*Do the conversion*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   347
    fun gettext thy_file  =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   348
      let
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   349
        (*Convert special HTML characters ('&', '>', and '<')*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   350
        val file =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   351
          explode (execute ("sed -e 's/\\&/\\&amp;/g' -e 's/>/\\&gt;/g' \
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   352
                            \-e 's/</\\&lt;/g' " ^ thy_file));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   353
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   354
        (*Isolate first (possibly nested) comment;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   355
          skip all leading whitespaces*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   356
        val (comment, file') =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   357
          let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   358
                | first_comment ("*" :: ")" :: cs) co d =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   359
                    first_comment cs (co ^ "*)") (d-1)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   360
                | first_comment ("(" :: "*" :: cs) co d =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   361
                    first_comment cs (co ^ "(*") (d+1)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   362
                | first_comment (" "  :: cs) "" 0 = first_comment cs "" 0
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   363
                | first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   364
                | first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   365
                | first_comment cs           "" 0 = ("", cs)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   366
                | first_comment (c :: cs) co d =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   367
                    first_comment cs (co ^ implode [c]) d
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   368
                | first_comment [] co _ =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   369
                    error ("Unexpected end of file " ^ tname ^ ".thy.");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   370
          in first_comment file "" 0 end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   371
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   372
        (*Process line defining theory's ancestors;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   373
          convert valid theory names to links to their HTML file*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   374
        val (ancestors, body) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   375
          let
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   376
            fun make_links l result =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   377
              let val (pre, letter) = take_prefix (not o is_letter) l;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   378
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   379
                  val (id, rest) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   380
                    take_prefix (is_quasi_letter orf is_digit) letter;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   381
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   382
                  val id = implode id;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   383
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   384
                  (*Make a HTML link out of a theory name*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   385
                  fun make_link t =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   386
                    let val path = path_of t;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   387
                    in "<A HREF = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   388
                       tack_on (relative_path tpath path) t ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   389
                       ".html\">" ^ t ^ "</A>" end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   390
              in if not (id mem theories) then (result, implode l)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   391
                 else if id mem thy_files then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   392
                   make_links rest (result ^ implode pre ^ make_link id)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   393
                 else make_links rest (result ^ implode pre ^ id)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   394
              end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   395
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   396
            val (pre, rest) = take_prefix (fn c => c <> "=") file';
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   397
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   398
            val (ancestors, body) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   399
              if null rest then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   400
                error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   401
                       \(Make sure that the last line ends with a linebreak.)")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   402
              else
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   403
                make_links rest "";
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   404
          in (implode pre ^ ancestors, body) end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   405
      in "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   406
         "<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   407
         tack_on index_path "index.html\
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   408
         \\">Back</A> to the main theory chart of " ^ package ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   409
         ".\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   410
         "</PRE>\n<HR><H2>Theorems proved in <A HREF = \"" ^ tname ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   411
         ".ML\">" ^ tname ^ ".ML</A>:</H2>\n"
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   412
      end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   413
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   414
    (** Make chart of super-theories **)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   415
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   416
    val sup_out = open_out (tack_on tpath tname ^ "_sup.html");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   417
    val sub_out = open_out (tack_on tpath tname ^ "_sub.html");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   418
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   419
    (*Theories that already have been listed in this chart*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   420
    val listed = ref [];
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   421
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   422
    val wanted_theories =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   423
      filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   424
             theories;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   425
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   426
    (*Make nested list of theories*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   427
    fun list_ancestors tname level continued =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   428
      let
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   429
        fun mk_entry [] = ()
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   430
          | mk_entry (t::ts) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   431
            let
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   432
              val is_pure = t = "Pure" orelse t = "CPure";
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   433
              val path = path_of t;
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   434
              val rel_path = if is_pure then index_path
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   435
                             else relative_path tpath path;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   436
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   437
              fun mk_offset [] cur =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   438
                    if level < cur then error "Error in mk_offset"
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   439
                    else implode (replicate (level - cur) "    ")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   440
                | mk_offset (l::ls) cur =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   441
                    implode (replicate (l - cur) "    ") ^ "|   " ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   442
                    mk_offset ls (l+1);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   443
            in output (sup_out,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   444
                 " " ^ mk_offset continued 0 ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   445
                 "\\__" ^ (if is_pure then t else "<A HREF=\"" ^ 
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   446
                             tack_on rel_path t ^ ".html\">" ^ t ^ "</A>") ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   447
                 " <A HREF = \"" ^ tack_on rel_path t ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   448
                 "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   449
                 tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   450
                 (if is_pure then ""
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   451
                  else "<A HREF = \"" ^ tack_on rel_path t ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   452
                       "_sup.html\"><IMG ALIGN=TOP SRC = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   453
                       tack_on gif_path "blue_arrow.gif\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   454
                       \\" ALT = /\\></A>"));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   455
              if t mem (!listed) andalso not (null (parents_of t)) then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   456
                output (sup_out,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   457
                  "<A HREF = \"" ^ tack_on rel_path t ^ "_sup.html\">\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   458
                  \<IMG ALIGN=TOP SRC = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   459
                  tack_on gif_path "green_arrow.gif\" ALT = &gt;></A>\n")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   460
              else (output (sup_out, "\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   461
                    listed := t :: (!listed);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   462
                    list_ancestors t (level+1) (if null ts then continued
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   463
                                                else continued @ [level]);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   464
                    mk_entry ts)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   465
            end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   466
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   467
        val relatives =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   468
          filter (fn s => s mem wanted_theories) (parents_of tname);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   469
      in mk_entry relatives end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   470
  in if is_some (!cur_htmlfile) then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   471
       error "thyfile2html: Last theory's HTML has not been closed."
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   472
     else ();
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   473
     cur_htmlfile := Some (open_out (tack_on tpath tname ^ ".html"));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   474
     output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   475
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   476
     mk_charthead sup_out tname "Ancestors" true gif_path index_path package;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   477
     output(sup_out,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   478
       "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   479
       \<A HREF = \"" ^ tname ^ "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   480
       tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   481
     list_ancestors tname 0 [];
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   482
     output (sup_out, "</PRE><HR></BODY></HTML>");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   483
     close_out sup_out;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   484
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   485
     mk_charthead sub_out tname "Children" false gif_path index_path package;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   486
     output(sub_out,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   487
       "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   488
       \<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   489
       tack_on gif_path "blue_arrow.gif\" ALT = \\/></A>\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   490
     close_out sub_out
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   491
  end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   492
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   493
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   494
(*Read .thy and .ML files that haven't been read yet or have changed since
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   495
  they were last read;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   496
  loaded_thys is a thy_info list ref containing all theories that have
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   497
  completly been read by this and preceeding use_thy calls.
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   498
  If a theory changed since its last use its children are marked as changed *)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   499
fun use_thy name =
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   500
  let
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   501
    val (path, tname) = split_filename name;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   502
    val (thy_file, ml_file) = get_filenames path tname;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   503
    val (abs_path, _) = if thy_file = "" then split_filename ml_file
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   504
                        else split_filename thy_file;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   505
    val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   506
    val old_parents = parents_of tname;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   507
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   508
    (*Set absolute path for loaded theory *)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   509
    fun set_path () =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   510
      let val ThyInfo {children, parents, thy_time, ml_time, theory, thms,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   511
                       thy_ss, simpset, ...} =
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   512
            the (Symtab.lookup (!loaded_thys, tname));
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   513
      in loaded_thys := Symtab.update ((tname,
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   514
                          ThyInfo {path = abs_path,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   515
                                   children = children, parents = parents,
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   516
                                   thy_time = thy_time, ml_time = ml_time,
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   517
                                   theory = theory, thms = thms,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   518
                                   thy_ss = thy_ss, simpset = simpset}),
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   519
                          !loaded_thys)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   520
      end;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   521
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   522
    (*Mark all direct descendants of a theory as changed *)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   523
    fun mark_children thy =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   524
      let val children = children_of thy;
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   525
          val present = filter (is_some o get_thyinfo) children;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   526
          val loaded = filter already_loaded present;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   527
      in if loaded <> [] then
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   528
           writeln ("The following children of theory " ^ (quote thy)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   529
                    ^ " are now out-of-date: "
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   530
                    ^ (quote (space_implode "\",\"" loaded)))
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   531
         else ();
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   532
         seq mark_outdated present
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   533
      end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   534
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   535
    (*Remove theorems associated with a theory*)
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   536
    fun delete_thms () =
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   537
      let
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   538
        val tinfo = case get_thyinfo tname of
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   539
            Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   540
                           thy_ss, simpset, ...}) =>
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   541
              ThyInfo {path = path, children = children, parents = parents,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   542
                       thy_time = thy_time, ml_time = ml_time,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   543
                       theory = theory, thms = Symtab.null,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   544
                       thy_ss = thy_ss, simpset = simpset}
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   545
          | None => ThyInfo {path = "", children = [], parents = [],
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   546
                             thy_time = None, ml_time = None,
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   547
                             theory = None, thms = Symtab.null,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   548
                             thy_ss = None, simpset = None};
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   549
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   550
        val ThyInfo {theory, ...} = tinfo;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   551
      in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   552
         case theory of
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   553
             Some t => delete_thm_db t
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   554
           | None => ()
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   555
      end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   556
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   557
    fun save_thy_ss () =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   558
      let val ThyInfo {path, children, parents, thy_time, ml_time,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   559
                       theory, thms, simpset, ...} = the (get_thyinfo tname);
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   560
      in loaded_thys := Symtab.update
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   561
           ((tname, ThyInfo {path = path,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   562
                             children = children, parents = parents,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   563
                             thy_time = thy_time, ml_time = ml_time,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   564
                             theory = theory, thms = thms,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   565
                             thy_ss = Some (!Simplifier.simpset),
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   566
                             simpset = simpset}),
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   567
            !loaded_thys)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   568
      end;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   569
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   570
    fun save_simpset () =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   571
      let val ThyInfo {path, children, parents, thy_time, ml_time,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   572
                       theory, thms, thy_ss, ...} = the (get_thyinfo tname);
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   573
      in loaded_thys := Symtab.update
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   574
           ((tname, ThyInfo {path = path,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   575
                             children = children, parents = parents,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   576
                             thy_time = thy_time, ml_time = ml_time,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   577
                             theory = theory, thms = thms,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   578
                             thy_ss = thy_ss,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   579
                             simpset = Some (!Simplifier.simpset)}),
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   580
            !loaded_thys)
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   581
      end;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   582
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   583
   (*Add theory to file listing all loaded theories (for index.html)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   584
     and to the sub-charts of its parents*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   585
   fun mk_html () =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   586
     let val new_parents = parents_of tname \\ old_parents;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   587
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   588
         (*Add child to parents' sub-theory charts*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   589
         fun add_to_parents t =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   590
           let val is_pure = t = "Pure" orelse t = "CPure";
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   591
               val path = if is_pure then (!index_path) else path_of t;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   592
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   593
               val gif_path = relative_path path (!gif_path);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   594
               val rel_path = relative_path path abs_path;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   595
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   596
               val out = open_append (tack_on path t ^ "_sub.html");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   597
           in output (out,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   598
                " |\n \\__<A HREF=\"" ^ tack_on rel_path tname ^ ".html\">" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   599
                tname ^ "</A> <A HREF = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   600
                tack_on rel_path tname ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   601
                "_sub.html\"><IMG ALIGN=TOP SRC = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   602
                tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   603
                \<A HREF = \"" ^ tack_on rel_path tname ^ "_sup.html\">\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   604
                \<IMG ALIGN=TOP SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   605
                \\" ALT = /\\></A>\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   606
              close_out out
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   607
           end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   608
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   609
         val theory_list =
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   610
           open_append (tack_on (!index_path) "theory_list.txt");
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   611
     in output (theory_list, tname ^ " " ^ abs_path ^ "\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   612
        close_out theory_list;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   613
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   614
        seq add_to_parents new_parents
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   615
     end
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   616
  in if thy_uptodate andalso ml_uptodate then ()
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   617
     else
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   618
      (if thy_file = "" then ()
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   619
       else if thy_uptodate then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   620
         simpset := let val ThyInfo {thy_ss, ...} = the (get_thyinfo tname);
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   621
                    in the thy_ss end
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   622
       else
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   623
         (writeln ("Reading \"" ^ name ^ ".thy\"");
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   624
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   625
          delete_thms ();
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   626
          read_thy tname thy_file;
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   627
          use (out_name tname);
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   628
          save_thy_ss ();
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   629
1308
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   630
          (*Store axioms of theory
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   631
            (but only if it's not a copy of an older theory)*)
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   632
          let val parents = parents_of tname;
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   633
              val this_thy = theory_of tname;
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   634
              val axioms =
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   635
                if length parents = 1
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   636
                   andalso Sign.eq_sg (sign_of (theory_of (hd parents)),
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   637
                                       sign_of this_thy) then []
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   638
                else axioms_of this_thy;
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   639
          in map store_thm_db axioms end;
396ef8aa37b7 removed "duplicate" warning from store_thm_db;
clasohm
parents: 1291
diff changeset
   640
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   641
          if not (!delete_tmpfiles) then ()
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   642
          else delete_file (out_name tname);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   643
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   644
          if not (!make_html) then ()
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   645
          else thyfile2html abs_path tname
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   646
         );
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   647
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   648
       set_info tname (Some (file_info thy_file)) None;
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   649
                                       (*mark thy_file as successfully loaded*)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   650
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   651
       if ml_file = "" then ()
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   652
       else (writeln ("Reading \"" ^ name ^ ".ML\"");
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   653
             use ml_file);
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   654
       save_simpset ();
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   655
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   656
       (*Store theory again because it could have been redefined*)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   657
       use_string
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   658
         ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   659
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
   660
       (*Add theory to list of all loaded theories (for index.html)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   661
         and add it to its parents' sub-charts*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   662
       if !make_html then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   663
         let val path = path_of tname;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   664
         in if path = "" then mk_html ()    (*first time theory has been read*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   665
            else ()
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   666
         end
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   667
       else ();
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   668
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   669
       (*Now set the correct info*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   670
       set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   671
       set_path ();
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   672
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   673
       (*Mark theories that have to be reloaded*)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   674
       mark_children tname;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   675
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   676
       (*Close HTML file*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   677
       case !cur_htmlfile of
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   678
           Some out => (output (out, "<HR></BODY></HTML>\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   679
                        close_out out;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   680
                        cur_htmlfile := None)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   681
         | None => ()
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   682
      )
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   683
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   684
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   685
fun time_use_thy tname = timeit(fn()=>
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   686
   (writeln("\n**** Starting Theory " ^ tname ^ " ****");
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   687
    use_thy tname;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   688
    writeln("\n**** Finished Theory " ^ tname ^ " ****"))
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   689
   );
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   690
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   691
(*Load all thy or ML files that have been changed and also
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   692
  all theories that depend on them *)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   693
fun update () =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   694
  let (*List theories in the order they have to be loaded *)
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   695
      fun load_order [] result = result
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   696
        | load_order thys result =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   697
            let fun next_level [] = []
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   698
                  | next_level (t :: ts) =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   699
                      let val children = children_of t
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   700
                      in children union (next_level ts) end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   701
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   702
                val descendants = next_level thys;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   703
            in load_order descendants ((result \\ descendants) @ descendants)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   704
            end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   705
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   706
      fun reload_changed (t :: ts) =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   707
            let fun abspath () = case get_thyinfo t of
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   708
                                     Some (ThyInfo {path, ...}) => path
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   709
                                   | None => "";
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   710
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   711
                val (thy_file, ml_file) = get_filenames (abspath ()) t;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   712
                val (thy_uptodate, ml_uptodate) =
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   713
                        thy_unchanged t thy_file ml_file;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   714
            in if thy_uptodate andalso ml_uptodate then ()
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   715
                                                   else use_thy t;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   716
               reload_changed ts
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   717
            end
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   718
        | reload_changed [] = ();
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   719
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   720
     (*Remove all theories that are no descendants of ProtoPure.
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   721
       If there are still children in the deleted theory's list
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   722
       schedule them for reloading *)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   723
     fun collect_garbage no_garbage =
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   724
       let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   725
                 if tname mem no_garbage then collect ts
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   726
                 else (writeln ("Theory \"" ^ tname ^
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   727
                       "\" is no longer linked with ProtoPure - removing it.");
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   728
                       remove_thy tname;
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   729
                       seq mark_outdated children)
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   730
             | collect [] = ()
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   731
       in collect (Symtab.dest (!loaded_thys)) end;
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   732
  in collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 871
diff changeset
   733
     reload_changed (load_order ["Pure", "CPure"] [])
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   734
  end;
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   735
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   736
(*Merge theories to build a base for a new theory.
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   737
  Base members are only loaded if they are missing.*)
586
201e115d8031 renamed base_on into mk_base and moved it to the beginning of the generated
clasohm
parents: 559
diff changeset
   738
fun mk_base bases child mk_draft =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   739
  let (*Show the cycle that would be created by add_child*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   740
      fun show_cycle base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   741
        let fun find_it result curr =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   742
              let val tinfo = get_thyinfo curr
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   743
              in if base = curr then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   744
                   error ("Cyclic dependency of theories: "
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   745
                          ^ child ^ "->" ^ base ^ result)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   746
                 else if is_some tinfo then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   747
                   let val ThyInfo {children, ...} = the tinfo
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   748
                   in seq (find_it ("->" ^ curr ^ result)) children
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   749
                   end
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   750
                 else ()
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   751
              end
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   752
        in find_it "" child end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   753
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   754
      (*Check if a cycle would be created by add_child*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   755
      fun find_cycle base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   756
        if base mem (get_descendants [child]) then show_cycle base
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   757
        else ();
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   758
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   759
      (*Add child to child list of base*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   760
      fun add_child base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   761
        let val tinfo =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   762
              case Symtab.lookup (!loaded_thys, base) of
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   763
                  Some (ThyInfo {path, children, parents, thy_time, ml_time,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   764
                           theory, thms, thy_ss, simpset}) =>
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   765
                    ThyInfo {path = path,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   766
                             children = child ins children, parents = parents,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   767
                             thy_time = thy_time, ml_time = ml_time,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   768
                             theory = theory, thms = thms,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   769
                             thy_ss = thy_ss, simpset = simpset}
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   770
                | None => ThyInfo {path = "", children = [child], parents = [],
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   771
                                   thy_time = None, ml_time = None,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   772
                                   theory = None, thms = Symtab.null,
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   773
                                   thy_ss = None, simpset = None};
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   774
        in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   775
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   776
      (*Load a base theory if not already done
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   777
        and no cycle would be created *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   778
      fun load base =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   779
          let val thy_loaded = already_loaded base
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   780
                                       (*test this before child is added *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   781
          in
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   782
            if child = base then
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   783
                error ("Cyclic dependency of theories: " ^ child
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   784
                       ^ "->" ^ child)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   785
            else
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   786
              (find_cycle base;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   787
               add_child base;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   788
               if thy_loaded then ()
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   789
               else (writeln ("Autoloading theory " ^ (quote base)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   790
                              ^ " (used by " ^ (quote child) ^ ")");
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   791
                     use_thy base)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   792
              )
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   793
          end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   794
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   795
      (*Get simpset for a theory*)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   796
      fun get_simpset tname =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   797
        let val ThyInfo {simpset, ...} = the (get_thyinfo tname);
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   798
        in simpset end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   799
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   800
      (*Load all needed files and make a list of all real theories *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   801
      fun load_base (Thy b :: bs) =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   802
           (load b;
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   803
            b :: load_base bs)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   804
        | load_base (File b :: bs) =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   805
           (load b;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   806
            load_base bs)                    (*don't add it to mergelist *)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   807
        | load_base [] = [];
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   808
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   809
      val dummy = unlink_thy child;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   810
      val mergelist = load_base bases;
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   811
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   812
      val dummy =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   813
        let val tinfo = case Symtab.lookup (!loaded_thys, child) of
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   814
              Some (ThyInfo {path, children, thy_time, ml_time, theory, thms,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   815
                             thy_ss, simpset, ...}) =>
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   816
                 ThyInfo {path = path,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   817
                          children = children, parents = mergelist,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   818
                          thy_time = thy_time, ml_time = ml_time,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   819
                          theory = theory, thms = thms,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   820
                          thy_ss = thy_ss, simpset = simpset}
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   821
             | None => error ("set_parents: theory " ^ child ^ " not found");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   822
        in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   823
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   824
      val base_thy = (writeln ("Loading theory " ^ (quote child));
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   825
                      merge_thy_list mk_draft (map theory_of mergelist));
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   826
 in simpset := foldr merge_ss (mapfilter get_simpset mergelist, empty_ss);
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   827
    base_thy
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   828
 end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   829
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   830
(*Change theory object for an existent item of loaded_thys*)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   831
fun store_theory (thy, tname) =
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   832
  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   833
               Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   834
                              thy_ss, simpset, ...}) =>
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   835
                 ThyInfo {path = path, children = children, parents = parents,
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   836
                          thy_time = thy_time, ml_time = ml_time,
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   837
                          theory = Some thy, thms = thms,
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   838
                          thy_ss = thy_ss, simpset = simpset}
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   839
             | None => error ("store_theory: theory " ^ tname ^ " not found");
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents: 1098
diff changeset
   840
  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents: 1098
diff changeset
   841
  end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   842
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   843
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   844
(** store and retrieve theorems **)
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   845
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   846
(*Guess to which theory a signature belongs and return it's thy_info*)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   847
fun thyinfo_of_sign sg =
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   848
  let
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   849
    val ref xname = hd (#stamps (Sign.rep_sg sg));
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   850
    val opt_info = get_thyinfo xname;
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   851
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   852
    fun eq_sg (ThyInfo {theory = None, ...}) = false
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   853
      | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   854
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   855
    val show_sg = Pretty.str_of o Sign.pretty_sg;
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   856
  in
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   857
    if is_some opt_info andalso eq_sg (the opt_info) then
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   858
      (xname, the opt_info)
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   859
    else
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   860
      (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   861
        Some name_info => name_info
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   862
      | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   863
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
   864
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   865
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   866
(*Try to get the theory object corresponding to a given signature*)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   867
fun theory_of_sign sg =
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   868
  (case thyinfo_of_sign sg of
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   869
    (_, ThyInfo {theory = Some thy, ...}) => thy
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   870
  | _ => sys_error "theory_of_sign");
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   871
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   872
(*Try to get the theory object corresponding to a given theorem*)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   873
val theory_of_thm = theory_of_sign o #sign o rep_thm;
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   874
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   875
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   876
(* Store theorems *)
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   877
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   878
(*Store a theorem in the thy_info of its theory,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   879
  and in the theory's HTML file*)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   880
fun store_thm (name, thm) =
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   881
  let
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   882
    val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   883
                            theory, thms, thy_ss, simpset}) =
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   884
      thyinfo_of_sign (#sign (rep_thm thm));
1236
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1223
diff changeset
   885
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   886
    val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
774
ea19f22ed23c added warning for already stored theorem to store_thm
clasohm
parents: 759
diff changeset
   887
      handle Symtab.DUPLICATE s => 
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   888
        (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
1236
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1223
diff changeset
   889
           (writeln ("Warning: Theory database already contains copy of\
774
ea19f22ed23c added warning for already stored theorem to store_thm
clasohm
parents: 759
diff changeset
   890
                     \ theorem " ^ quote name);
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   891
            (thms, true))
1236
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1223
diff changeset
   892
         else error ("Duplicate theorem name " ^ quote s
b54d51df9065 added check for duplicate theorems in theorem database;
clasohm
parents: 1223
diff changeset
   893
                     ^ " used in theory database"));
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   894
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   895
    fun thm_to_html () =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   896
      let fun escape []       = ""
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   897
            | escape ("<"::s) = "&lt;" ^ escape s
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   898
            | escape (">"::s) = "&gt;" ^ escape s
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   899
            | escape ("&"::s) = "&amp;" ^ escape s
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   900
            | escape (c::s)   = c ^ escape s;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   901
      in case !cur_htmlfile of
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   902
             Some out =>
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   903
               output (out, "<EM>" ^ name ^ "</EM>\n<PRE>" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   904
                            escape (explode (string_of_thm (freeze thm))) ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   905
                            "</PRE><P>\n")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   906
           | None => ()
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   907
      end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   908
  in
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   909
    loaded_thys := Symtab.update
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   910
     ((thy_name, ThyInfo {path = path, children = children, parents = parents,
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   911
                          thy_time = thy_time, ml_time = ml_time,
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   912
                          theory = theory, thms = thms',
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   913
                          thy_ss = thy_ss, simpset = simpset}),
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1236
diff changeset
   914
      !loaded_thys);
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   915
    thm_to_html ();
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   916
    if duplicate then thm else store_thm_db (name, thm)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   917
  end;
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   918
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   919
(*Store result of proof in loaded_thys and as ML value*)
758
c2b210bda710 added bind_thm
clasohm
parents: 746
diff changeset
   920
c2b210bda710 added bind_thm
clasohm
parents: 746
diff changeset
   921
val qed_thm = ref flexpair_def(*dummy*);
c2b210bda710 added bind_thm
clasohm
parents: 746
diff changeset
   922
c2b210bda710 added bind_thm
clasohm
parents: 746
diff changeset
   923
fun bind_thm (name, thm) =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   924
 (qed_thm := standard thm;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   925
  store_thm (name, standard thm);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   926
  use_string ["val " ^ name ^ " = !qed_thm;"]);
758
c2b210bda710 added bind_thm
clasohm
parents: 746
diff changeset
   927
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   928
fun qed name =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   929
 (qed_thm := result ();
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   930
  store_thm (name, !qed_thm);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   931
  use_string ["val " ^ name ^ " = !qed_thm;"]);
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   932
746
6e815617d79f added qed_goal[w]
clasohm
parents: 715
diff changeset
   933
fun qed_goal name thy agoal tacsf =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   934
 (qed_thm := prove_goal thy agoal tacsf;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   935
  store_thm (name, !qed_thm);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   936
  use_string ["val " ^ name ^ " = !qed_thm;"]);
746
6e815617d79f added qed_goal[w]
clasohm
parents: 715
diff changeset
   937
6e815617d79f added qed_goal[w]
clasohm
parents: 715
diff changeset
   938
fun qed_goalw name thy rths agoal tacsf =
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   939
 (qed_thm := prove_goalw thy rths agoal tacsf;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   940
  store_thm (name, !qed_thm);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   941
  use_string ["val " ^ name ^ " = !qed_thm;"]);
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   942
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   943
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   944
(* Retrieve theorems *)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   945
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   946
(*Get all theorems belonging to a given theory*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   947
fun thmtab_of_thy thy =
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   948
  let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   949
  in thms end;
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   950
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   951
fun thmtab_of_name name =
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   952
  let val ThyInfo {thms, ...} = the (get_thyinfo name);
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   953
  in thms end;
476
836cad329311 added check for concistency of filename and theory name;
clasohm
parents: 426
diff changeset
   954
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   955
(*Get a stored theorem specified by theory and name*)
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   956
fun get_thm thy name =
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   957
  let fun get [] [] searched =
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   958
           raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   959
        | get [] ng searched =
871
1c060d444a81 simplified get_thm a bit
clasohm
parents: 783
diff changeset
   960
            get (ng \\ searched) [] searched
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   961
        | get (t::ts) ng searched =
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   962
            (case Symtab.lookup (thmtab_of_name t, name) of
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   963
                 Some thm => thm
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   964
               | None => get ts (ng union (parents_of t)) (t::searched));
783
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   965
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   966
      val (tname, _) = thyinfo_of_sign (sign_of thy);
08f1785a4384 changed get_thm to search all parent theories if the theorem is not found
clasohm
parents: 778
diff changeset
   967
  in get [tname] [] [] end;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   968
715
f76ad10f5802 added call of store_theory after thy file has been read
clasohm
parents: 586
diff changeset
   969
(*Get stored theorems of a theory*)
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   970
val thms_of = Symtab.dest o thmtab_of_thy;
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   971
1262
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   972
(*Get simpset of a theory*)
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   973
fun simpset_of tname =
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   974
  case get_thyinfo tname of
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   975
      Some (ThyInfo {simpset, ...}) =>
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   976
        if is_some simpset then the simpset
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   977
        else error ("Simpset of theory " ^ tname ^ " has not been stored yet")
8f40ff1299d8 added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents: 1244
diff changeset
   978
    | None => error ("Theory " ^ tname ^ " not stored by loader");
559
00365d2e0c50 added theory_of_sign, theory_of_thm;
wenzelm
parents: 476
diff changeset
   979
778
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   980
(* print theory *)
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   981
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   982
fun print_thms thy =
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   983
  let
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   984
    val thms = thms_of thy;
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   985
    fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   986
      Pretty.quote (pretty_thm th)];
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   987
  in
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   988
    Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   989
  end;
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   990
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   991
fun print_theory thy = (Drule.print_theory thy; print_thms thy);
9a03ed31ea2f added print_theory that prints stored thms;
wenzelm
parents: 774
diff changeset
   992
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   993
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   994
(* Misc HTML functions *)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   995
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   996
(*Init HTML generator by setting paths and creating new files*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   997
fun init_html () =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   998
  let val pure_out = open_out "Pure_sub.html";
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
   999
      val cpure_out = open_out "CPure_sub.html";
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1000
      val theory_list = close_out (open_out "theory_list.txt");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1001
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1002
      val rel_gif_path = relative_path (pwd ()) (!gif_path);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1003
      val package = hd (rev (space_explode "/" (pwd ())));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1004
  in make_html := true;
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1005
     index_path := pwd();
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1006
     writeln ("Setting path for index.html to " ^ quote (!index_path) ^
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1007
              "\nGIF path has been set to " ^ quote (!gif_path));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1008
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1009
     mk_charthead pure_out "Pure" "Children" false rel_gif_path "" package;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1010
     mk_charthead cpure_out "CPure" "Children" false rel_gif_path "" package;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1011
     output (pure_out, "Pure\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1012
     output (cpure_out, "CPure\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1013
     close_out pure_out;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1014
     close_out cpure_out
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1015
  end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1016
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1017
(*Generate index.html*)
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1018
fun make_chart () = if not (!make_html) then () else
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1019
  let val theory_list = open_in (tack_on (!index_path) "theory_list.txt");
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1020
      val theories = space_explode "\n" (input (theory_list, 999999));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1021
      val dummy = close_in theory_list;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1022
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1023
      (*Path to Isabelle's main directory = $gif_path/.. *)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1024
      val base_path = "/" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1025
        space_implode "/" (rev (tl (rev (space_explode "/" (!gif_path)))));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1026
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1027
      val gif_path = relative_path (!index_path) (!gif_path);
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1028
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1029
      (*Make entry for main chart of all theories.*)
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1030
      fun main_entries [] curdir =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1031
            implode (replicate (length curdir -1) "</UL>\n")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1032
        | main_entries (t::ts) curdir =
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1033
            let
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1034
              val (name, path) = take_prefix (not_equal " ") (explode t);
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1035
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1036
              val tname = implode name
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1037
              val tpath =
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1038
                tack_on (relative_path (!index_path) (implode (tl path)))
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1039
                        tname;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1040
              val subdir = space_explode "/"
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1041
                                 (relative_path base_path (implode (tl path)));
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1042
              val level_diff = length subdir - length curdir;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1043
            in "\n" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1044
               (if subdir <> curdir then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1045
                  (implode (if level_diff > 0 then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1046
                              replicate level_diff "<UL>\n"
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1047
                            else if level_diff < 0 then
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1048
                              replicate (~level_diff) "</UL>\n"
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1049
                            else []) ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1050
                  "<H3>" ^ space_implode "/" subdir ^ "</H3>\n")
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1051
                else "") ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1052
               "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1053
               tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1054
               "<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1055
               tack_on gif_path "blue_arrow.gif\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1056
               \\" ALT = /\\></A> <A HREF = \"" ^ tpath ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1057
               ".html\">" ^ tname ^ "</A><BR>\n" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1058
               main_entries ts subdir
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1059
            end;
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1060
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1061
      val out = open_out (tack_on (!index_path) "index.html");
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1062
      val subdir = relative_path base_path (!index_path);
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1063
  in output (out,
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1064
       "<HTML><HEAD><TITLE>Isabelle/" ^ subdir ^ "</TITLE></HEAD>\n\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1065
       \<H2>Isabelle/" ^ subdir ^ "</H2>\n\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1066
       \The name of every theory is linked to its theory file<BR>\n\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1067
       \<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1068
       \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1069
       \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1070
       \\" ALT = /\\></A> stands for supertheories (parent theories)\n\
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1071
       \<P><A HREF = \"" ^
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1308
diff changeset
  1072
       tack_on (relative_path (!index_path) base_path) "index.html\">\
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1073
       \Back</A> to the index of Isabelle logics.\n<HR>" ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1074
       main_entries theories (space_explode "/" base_path) ^
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1075
       "</BODY></HTML>\n");
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1076
     close_out out
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1262
diff changeset
  1077
  end;
391
e960fe156cd8 (was Thy/read.ML)
wenzelm
parents:
diff changeset
  1078
end;