# HG changeset patch # User wenzelm # Date 921059633 -3600 # Node ID b995ab76811795ead6f13bc8e01e948da14baf74 # Parent bf0d22535e47e3299e60df9d07a76999fd960633 maintain current/parent index; removed junk; diff -r bf0d22535e47 -r b995ab768117 src/Pure/Thy/browser_info.ML --- a/src/Pure/Thy/browser_info.ML Wed Mar 10 10:53:02 1999 +0100 +++ b/src/Pure/Thy/browser_info.ML Wed Mar 10 10:53:53 1999 +0100 @@ -5,10 +5,9 @@ Theory browsing information (HTML and graph files). TODO: - - Contents: theories, sessions; + - href parent theories (this vs. ancestor session!?); + - check 'README'; - symlink ".parent", ".top" (URLs!?); - - extend parent index: maintain "" marker (!?); - - proper handling of out of context theorems / sections (!?); - usedir: exclude arrow gifs; *) @@ -20,7 +19,7 @@ signature BROWSER_INFO = sig include BASIC_BROWSER_INFO - val init: bool -> string -> string list -> string -> string -> unit + val init: bool -> string list -> string list -> string list -> string -> unit val finish: unit -> unit val theory_source: string -> (string, 'a) Source.source -> unit val begin_theory: string -> string list -> (Path.T * bool) list -> unit @@ -72,6 +71,9 @@ | Some info => (Symtab.update ((name, map_theory_info f info), theories), index))); +fun add_index txt = change_browser_info (fn (theories, index) => + (theories, Buffer.add txt index)); + fun add_source name txt = change_theory_info name (fn (source, html, graph) => (Buffer.add txt source, html, graph)); @@ -90,22 +92,25 @@ val output_path = Path.variable "ISABELLE_BROWSER_INFO"; fun top_path sess_path = Path.append (Path.appends (replicate (length sess_path) Path.parent)); -val parent_path = Path.append Path.parent; val html_ext = Path.ext "html"; val html_path = html_ext o Path.basic; val graph_path = Path.ext "graph" o Path.basic; val index_path = Path.basic "index.html"; +val session_path = Path.basic ".session"; +val session_entries_path = Path.unpack ".session/entries"; +val pre_index_path = Path.unpack ".session/pre-index"; + (* session_info *) type session_info = - {session: string, path: string list, parent: string, name: string, + {parent: string, session: string, path: string list, name: string, html_prefix: Path.T, graph_prefix: Path.T}; -fun make_session_info (session, path, parent, name, html_prefix, graph_prefix) = - {session = session, path = path, parent = parent, name = name, +fun make_session_info (parent, session, path, name, html_prefix, graph_prefix) = + {parent = parent, session = session, path = path, name = name, html_prefix = html_prefix, graph_prefix = graph_prefix}: session_info; val session_info = ref (None: session_info option); @@ -114,45 +119,87 @@ fun conditional f = (case ! session_info of None => () | Some info => f info); + +(** HTML output **) + + +(* maintain index *) + +val session_entries = + HTML.session_entries o map (fn name => (Path.append (Path.basic name) index_path, name)); + +fun get_entries dir = + split_lines (File.read (Path.append dir session_entries_path)); + +fun put_entries entries dir = + File.write (Path.append dir session_entries_path) (cat_lines entries); + + +fun create_index dir = + File.read (Path.append dir pre_index_path) ^ + session_entries (get_entries dir) ^ HTML.end_index + |> File.write (Path.append dir index_path); + +fun update_index dir name = + (case try get_entries dir of + None => () + | Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir)); + + (* init session *) +fun name_of_session ids = space_implode "/" ("Isabelle" :: tl ids); + fun init false _ _ _ _ = (browser_info := empty_browser_info; session_info := None) - | init true session path parent name = + | init true parent session path name = let + val parent_name = name_of_session parent; + val session_name = name_of_session session; + val sess_prefix = Path.make path; + val out_path = Path.expand output_path; - val sess_prefix = Path.make path; val html_prefix = Path.append out_path sess_prefix; val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix]; in File.mkdir html_prefix; File.mkdir graph_prefix; + File.mkdir (Path.append html_prefix session_path); + File.write (Path.append html_prefix session_entries_path) ""; + session_info := Some (make_session_info (parent_name, session_name, path, name, + html_prefix, graph_prefix)); browser_info := empty_browser_info; - session_info := - Some (make_session_info (session, path, parent, name, html_prefix, graph_prefix)) + add_index (* FIXME 'README' *) + (HTML.begin_index (Path.append Path.parent index_path, parent_name) (index_path, session_name) None) end; (* finish session *) -fun finish_node html_prefix graph_prefix (name, {source = _, html, graph}) = - (Buffer.write (Path.append html_prefix (html_path name)) (Buffer.add HTML.conclude_theory html); - Buffer.write (Path.append graph_prefix (graph_path name)) graph); +fun finish () = conditional (fn {html_prefix, graph_prefix, name, ...} => + let + val {theories, index} = ! browser_info; -fun finish () = conditional (fn {html_prefix, graph_prefix, ...} => - let val {theories, index} = ! browser_info in - seq (finish_node html_prefix graph_prefix) (Symtab.dest theories); - Buffer.write (Path.append html_prefix index_path) index; + fun finish_node (a, {source = _, html, graph}) = + (Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html); + Buffer.write (Path.append graph_prefix (graph_path a)) graph); + in + seq finish_node (Symtab.dest theories); + Buffer.write (Path.append html_prefix pre_index_path) index; + create_index html_prefix; + update_index (Path.append html_prefix Path.parent) name; browser_info := empty_browser_info; session_info := None end); - -(** HTML output **) +(* theory elements *) fun theory_source name src = conditional (fn _ => (init_theory_info name empty_theory_info; add_source name (HTML.source src))); + +(* FIXME clean *) + fun begin_theory name parents orig_files = conditional (fn {session, html_prefix, ...} => let val ml_path = ThyLoad.ml_path name; @@ -175,10 +222,11 @@ in (Buffer.empty, Buffer.add txt html, graph) end; in seq (prep_file o #1) files; - change_theory_info name prep_source + change_theory_info name prep_source; + add_index (HTML.theory_entry (html_path name, name)) end); -fun end_theory name = conditional (fn _ => add_html name HTML.end_theory); +fun end_theory _ = (); fun theorem name thm = conditional (fn _ => in_context add_html (HTML.theorem name thm)); fun section s = conditional (fn _ => in_context add_html (HTML.section s)); @@ -205,61 +253,6 @@ (if not repeats then "" else "
... stands for repeated subtrees") ^ "

\nBack to " ^ parent ^ "\n


\n"; -(* FIXME "
"  *)
-
-
-(* theory_file *)
-
-(*convert .thy file to HTML and make chart of its super-theories*)
-
-(* FIXME include ML file (!?!?) *)
-
-    (* path of directory, where corresponding HTML file is stored *)
-    val tpath = html_path thy_path;
-
-    (* gif directory *)
-    val rel_gif_path = relative_path tpath (gif_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, {thy_time, ...}: thy_info) :: 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)) [] [];
-
-
-fun file_name path = "" ^ Path.pack src_path ^ "";
-
-fun ml_file src_path = conditional (fn () =>
-  (case ThyLoad.check_file src_path of
-    None => file_name src_path
-  | Some (path, _) =>
-      let
-        val base_path = Path.base path;
-        val html_base_path = html_ext base_path;
-        val name = Path.pack base_path;
-        val txt = implode (html_escape (explode (File.read path)));
-        val html_txt =
-          "" ^ name ^ "\n\n\n" ^
-          "

File " ^ name ^ "

\n
\n\n
\n" ^ txt ^ "

"; - in - File.write (output_path html_base_path) html_text; - "" ^ file_name src_path ^ "" - "file " ^ Path.pack src_path ^ "" - - -fun theory_header name parents files = - FIXME; - - - fun theory_file name text = conditional (fn () => let