# HG changeset patch
# User berghofe
# Date 870819781 -7200
# Node ID cdfb8b7e60fa59f2e205a3911deb74ce844afc7e
# Parent 43c7912aac8d825b26a699f86b5c204637565c34
Moved several functions:
html generation --> browser_info.ML
theory information storage / retrieval --> thy_info.ML
theorem storage (qed) --> thm_database.ML
diff -r 43c7912aac8d -r cdfb8b7e60fa src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML Wed Aug 06 00:18:34 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML Wed Aug 06 00:23:01 1997 +0200
@@ -4,62 +4,19 @@
Tobias Nipkow and L C Paulson
Copyright 1994 TU Muenchen
-Functions for reading theory files, and storing and retrieving theories,
-theorems.
+Functions for reading theory files.
*)
-(*Types for theory storage*)
-
-(*Functions to handle arbitrary data added by the user; type "exn" is used
- to store data*)
-datatype thy_methods =
- ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
-
-datatype thy_info =
- ThyInfo of {path: string,
- children: string list, parents: string list,
- thy_time: string option, ml_time: string option,
- theory: theory option, thms: thm Symtab.table,
- methods: thy_methods Symtab.table,
- data: exn Symtab.table * exn Symtab.table};
- (*thy_time, ml_time = None theory file has not been read yet
- = Some "" theory was read but has either been marked
- as outdated or there is no such file for
- this theory (see e.g. 'virtual' theories
- like Pure or theories without a ML file)
- theory = None theory has not been read yet
-
- parents: While 'children' contains all theories the theory depends
- on (i.e. also ones quoted in the .thy file),
- 'parents' only contains the theories which were used to form
- the base of this theory.
-
- methods: three methods for each user defined data;
- merge: merges data of ancestor theories
- put: retrieves data from loaded_thys and stores it somewhere
- get: retrieves data from somewhere and stores it
- in loaded_thys
- Warning: If these functions access reference variables inside
- READTHY, they have to be redefined each time
- init_thy_reader is invoked
- data: user defined data; exn is used to allow arbitrary types;
- first element of pairs contains result that get returned after
- thy file was read, second element after ML file was read;
- if ML files has not been read, second element is identical to
- first one because get_thydata, which is meant to return the
- latest data, always accesses the 2nd element
- *)
-
signature READTHY =
sig
datatype basetype = Thy of string
| File of string
- val loaded_thys : thy_info Symtab.table ref
val loadpath : string list ref
- val thy_reader_files: string list ref
val delete_tmpfiles: bool ref
+ val set_parser : (string -> string -> string) -> unit
+
val use_thy : string -> unit
val time_use_thy : string -> unit
val use_dir : string -> unit
@@ -67,158 +24,55 @@
val update : unit -> unit
val unlink_thy : string -> unit
val mk_base : basetype list -> string -> bool -> theory
- val store_theory : theory * string -> unit
-
- val theory_of : string -> theory
- val theory_of_sign : Sign.sg -> theory
- val theory_of_thm : thm -> theory
- val children_of : string -> string list
- val parents_of_name: string -> string list
- val thyname_of_sign: Sign.sg -> string
-
- val store_thm : string * thm -> thm
- val bind_thm : string * thm -> unit
- val qed : string -> unit
- val qed_thm : thm ref
- val qed_goal : string -> theory -> string
- -> (thm list -> tactic list) -> unit
- val qed_goalw : string -> theory -> thm list -> string
- -> (thm list -> tactic list) -> unit
- val get_thm : theory -> string -> thm
- val thms_of : theory -> (string * thm) list
- val delete_thms : string -> unit
-
- val add_thydata : string -> string * thy_methods -> unit
- val get_thydata : string -> string -> exn option
- val add_thy_reader_file: string -> unit
- val set_thy_reader_file: string -> unit
- val read_thy_reader_files: unit -> unit
- val set_current_thy: string -> unit
-
- val print_theory : theory -> unit
-
- val base_path : string ref
- val gif_path : string ref
- val index_path : string ref
- val pure_subchart : string option ref
- val make_html : bool ref
- val init_html : unit -> unit
- val finish_html : unit -> unit
- val section : string -> unit
end;
-functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
+structure ReadThy : READTHY =
struct
-open ThmDB;
+open ThmDB ThyInfo BrowserInfo;
+
datatype basetype = Thy of string
| File of string;
-val loaded_thys =
- ref (Symtab.make [("ProtoPure",
- ThyInfo {path = "",
- children = ["Pure", "CPure"], parents = [],
- thy_time = Some "", ml_time = Some "",
- theory = Some proto_pure_thy,
- thms = Symtab.null, methods = Symtab.null,
- data = (Symtab.null, Symtab.null)}),
- ("Pure",
- ThyInfo {path = "", children = [],
- parents = ["ProtoPure"],
- thy_time = Some "", ml_time = Some "",
- theory = Some pure_thy, thms = Symtab.null,
- methods = Symtab.null,
- data = (Symtab.null, Symtab.null)}),
- ("CPure",
- ThyInfo {path = "",
- children = [], parents = ["ProtoPure"],
- thy_time = Some "", ml_time = Some "",
- theory = Some cpure_thy,
- thms = Symtab.null,
- methods = Symtab.null,
- data = (Symtab.null, Symtab.null)})
- ]);
+
+(*parser for theory files*)
+val parser = ref ((K (K "")):string -> string -> string);
+
+
+(*set parser for theory files*)
+fun set_parser p = parser := p;
+
(*Default search path for theory files*)
val loadpath = ref ["."];
+
(*Directory given as parameter to use_thy. This is temporarily added to
loadpath while the theory's ancestors are loaded.*)
val tmp_loadpath = ref [] : string list ref;
-(*ML files to be read by init_thy_reader; they normally contain redefinitions
- of functions accessing reference variables inside READTHY*)
-val thy_reader_files = ref [] : string list ref;
(*Remove temporary files after use*)
-val delete_tmpfiles = ref true;
-
-
-(*Set location of graphics for HTML files
- (When this is executed for the first time we are in $ISABELLE/Pure/Thy.
- This path is converted to $ISABELLE/Tools by removing the last two
- directories and appending "Tools". All subsequently made ReadThy
- structures inherit this value.)
-*)
-val gif_path = ref (tack_on ("/" ^
- space_implode "/" (rev (tl (tl (rev (space_explode "/"
- (OS.FileSys.getDir ())))))))
- "Tools");
-
-(*Path of Isabelle's main directory*)
-val base_path = ref (
- "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ())))))));
-
-
-(** HTML variables **)
-
-(*Location of .theory-list.txt and index.html (set by init_html)*)
-val index_path = ref "";
-
-(*Location of .Pure_sub.html and .CPure_sub.html*)
-val pure_subchart = ref (None : string option);
-
-(*Controls whether HTML files should be generated*)
-val make_html = ref false;
-
-(*HTML file of theory currently being read
- (Initialized by thyfile2html; used by use_thy and store_thm)*)
-val cur_htmlfile = ref None : TextIO.outstream option ref;
-
-(*Boolean variable which indicates if the title "Theorems proved in foo.ML"
- has already been inserted into the current HTML file*)
-val cur_has_title = ref false;
-
-(*Name of theory currently being read*)
-val cur_thyname = ref "";
-
-
+val delete_tmpfiles = ref true;
+
(*Make name of the TextIO.output ML file for a theory *)
fun out_name tname = "." ^ tname ^ ".thy.ML";
+
(*Read a file specified by thy_file containing theory thy *)
fun read_thy tname thy_file =
let
val instream = TextIO.openIn thy_file;
val outstream = TextIO.openOut (out_name tname);
in
- TextIO.output (outstream, ThySyn.parse tname (TextIO.inputAll instream));
+ TextIO.output (outstream, (!parser) tname (TextIO.inputAll instream));
TextIO.closeOut outstream;
TextIO.closeIn instream
end;
-fun file_exists file = (file_info file <> "");
-
-(*Get last directory in path (e.g. /usr/proj/isabelle -> isabelle) *)
-fun last_path s = case space_explode "/" s of
- [] => ""
- | ds => last_elem ds;
-
-(*Get thy_info for a loaded theory *)
-fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
(*Check if a theory was completly loaded *)
fun already_loaded thy =
@@ -228,6 +82,7 @@
in is_some thy_time andalso is_some ml_time end
end;
+
(*Check if a theory file has changed since its last use.
Return a pair of boolean values for .thy and for .ML *)
fun thy_unchanged thy thy_file ml_file =
@@ -245,15 +100,6 @@
end
| None => (false, false)
-(*Get all direct descendants of a theory*)
-fun children_of t =
- case get_thyinfo t of Some (ThyInfo {children, ...}) => children
- | None => [];
-
-(*Get all direct ancestors of a theory*)
-fun parents_of_name t =
- case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
- | None => [];
(*Get all descendants of a theory list *)
fun get_descendants [] = []
@@ -261,16 +107,6 @@
let val children = children_of t
in children union (get_descendants (children union ts)) end;
-(*Get theory object for a loaded theory *)
-fun theory_of name =
- case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t
- | _ => error ("Theory " ^ name ^
- " not stored by loader");
-
-(*Get path where theory's files are located*)
-fun path_of tname =
- let val ThyInfo {path, ...} = the (get_thyinfo tname)
- in path end;
(*Find a file using a list of paths if no absolute or relative path is
specified.*)
@@ -286,6 +122,7 @@
if file_exists (tack_on path name) then tack_on path name
else "";
+
(*Get absolute pathnames for a new or already loaded theory *)
fun get_filenames path name =
let fun new_filename () =
@@ -326,6 +163,7 @@
else new_filename ()
end;
+
(*Remove theory from all child lists in loaded_thys *)
fun unlink_thy tname =
let fun remove (ThyInfo {path, children, parents, thy_time, ml_time,
@@ -335,11 +173,13 @@
thms = thms, methods = methods, data = data}
in loaded_thys := Symtab.map remove (!loaded_thys) end;
+
(*Remove a theory from loaded_thys *)
fun remove_thy tname =
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
(Symtab.dest (!loaded_thys)));
+
(*Change thy_time and ml_time for an existent item *)
fun set_info tname thy_time ml_time =
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
@@ -352,6 +192,7 @@
| None => error ("set_info: theory " ^ tname ^ " not found");
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
+
(*Mark theory as changed since last read if it has been completly read *)
fun mark_outdated tname =
let val t = get_thyinfo tname;
@@ -363,245 +204,6 @@
end
end;
-(*Remove theorems associated with a theory from theory and theorem database*)
-fun delete_thms tname =
- let
- val tinfo = case get_thyinfo tname of
- Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
- methods, data, ...}) =>
- ThyInfo {path = path, children = children, parents = parents,
- thy_time = thy_time, ml_time = ml_time,
- theory = theory, thms = Symtab.null,
- methods = methods, data = data}
- | None => error ("Theory " ^ tname ^ " not stored by loader");
-
- val ThyInfo {theory, ...} = tinfo;
- in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
- case theory of
- Some t => delete_thm_db t
- | None => ()
- end;
-
-(*Make head of HTML dependency charts
- Parameters are:
- file: HTML file
- tname: theory name
- suffix: suffix of complementary chart
- (sup if this head is for a sub-chart, sub if it is for a sup-chart;
- empty for Pure and CPure sub-charts)
- gif_path: relative path to directory containing GIFs
- index_path: relative path to directory containing main theory chart
-*)
-fun mk_charthead file tname title repeats gif_path index_path package =
- TextIO.output (file,
- "" ^ title ^ " of " ^ tname ^
- "\n" ^ title ^ " of theory " ^ tname ^
- "
\nThe name of every theory is linked to its theory file
\n" ^
- "![\\/](\"")
stands for subtheories (child theories)
\n\
- \ stands for supertheories (parent theories)\n" ^
- (if not repeats then "" else
- "
... stands for repeated subtrees") ^
- "\nBack to the index of " ^ package ^ "\n
\n");
-
-(*Convert .thy file to HTML and make chart of its super-theories*)
-fun thyfile2html tpath tname =
- let
- val gif_path = relative_path tpath (!gif_path);
-
- (*Determine name of current logic; if index_path is no subdirectory of
- base_path then we take the last directory of index_path*)
- val package =
- if (!index_path) = "" then
- error "index_path is empty. Please use 'init_html()' instead of \
- \'make_html := true'"
- else if (!index_path) subdir_of (!base_path) then
- relative_path (!base_path) (!index_path)
- else last_path (!index_path);
- val rel_index_path = relative_path tpath (!index_path);
-
- (*Make list of all theories and all theories that own a .thy file*)
- fun list_theories [] theories thy_files = (theories, thy_files)
- | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)
- theories thy_files =
- list_theories ts (tname :: theories)
- (if is_some thy_time andalso the thy_time <> "" then
- tname :: thy_files
- else thy_files);
-
- val (theories, thy_files) =
- list_theories (Symtab.dest (!loaded_thys)) [] [];
-
- (*Do the conversion*)
- fun gettext thy_file =
- let
- (*Convert special HTML characters ('&', '>', and '<')*)
- val file =
- explode (execute ("sed -e 's/\\&/\\&/g' -e 's/>/\\>/g' \
- \-e 's/" ^ t ^ "" end;
- in if not (id mem theories) then (result, implode l)
- else if id mem thy_files then
- make_links rest (result ^ implode pre ^ make_link id)
- else make_links rest (result ^ implode pre ^ id)
- end;
-
- val (pre, rest) = take_prefix (fn c => c <> "=") file';
-
- val (ancestors, body) =
- if null rest then
- error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\
- \(Make sure that the last line ends with a linebreak.)")
- else
- make_links rest "";
- in (implode pre ^ ancestors, body) end;
- in "" ^ tname ^ ".thy\n\n\n" ^
- "" ^ tname ^ ".thy
\nBack to the index of " ^ package ^
- "\n
\n\n\n" ^ comment ^ ancestors ^ body ^
- "
\n"
- end;
-
- (** Make chart of super-theories **)
-
- val sup_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sup.html"));
- val sub_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sub.html"));
-
- (*Theories that already have been listed in this chart*)
- val listed = ref [];
-
- val wanted_theories =
- filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure")
- theories;
-
- (*Make tree of theory dependencies*)
- fun list_ancestors tname level continued =
- let
- fun mk_entry [] = ()
- | mk_entry (t::ts) =
- let
- val is_pure = t = "Pure" orelse t = "CPure";
- val path = if is_pure then (the (!pure_subchart))
- else path_of t;
- val rel_path = relative_path tpath path;
- val repeated = t mem (!listed) andalso
- not (null (parents_of_name t));
-
- fun mk_offset [] cur =
- if level < cur then error "Error in mk_offset"
- else implode (replicate (level - cur) " ")
- | mk_offset (l::ls) cur =
- implode (replicate (l - cur) " ") ^ "| " ^
- mk_offset ls (l+1);
- in TextIO.output (sup_out,
- " " ^ mk_offset continued 0 ^
- "\\__" ^ (if is_pure then t else
- "" ^ t ^ "") ^
- (if repeated then "..." else " ") ^
- "" ^
- (if is_pure then ""
- else "") ^
- "\n");
- if repeated then ()
- else (listed := t :: (!listed);
- list_ancestors t (level+1) (if null ts then continued
- else continued @ [level]);
- mk_entry ts)
- end;
-
- val relatives =
- filter (fn s => s mem wanted_theories) (parents_of_name tname);
- in mk_entry relatives end;
- in if is_some (!cur_htmlfile) then
- (TextIO.closeOut (the (!cur_htmlfile));
- warning "Last theory's HTML file has not been closed.")
- else ();
- cur_htmlfile := Some (TextIO.openOut (tack_on tpath ("." ^ tname ^ ".html")));
- cur_has_title := false;
- TextIO.output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
-
- mk_charthead sup_out tname "Ancestors" true gif_path rel_index_path
- package;
- TextIO.output(sup_out,
- "" ^ tname ^ " \
- \\n");
- list_ancestors tname 0 [];
- TextIO.output (sup_out, "
");
- TextIO.closeOut sup_out;
-
- mk_charthead sub_out tname "Children" false gif_path rel_index_path
- package;
- TextIO.output(sub_out,
- "" ^ tname ^ " \
- \\n");
- TextIO.closeOut sub_out
- end;
-
-(*Invoke every put method stored in a theory's methods table to initialize
- the state of user defined variables*)
-fun put_thydata first tname =
- let val (methods, data) =
- case get_thyinfo tname of
- Some (ThyInfo {methods, data, ...}) =>
- (methods, Symtab.dest ((if first then fst else snd) data))
- | None => error ("Theory " ^ tname ^ " not stored by loader");
-
- fun put_data (id, date) =
- case Symtab.lookup (methods, id) of
- Some (ThyMethods {put, ...}) => put date
- | None => error ("No method defined for theory data \"" ^
- id ^ "\"");
- in seq put_data data end;
-
-val set_current_thy = put_thydata false;
(*Read .thy and .ML files that haven't been read yet or have changed since
they were last read;
@@ -675,61 +277,6 @@
!loaded_thys)
end;
- (*Add theory to file listing all loaded theories (for index.html)
- and to the sub-charts of its parents*)
- local exception MK_HTML in
- fun mk_html () =
- let val new_parents = parents_of_name tname \\ old_parents;
-
- fun robust_seq (proc: 'a -> unit) : 'a list -> unit =
- let fun seqf [] = ()
- | seqf (x :: xs) = (proc x handle _ => (); seqf xs)
- in seqf end;
-
- (*Add child to parents' sub-theory charts*)
- fun add_to_parents t =
- let val path = if t = "Pure" orelse t = "CPure" then
- (the (!pure_subchart))
- else path_of t;
-
- val gif_path = relative_path path (!gif_path);
- val rel_path = relative_path path abs_path;
- val tpath = tack_on rel_path ("." ^ tname);
-
- val fname = tack_on path ("." ^ t ^ "_sub.html");
- val out = if file_exists fname then
- TextIO.openAppend fname handle e =>
- (warning ("Unable to write to file " ^
- fname); raise e)
- else raise MK_HTML;
- in TextIO.output (out,
- " |\n \\__" ^ tname ^
- " \
- \\
- \\
- \\n");
- TextIO.closeOut out
- end;
-
- val theory_list =
- TextIO.openAppend (tack_on (!index_path) ".theory_list.txt")
- handle _ => (make_html := false;
- warning ("Cannot write to " ^
- (!index_path) ^ " while making HTML files.\n\
- \HTML generation has been switched off.\n\
- \Call init_html() from within a \
- \writeable directory to reactivate it.");
- raise MK_HTML)
- in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n");
- TextIO.closeOut theory_list;
-
- robust_seq add_to_parents new_parents
- end
- end;
-
(*Make sure that loaded_thys contains an entry for tname*)
fun init_thyinfo () =
let val tinfo = ThyInfo {path = "", children = [], parents = [],
@@ -767,8 +314,7 @@
if not (!delete_tmpfiles) then ()
else OS.FileSys.remove (out_name tname);
- if not (!make_html) then ()
- else thyfile2html abs_path tname
+ thyfile2html tname abs_path
);
set_info tname (Some (file_info thy_file)) None;
@@ -785,13 +331,18 @@
(*Add theory to list of all loaded theories (for index.html)
and add it to its parents' sub-charts*)
- if !make_html then
- let val path = path_of tname;
- in if path = "" then (*first time theory has been read*)
- (mk_html() handle MK_HTML => ())
- else ()
- end
- else ();
+ let val path = path_of tname;
+ in if path = "" then (*first time theory has been read*)
+ (
+ (*Add theory to list of all loaded theories (for index.html)
+ and add it to its parents' sub-charts*)
+ mk_html tname abs_path old_parents;
+
+ (*Add theory to graph definition file*)
+ mk_graph tname abs_path
+ )
+ else ()
+ end;
(*Now set the correct info*)
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
@@ -801,22 +352,21 @@
mark_children tname;
(*Close HTML file*)
- case !cur_htmlfile of
- Some out => (TextIO.output (out, "