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