maintain current/parent index;
authorwenzelm
Wed Mar 10 10:53:53 1999 +0100 (1999-03-10)
changeset 6339b995ab768117
parent 6338 bf0d22535e47
child 6340 7d5cbd5819a0
maintain current/parent index;
removed junk;
src/Pure/Thy/browser_info.ML
     1.1 --- a/src/Pure/Thy/browser_info.ML	Wed Mar 10 10:53:02 1999 +0100
     1.2 +++ b/src/Pure/Thy/browser_info.ML	Wed Mar 10 10:53:53 1999 +0100
     1.3 @@ -5,10 +5,9 @@
     1.4  Theory browsing information (HTML and graph files).
     1.5  
     1.6  TODO:
     1.7 -  - Contents: theories, sessions;
     1.8 +  - href parent theories (this vs. ancestor session!?);
     1.9 +  - check 'README';
    1.10    - symlink ".parent", ".top" (URLs!?);
    1.11 -  - extend parent index: maintain "<!--insert--here-->" marker (!?);
    1.12 -  - proper handling of out of context theorems / sections (!?);
    1.13    - usedir: exclude arrow gifs;
    1.14  *)
    1.15  
    1.16 @@ -20,7 +19,7 @@
    1.17  signature BROWSER_INFO =
    1.18  sig
    1.19    include BASIC_BROWSER_INFO
    1.20 -  val init: bool -> string -> string list -> string -> string -> unit
    1.21 +  val init: bool -> string list -> string list -> string list -> string -> unit
    1.22    val finish: unit -> unit
    1.23    val theory_source: string -> (string, 'a) Source.source -> unit
    1.24    val begin_theory: string -> string list -> (Path.T * bool) list -> unit
    1.25 @@ -72,6 +71,9 @@
    1.26    | Some info => (Symtab.update ((name, map_theory_info f info), theories), index)));
    1.27  
    1.28  
    1.29 +fun add_index txt = change_browser_info (fn (theories, index) =>
    1.30 +  (theories, Buffer.add txt index));
    1.31 +
    1.32  fun add_source name txt = change_theory_info name (fn (source, html, graph) =>
    1.33    (Buffer.add txt source, html, graph));
    1.34  
    1.35 @@ -90,22 +92,25 @@
    1.36  val output_path = Path.variable "ISABELLE_BROWSER_INFO";
    1.37  
    1.38  fun top_path sess_path = Path.append (Path.appends (replicate (length sess_path) Path.parent));
    1.39 -val parent_path = Path.append Path.parent;
    1.40  
    1.41  val html_ext = Path.ext "html";
    1.42  val html_path = html_ext o Path.basic;
    1.43  val graph_path = Path.ext "graph" o Path.basic;
    1.44  val index_path = Path.basic "index.html";
    1.45  
    1.46 +val session_path = Path.basic ".session";
    1.47 +val session_entries_path = Path.unpack ".session/entries";
    1.48 +val pre_index_path = Path.unpack ".session/pre-index";
    1.49 +
    1.50  
    1.51  (* session_info *)
    1.52  
    1.53  type session_info =
    1.54 -  {session: string, path: string list, parent: string, name: string,
    1.55 +  {parent: string, session: string, path: string list, name: string,
    1.56      html_prefix: Path.T, graph_prefix: Path.T};
    1.57  
    1.58 -fun make_session_info (session, path, parent, name, html_prefix, graph_prefix) =
    1.59 -  {session = session, path = path, parent = parent, name = name,
    1.60 +fun make_session_info (parent, session, path, name, html_prefix, graph_prefix) =
    1.61 +  {parent = parent, session = session, path = path, name = name,
    1.62      html_prefix = html_prefix, graph_prefix = graph_prefix}: session_info;
    1.63  
    1.64  val session_info = ref (None: session_info option);
    1.65 @@ -114,45 +119,87 @@
    1.66  fun conditional f = (case ! session_info of None => () | Some info => f info);
    1.67  
    1.68  
    1.69 +
    1.70 +(** HTML output **)
    1.71 +
    1.72 +
    1.73 +(* maintain index *)
    1.74 +
    1.75 +val session_entries =
    1.76 +  HTML.session_entries o map (fn name => (Path.append (Path.basic name) index_path, name));
    1.77 +
    1.78 +fun get_entries dir =
    1.79 +  split_lines (File.read (Path.append dir session_entries_path));
    1.80 +
    1.81 +fun put_entries entries dir =
    1.82 +  File.write (Path.append dir session_entries_path) (cat_lines entries);
    1.83 +
    1.84 +
    1.85 +fun create_index dir =
    1.86 +  File.read (Path.append dir pre_index_path) ^
    1.87 +    session_entries (get_entries dir) ^ HTML.end_index
    1.88 +  |> File.write (Path.append dir index_path);
    1.89 +
    1.90 +fun update_index dir name =
    1.91 +  (case try get_entries dir of
    1.92 +    None => ()
    1.93 +  | Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir));
    1.94 +  
    1.95 +
    1.96  (* init session *)
    1.97  
    1.98 +fun name_of_session ids = space_implode "/" ("Isabelle" :: tl ids);
    1.99 +
   1.100  fun init false _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
   1.101 -  | init true session path parent name =
   1.102 +  | init true parent session path name =
   1.103        let
   1.104 +        val parent_name = name_of_session parent;
   1.105 +        val session_name = name_of_session session;
   1.106 +        val sess_prefix = Path.make path;
   1.107 +
   1.108          val out_path = Path.expand output_path;
   1.109 -        val sess_prefix = Path.make path;
   1.110          val html_prefix = Path.append out_path sess_prefix;
   1.111          val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix];
   1.112        in
   1.113          File.mkdir html_prefix;
   1.114          File.mkdir graph_prefix;
   1.115 +        File.mkdir (Path.append html_prefix session_path);
   1.116 +        File.write (Path.append html_prefix session_entries_path) "";
   1.117 +        session_info := Some (make_session_info (parent_name, session_name, path, name,
   1.118 +          html_prefix, graph_prefix));
   1.119          browser_info := empty_browser_info;
   1.120 -        session_info :=
   1.121 -          Some (make_session_info (session, path, parent, name, html_prefix, graph_prefix))
   1.122 +        add_index							(* FIXME 'README' *)
   1.123 +          (HTML.begin_index (Path.append Path.parent index_path, parent_name) (index_path, session_name) None)
   1.124        end;
   1.125  
   1.126  
   1.127  (* finish session *)
   1.128  
   1.129 -fun finish_node html_prefix graph_prefix (name, {source = _, html, graph}) =
   1.130 - (Buffer.write (Path.append html_prefix (html_path name)) (Buffer.add HTML.conclude_theory html);
   1.131 -  Buffer.write (Path.append graph_prefix (graph_path name)) graph);
   1.132 +fun finish () = conditional (fn {html_prefix, graph_prefix, name, ...} =>
   1.133 +  let
   1.134 +    val {theories, index} = ! browser_info;
   1.135  
   1.136 -fun finish () = conditional (fn {html_prefix, graph_prefix, ...} =>
   1.137 -  let val {theories, index} = ! browser_info in
   1.138 -    seq (finish_node html_prefix graph_prefix) (Symtab.dest theories);
   1.139 -    Buffer.write (Path.append html_prefix index_path) index;
   1.140 +    fun finish_node (a, {source = _, html, graph}) =
   1.141 +      (Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html);
   1.142 +        Buffer.write (Path.append graph_prefix (graph_path a)) graph);
   1.143 +  in
   1.144 +    seq finish_node (Symtab.dest theories);
   1.145 +    Buffer.write (Path.append html_prefix pre_index_path) index;
   1.146 +    create_index html_prefix;
   1.147 +    update_index (Path.append html_prefix Path.parent) name;
   1.148      browser_info := empty_browser_info;
   1.149      session_info := None
   1.150    end);
   1.151  
   1.152  
   1.153 -
   1.154 -(** HTML output **)
   1.155 +(* theory elements *)
   1.156  
   1.157  fun theory_source name src = conditional (fn _ =>
   1.158    (init_theory_info name empty_theory_info; add_source name (HTML.source src)));
   1.159  
   1.160 +
   1.161 +(* FIXME clean *)
   1.162 +
   1.163  fun begin_theory name parents orig_files = conditional (fn {session, html_prefix, ...} =>
   1.164    let
   1.165      val ml_path = ThyLoad.ml_path name;
   1.166 @@ -175,10 +222,11 @@
   1.167          in (Buffer.empty, Buffer.add txt html, graph) end;
   1.168    in
   1.169      seq (prep_file o #1) files;
   1.170 -    change_theory_info name prep_source
   1.171 +    change_theory_info name prep_source;
   1.172 +    add_index (HTML.theory_entry (html_path name, name))
   1.173    end);
   1.174  
   1.175 -fun end_theory name = conditional (fn _ => add_html name HTML.end_theory);
   1.176 +fun end_theory _ = ();
   1.177  
   1.178  fun theorem name thm = conditional (fn _ => in_context add_html (HTML.theorem name thm));
   1.179  fun section s = conditional (fn _ => in_context add_html (HTML.section s));
   1.180 @@ -205,61 +253,6 @@
   1.181    (if not repeats then "" else "<br><tt>...</tt> stands for repeated subtrees") ^
   1.182    "<p>\n<a href=" ^ htmlify index_path ^ ">Back</a> to " ^ parent ^ "\n<hr>\n";
   1.183  
   1.184 -(* FIXME "<pre>"  *)
   1.185 -
   1.186 -
   1.187 -(* theory_file *)
   1.188 -
   1.189 -(*convert .thy file to HTML and make chart of its super-theories*)
   1.190 -
   1.191 -(* FIXME include ML file (!?!?) *)
   1.192 -
   1.193 -    (* path of directory, where corresponding HTML file is stored *)
   1.194 -    val tpath = html_path thy_path;
   1.195 -
   1.196 -    (* gif directory *)
   1.197 -    val rel_gif_path = relative_path tpath (gif_path ());
   1.198 -
   1.199 -    val rel_index_path = relative_path tpath (!index_path);
   1.200 -
   1.201 -    (*Make list of all theories and all theories that own a .thy file*)
   1.202 -    fun list_theories [] theories thy_files = (theories, thy_files)
   1.203 -      | list_theories ((tname, {thy_time, ...}: thy_info) :: ts)
   1.204 -                      theories thy_files =
   1.205 -          list_theories ts (tname :: theories)
   1.206 -            (if is_some thy_time andalso the thy_time <> "" then
   1.207 -               tname :: thy_files
   1.208 -             else thy_files);
   1.209 -
   1.210 -    val (theories, thy_files) =
   1.211 -      list_theories (Symtab.dest (!loaded_thys)) [] [];
   1.212 -
   1.213 -
   1.214 -fun file_name path = "<tt>" ^ Path.pack src_path ^ "</tt>";
   1.215 -
   1.216 -fun ml_file src_path = conditional (fn () =>
   1.217 -  (case ThyLoad.check_file src_path of
   1.218 -    None => file_name src_path
   1.219 -  | Some (path, _) =>
   1.220 -      let
   1.221 -        val base_path = Path.base path;
   1.222 -        val html_base_path = html_ext base_path;
   1.223 -        val name = Path.pack base_path;
   1.224 -        val txt = implode (html_escape (explode (File.read path)));
   1.225 -        val html_txt =
   1.226 -          "<html><head><title>" ^ name ^ "</title></head>\n\n<body>\n" ^
   1.227 -          "<h2>File " ^ name ^ "</h2>\n<hr>\n\n<pre>\n" ^ txt ^ "</pre><hr></body></html>";
   1.228 -      in
   1.229 -        File.write (output_path html_base_path) html_text;
   1.230 -        "<a href=" ^ htmlify html_base_path ^ ">" ^ file_name src_path ^ "</a>"
   1.231 -        "file <a href=" ^ "<tt>" ^ Path.pack src_path ^ "</tt>"
   1.232 -        
   1.233 -
   1.234 -fun theory_header name parents files =
   1.235 -  FIXME;
   1.236 -
   1.237 -
   1.238 -
   1.239  
   1.240  fun theory_file name text = conditional (fn () =>
   1.241    let