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