This file now contains all functions for generating html
authorberghofe
Wed Aug 06 00:24:49 1997 +0200 (1997-08-06)
changeset 36035eef2ff0eb72
parent 3602 cdfb8b7e60fa
child 3604 6bf9f09f3d61
This file now contains all functions for generating html
and graph data.
src/Pure/Thy/browser_info.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/browser_info.ML	Wed Aug 06 00:24:49 1997 +0200
     1.3 @@ -0,0 +1,787 @@
     1.4 +(*  Title:      Pure/Thy/thy_browser_info.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer and Carsten Clasohm
     1.7 +    Copyright   1994, 1997 TU Muenchen
     1.8 +
     1.9 +Functions for generating theory browsing information
    1.10 +(i.e. *.html and *.graph - files).
    1.11 +*)
    1.12 +
    1.13 +signature BROWSER_INFO =
    1.14 +sig
    1.15 +  val output_dir       : string ref
    1.16 +  val home_path        : string ref
    1.17 +
    1.18 +  val make_graph       : bool ref
    1.19 +  val init_graph       : string -> unit
    1.20 +  val mk_graph         : string -> string -> unit
    1.21 +  val cur_thyname      : string ref
    1.22 +  val make_html        : bool ref
    1.23 +  val mk_html          : string -> string -> string list -> unit
    1.24 +  val thyfile2html     : string -> string -> unit
    1.25 +  val init_html        : unit -> unit
    1.26 +  val finish_html      : unit -> unit
    1.27 +  val section          : string -> unit
    1.28 +  val thm_to_html      : thm -> string -> unit
    1.29 +  val close_html       : unit -> unit
    1.30 +end;
    1.31 +
    1.32 +
    1.33 +structure BrowserInfo : BROWSER_INFO =
    1.34 +struct
    1.35 +
    1.36 +open ThyInfo;
    1.37 +
    1.38 +
    1.39 +(*directory where to put html and graph files*)
    1.40 +val output_dir = ref "";
    1.41 +
    1.42 +
    1.43 +(*path of user home directory*)
    1.44 +val home_path = ref "";
    1.45 +
    1.46 +
    1.47 +(*normalize a path
    1.48 +  FIXME: move to library?*)
    1.49 +fun normalize_path p =
    1.50 +   let val curr_dir = pwd ();
    1.51 +       val _ = cd p;
    1.52 +       val norm_path = pwd ();
    1.53 +       val _ = cd curr_dir
    1.54 +   in norm_path end;
    1.55 +
    1.56 +
    1.57 +(*create directory
    1.58 +  FIXME: move to library?*)
    1.59 +fun mkdir path = (execute ("mkdir -p " ^ path) ; ());
    1.60 +
    1.61 +
    1.62 +(*Path of Isabelle's main (source) directory
    1.63 +  FIXME: this value should be provided by isatool!*)
    1.64 +val base_path = ref (
    1.65 +  "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ())))))));
    1.66 +
    1.67 +
    1.68 +(******************** HTML generation functions *************************)
    1.69 +
    1.70 +(*Set location of graphics for HTML files*)
    1.71 +fun gif_path () = tack_on (normalize_path (!output_dir)) "gif";
    1.72 +
    1.73 +
    1.74 +(*Name of theory currently being read*)
    1.75 +val cur_thyname = ref "";
    1.76 +
    1.77 +
    1.78 +(*Name of current logic*)
    1.79 +val package = ref "";
    1.80 +
    1.81 +
    1.82 +(* Return path of directory where to store html / graph data
    1.83 +   corresponding to theory with given path *)
    1.84 +local
    1.85 +  fun make_path q p =
    1.86 +    let val base  = tack_on (normalize_path (!output_dir)) q;
    1.87 +        val rpath = if p subdir_of (!base_path) then relative_path (!base_path) p
    1.88 +                    else relative_path (normalize_path (!home_path)) p;
    1.89 +    in tack_on base rpath end
    1.90 +in
    1.91 +  val html_path = make_path "html";
    1.92 +  val graph_path = make_path "graph"
    1.93 +end;
    1.94 +
    1.95 +
    1.96 +(*Location of theory-list.txt and index.html (set by init_html)*)
    1.97 +val index_path = ref "";
    1.98 +
    1.99 +
   1.100 +(*Original path of ROOT.ML*)
   1.101 +val original_path = ref "";
   1.102 +
   1.103 +
   1.104 +(*Location of Pure_sub.html and CPure_sub.html*)
   1.105 +val pure_subchart = ref (None : string option);
   1.106 +
   1.107 +
   1.108 +(*Controls whether HTML files should be generated*)
   1.109 +val make_html = ref false;
   1.110 +
   1.111 +
   1.112 +(*HTML file of theory currently being read
   1.113 +  (Initialized by thyfile2html; used by use_thy and store_thm)*)
   1.114 +val cur_htmlfile = ref None : TextIO.outstream option ref;
   1.115 +
   1.116 +
   1.117 +(*Boolean variable which indicates if the title "Theorems proved in foo.ML"
   1.118 +  has already been inserted into the current HTML file*)
   1.119 +val cur_has_title = ref false;
   1.120 +
   1.121 +
   1.122 +(*Make head of HTML dependency charts
   1.123 +  Parameters are:
   1.124 +    file: HTML file
   1.125 +    tname: theory name
   1.126 +    suffix: suffix of complementary chart
   1.127 +            (sup if this head is for a sub-chart, sub if it is for a sup-chart;
   1.128 +             empty for Pure and CPure sub-charts)
   1.129 +    gif_path: relative path to directory containing GIFs
   1.130 +    index_path: relative path to directory containing main theory chart
   1.131 +*)
   1.132 +fun mk_charthead file tname title repeats gif_path index_path package =
   1.133 +  TextIO.output (file,
   1.134 +   "<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^
   1.135 +   "</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^
   1.136 +   "</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^
   1.137 +   "<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
   1.138 +   \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
   1.139 +   \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
   1.140 +   \\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^
   1.141 +   (if not repeats then "" else
   1.142 +      "<BR><TT>...</TT> stands for repeated subtrees") ^
   1.143 +   "<P>\n<A HREF = \"" ^ tack_on index_path "index.html\
   1.144 +   \\">Back</A> to the index of " ^ package ^ "\n<HR>\n<PRE>");
   1.145 +
   1.146 +
   1.147 +(*Convert special HTML characters ('&', '>', and '<')*)
   1.148 +fun escape []       = []
   1.149 +  | escape ("<"::s) = "&lt;" :: escape s
   1.150 +  | escape (">"::s) = "&gt;" :: escape s
   1.151 +  | escape ("&"::s) = "&amp;" :: escape s
   1.152 +  | escape (c::s)   = c :: escape s;
   1.153 +
   1.154 +
   1.155 +(*Convert .thy file to HTML and make chart of its super-theories*)
   1.156 +fun thyfile2html tname thy_path = if not (!make_html) then () else
   1.157 +  let
   1.158 +    (* path of directory, where corresponding HTML file is stored *)
   1.159 +    val tpath = html_path thy_path;
   1.160 +
   1.161 +    (* gif directory *)
   1.162 +    val rel_gif_path = relative_path tpath (gif_path ());
   1.163 +
   1.164 +    val rel_index_path = relative_path tpath (!index_path);
   1.165 +
   1.166 +    (*Make list of all theories and all theories that own a .thy file*)
   1.167 +    fun list_theories [] theories thy_files = (theories, thy_files)
   1.168 +      | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)
   1.169 +                      theories thy_files =
   1.170 +          list_theories ts (tname :: theories)
   1.171 +            (if is_some thy_time andalso the thy_time <> "" then
   1.172 +               tname :: thy_files
   1.173 +             else thy_files);
   1.174 +
   1.175 +    val (theories, thy_files) =
   1.176 +      list_theories (Symtab.dest (!loaded_thys)) [] [];
   1.177 +
   1.178 +    (*convert ML file to html *)
   1.179 +    fun ml2html name abs_path =
   1.180 +      let val is  = TextIO.openIn (tack_on abs_path (name ^ ".ML"));
   1.181 +          val inp = implode (escape (explode (TextIO.inputAll is)));
   1.182 +          val _   = TextIO.closeIn is;
   1.183 +          val os  = TextIO.openOut (tack_on (html_path abs_path) (name ^ "_ML.html"));
   1.184 +          val _   = TextIO.output (os,
   1.185 +            "<HTML><HEAD><TITLE>" ^ name ^ ".ML</TITLE></HEAD>\n\n<BODY>\n" ^
   1.186 +            "<H2>" ^ name ^ ".ML</H2>\n<A HREF = \"" ^
   1.187 +            name ^ ".html\">Back</A> to theory " ^ name ^
   1.188 +            "\n<HR>\n\n<PRE>\n" ^ inp ^ "</PRE><HR></BODY></HTML>");
   1.189 +          val _   = TextIO.closeOut os;
   1.190 +     in () end;
   1.191 +
   1.192 +    (*Do the conversion*)
   1.193 +    fun gettext thy_file  =
   1.194 +      let
   1.195 +        (*Convert special HTML characters ('&', '>', and '<')*)
   1.196 +        val file =
   1.197 +          let val is  = TextIO.openIn thy_file;
   1.198 +              val inp = TextIO.inputAll is;
   1.199 +          in (TextIO.closeIn is; escape (explode inp)) end;
   1.200 +
   1.201 +
   1.202 +        (*Isolate first (possibly nested) comment;
   1.203 +          skip all leading whitespaces*)
   1.204 +        val (comment, file') =
   1.205 +          let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs)
   1.206 +                | first_comment ("*" :: ")" :: cs) co d =
   1.207 +                    first_comment cs (co ^ "*)") (d-1)
   1.208 +                | first_comment ("(" :: "*" :: cs) co d =
   1.209 +                    first_comment cs (co ^ "(*") (d+1)
   1.210 +                | first_comment (" "  :: cs) "" 0 = first_comment cs "" 0
   1.211 +                | first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0
   1.212 +                | first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0
   1.213 +                | first_comment cs           "" 0 = ("", cs)
   1.214 +                | first_comment (c :: cs) co d =
   1.215 +                    first_comment cs (co ^ implode [c]) d
   1.216 +                | first_comment [] co _ =
   1.217 +                    error ("Unexpected end of file " ^ tname ^ ".thy.");
   1.218 +          in first_comment file "" 0 end;
   1.219 +
   1.220 +        (*Process line defining theory's ancestors;
   1.221 +          convert valid theory names to links to their HTML file*)
   1.222 +        val (ancestors, body) =
   1.223 +          let
   1.224 +            fun make_links l result =
   1.225 +              let val (pre, letter) = take_prefix (not o is_letter) l;
   1.226 +
   1.227 +                  val (id, rest) =
   1.228 +                    take_prefix (is_quasi_letter orf is_digit) letter;
   1.229 +
   1.230 +                  val id = implode id;
   1.231 +
   1.232 +                  (*Make a HTML link out of a theory name*)
   1.233 +                  fun make_link t =
   1.234 +                    let val path = html_path (path_of t);
   1.235 +                    in "<A HREF = \"" ^
   1.236 +                       tack_on (relative_path tpath path) t ^
   1.237 +                       ".html\">" ^ t ^ "</A>" end;
   1.238 +              in if not (id mem theories) then (result, implode l)
   1.239 +                 else if id mem thy_files then
   1.240 +                   make_links rest (result ^ implode pre ^ make_link id)
   1.241 +                 else make_links rest (result ^ implode pre ^ id)
   1.242 +              end;
   1.243 +
   1.244 +            val (pre, rest) = take_prefix (fn c => c <> "=") file';
   1.245 +
   1.246 +            val (ancestors, body) =
   1.247 +              if null rest then
   1.248 +                error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\
   1.249 +                       \(Make sure that the last line ends with a linebreak.)")
   1.250 +              else
   1.251 +                make_links rest "";
   1.252 +          in (implode pre ^ ancestors, body) end;
   1.253 +      in "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^
   1.254 +         "<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^
   1.255 +         tack_on rel_index_path "index.html\
   1.256 +         \\">Back</A> to the index of " ^ (!package) ^
   1.257 +         "\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^
   1.258 +         "</PRE>\n"
   1.259 +      end;
   1.260 +
   1.261 +    (** Make chart of super-theories **)
   1.262 +
   1.263 +    val _ = mkdir tpath;
   1.264 +    val sup_out = TextIO.openOut (tack_on tpath (tname ^ "_sup.html"));
   1.265 +    val sub_out = TextIO.openOut (tack_on tpath (tname ^ "_sub.html"));
   1.266 +
   1.267 +    (*Theories that already have been listed in this chart*)
   1.268 +    val listed = ref [];
   1.269 +
   1.270 +    val wanted_theories =
   1.271 +      filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure")
   1.272 +             theories;
   1.273 +
   1.274 +    (*Make tree of theory dependencies*)
   1.275 +    fun list_ancestors tname level continued =
   1.276 +      let
   1.277 +        fun mk_entry [] = ()
   1.278 +          | mk_entry (t::ts) =
   1.279 +            let
   1.280 +              val is_pure = t = "Pure" orelse t = "CPure";
   1.281 +              val path = if is_pure then (the (!pure_subchart))
   1.282 +                         else html_path (path_of t);
   1.283 +              val rel_path = relative_path tpath path;
   1.284 +              val repeated = t mem (!listed) andalso
   1.285 +                             not (null (parents_of_name t));
   1.286 +
   1.287 +              fun mk_offset [] cur =
   1.288 +                    if level < cur then error "Error in mk_offset"
   1.289 +                    else implode (replicate (level - cur) "    ")
   1.290 +                | mk_offset (l::ls) cur =
   1.291 +                    implode (replicate (l - cur) "    ") ^ "|   " ^
   1.292 +                    mk_offset ls (l+1);
   1.293 +            in TextIO.output (sup_out,
   1.294 +                 " " ^ mk_offset continued 0 ^
   1.295 +                 "\\__" ^ (if is_pure then t else
   1.296 +                             "<A HREF=\"" ^ tack_on rel_path t ^
   1.297 +                             ".html\">" ^ t ^ "</A>") ^
   1.298 +                 (if repeated then "..." else " ") ^
   1.299 +                 "<A HREF = \"" ^ tack_on rel_path t ^
   1.300 +                 "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   1.301 +                 tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>" ^
   1.302 +                 (if is_pure then ""
   1.303 +                  else "<A HREF = \"" ^ tack_on rel_path t ^
   1.304 +                       "_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   1.305 +                       tack_on rel_gif_path "blue_arrow.gif\
   1.306 +                       \\" ALT = /\\></A>") ^
   1.307 +                 "\n");
   1.308 +              if repeated then ()
   1.309 +              else (listed := t :: (!listed);
   1.310 +                    list_ancestors t (level+1) (if null ts then continued
   1.311 +                                                else continued @ [level]);
   1.312 +                    mk_entry ts)
   1.313 +            end;
   1.314 +
   1.315 +        val relatives =
   1.316 +          filter (fn s => s mem wanted_theories) (parents_of_name tname);
   1.317 +      in mk_entry relatives end;
   1.318 +  in if is_some (!cur_htmlfile) then
   1.319 +       (TextIO.closeOut (the (!cur_htmlfile));
   1.320 +        warning "Last theory's HTML file has not been closed.")
   1.321 +     else ();
   1.322 +     cur_htmlfile := Some (TextIO.openOut (tack_on tpath (tname ^ ".html")));
   1.323 +     cur_has_title := false;
   1.324 +     if file_exists (tack_on thy_path (tname ^ ".ML")) 
   1.325 +       then ml2html tname thy_path else ();
   1.326 +     TextIO.output (the (!cur_htmlfile), gettext (tack_on thy_path tname ^ ".thy"));
   1.327 +
   1.328 +     mk_charthead sup_out tname "Ancestors" true rel_gif_path rel_index_path
   1.329 +                  (!package);
   1.330 +     TextIO.output(sup_out,
   1.331 +       "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
   1.332 +       \<A HREF = \"" ^ tname ^
   1.333 +       "_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   1.334 +       tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>\n");
   1.335 +     list_ancestors tname 0 [];
   1.336 +     TextIO.output (sup_out, "</PRE><HR></BODY></HTML>");
   1.337 +     TextIO.closeOut sup_out;
   1.338 +
   1.339 +     mk_charthead sub_out tname "Children" false rel_gif_path rel_index_path
   1.340 +                  (!package);
   1.341 +     TextIO.output(sub_out,
   1.342 +       "<A HREF=\"" ^ tname ^ ".html\">" ^ tname ^ "</A> \
   1.343 +       \<A HREF = \"" ^ tname ^ "_sup.html\"><IMG SRC = \"" ^
   1.344 +       tack_on rel_gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n");
   1.345 +     TextIO.closeOut sub_out
   1.346 +  end;
   1.347 +
   1.348 +
   1.349 +(*Makes HTML title for list of theorems; as this list may be empty and we
   1.350 +  don't want a title in that case, mk_theorems_title is only invoked when
   1.351 +  something is added to the list*)
   1.352 +fun mk_theorems_title out =
   1.353 +  if not (!cur_has_title) then
   1.354 +    (cur_has_title := true;
   1.355 +     TextIO.output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^
   1.356 +                  (!cur_thyname) ^ "_ML.html\">" ^ (!cur_thyname) ^
   1.357 +                  ".ML</A>:</H2>\n"))
   1.358 +  else ();
   1.359 +
   1.360 +
   1.361 +exception MK_HTML;
   1.362 +
   1.363 +(*Add theory to file listing all loaded theories (for index.html)
   1.364 +  and to the sub-charts of its parents*)
   1.365 +fun mk_html tname abs_path old_parents = if not (!make_html) then () else
   1.366 +  ( let val new_parents = parents_of_name tname \\ old_parents;
   1.367 +
   1.368 +        fun robust_seq (proc: 'a -> unit) : 'a list -> unit =
   1.369 +          let fun seqf [] = ()
   1.370 +                | seqf (x :: xs) = (proc x  handle _ => (); seqf xs)
   1.371 +          in seqf end;
   1.372 +
   1.373 +        (*Add child to parents' sub-theory charts*)
   1.374 +        fun add_to_parents t =
   1.375 +          let val path = if t = "Pure" orelse t = "CPure" then
   1.376 +                           (the (!pure_subchart))
   1.377 +                         else html_path (path_of t);
   1.378 + 
   1.379 +              val rel_gif_path = relative_path path (gif_path ());
   1.380 +              val rel_path = relative_path path (html_path abs_path);
   1.381 +              val tpath = tack_on rel_path tname;
   1.382 +
   1.383 +              val fname = tack_on path (t ^ "_sub.html");
   1.384 +              val out = if file_exists fname then
   1.385 +                          TextIO.openAppend fname  handle e  =>
   1.386 +                            (warning ("Unable to write to file " ^
   1.387 +                                      fname); raise e)
   1.388 +                        else raise MK_HTML;
   1.389 +          in TextIO.output (out,
   1.390 +               " |\n \\__<A HREF=\"" ^
   1.391 +               tack_on rel_path tname ^ ".html\">" ^ tname ^
   1.392 +               "</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\
   1.393 +               \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   1.394 +               tack_on rel_gif_path "red_arrow.gif\" ALT = \\/></A>\
   1.395 +               \<A HREF = \"" ^ tpath ^ "_sup.html\">\
   1.396 +               \<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^
   1.397 +               tack_on rel_gif_path "blue_arrow.gif\" ALT = /\\></A>\n");
   1.398 +             TextIO.closeOut out
   1.399 +          end;
   1.400 + 
   1.401 +        val theory_list =
   1.402 +          TextIO.openAppend (tack_on (!index_path) "theory_list.txt")
   1.403 +            handle _ => (make_html := false;
   1.404 +                         warning ("Cannot write to " ^
   1.405 +                                (!index_path) ^ " while making HTML files.\n\
   1.406 +                                \HTML generation has been switched off.\n\
   1.407 +                                \Call init_html() from within a \
   1.408 +                                \writeable directory to reactivate it.");
   1.409 +                         raise MK_HTML)
   1.410 +    in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n");
   1.411 +       TextIO.closeOut theory_list; 
   1.412 +       robust_seq add_to_parents new_parents
   1.413 +    end
   1.414 +  ) handle MK_HTML => ();
   1.415 +
   1.416 +
   1.417 +(*** Misc HTML functions ***)
   1.418 +
   1.419 +(*Init HTML generator by setting paths and creating new files*)
   1.420 +fun init_html () =
   1.421 +  let val cwd = OS.FileSys.getDir();
   1.422 +      val _ = mkdir (html_path cwd);
   1.423 +
   1.424 +      val theory_list = TextIO.closeOut (TextIO.openOut (tack_on (html_path cwd) "theory_list.txt"));
   1.425 +
   1.426 +      val rel_gif_path = relative_path (html_path cwd) (gif_path ());
   1.427 +
   1.428 +      (*Make new HTML files for Pure and CPure*)
   1.429 +      fun init_pure_html () =
   1.430 +        let val pure_out = TextIO.openOut (tack_on (html_path cwd) "Pure_sub.html");
   1.431 +            val cpure_out = TextIO.openOut (tack_on (html_path cwd) "CPure_sub.html");
   1.432 +        in mk_charthead pure_out "Pure" "Children" false rel_gif_path ""
   1.433 +                        (!package);
   1.434 +           mk_charthead cpure_out "CPure" "Children" false rel_gif_path ""
   1.435 +                        (!package);
   1.436 +           TextIO.output (pure_out, "Pure\n");
   1.437 +           TextIO.output (cpure_out, "CPure\n");
   1.438 +           TextIO.closeOut pure_out;
   1.439 +           TextIO.closeOut cpure_out;
   1.440 +           pure_subchart := Some (html_path cwd)
   1.441 +        end;
   1.442 +
   1.443 +      (*Copy files
   1.444 +        FIXME: move to library?*)
   1.445 +      fun copy_file infile outfile = if not (file_exists infile) then () else
   1.446 +        let val is = TextIO.openIn infile;
   1.447 +            val inp = TextIO.inputAll is;
   1.448 +            val _ = TextIO.closeIn is;
   1.449 +            val os = TextIO.openOut outfile;
   1.450 +            val _ = TextIO.output (os, inp);
   1.451 +            val _ = TextIO.closeOut os
   1.452 +        in () end
   1.453 +
   1.454 +  in make_html := true;
   1.455 +     (*Make sure that base_path contains the physical path and no
   1.456 +       symbolic links*)
   1.457 +     base_path := normalize_path (!base_path);
   1.458 +     original_path := cwd;
   1.459 +     index_path := html_path cwd;
   1.460 +     package :=
   1.461 +        (if cwd subdir_of (!base_path) then
   1.462 +          relative_path (!base_path) cwd
   1.463 +         else base_name cwd);
   1.464 +
   1.465 +     (*Copy README files to html directory
   1.466 +       FIXME: let usedir do this job*)
   1.467 +     copy_file (tack_on cwd "README.html") (tack_on (!index_path) "README.html");
   1.468 +     copy_file (tack_on cwd "README") (tack_on (!index_path) "README");
   1.469 +
   1.470 +     if cwd subdir_of (!base_path) then ()
   1.471 +     else warning "The current working directory seems to be no \
   1.472 +                  \subdirectory of\nIsabelle's main directory. \
   1.473 +                  \Please ensure that base_path's value is correct.\n";
   1.474 +
   1.475 +     writeln ("Setting path for index.html to " ^ quote (!index_path) ^
   1.476 +              "\nGIF path has been set to " ^ quote (gif_path ()));
   1.477 +
   1.478 +     if is_none (!pure_subchart) then init_pure_html()
   1.479 +     else ()
   1.480 +  end;
   1.481 +
   1.482 +
   1.483 +(*Generate index.html*)
   1.484 +fun finish_html () = if not (!make_html) then () else
   1.485 +  let val tlist_path = tack_on (!index_path) "theory_list.txt";
   1.486 +      val theory_list = TextIO.openIn tlist_path;
   1.487 +      val theories = space_explode "\n" (TextIO.inputAll theory_list);
   1.488 +      val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path);
   1.489 +
   1.490 +      val rel_gif_path = relative_path (!index_path) (gif_path ());
   1.491 +
   1.492 +      (*Make entry for main chart of all theories.*)
   1.493 +      fun main_entry t =
   1.494 +        let
   1.495 +          val (name, path) = take_prefix (not_equal " ") (explode t);
   1.496 +
   1.497 +          val tname = implode name
   1.498 +          val tpath = tack_on (relative_path (!index_path) (html_path (implode (tl path))))
   1.499 +                              tname;
   1.500 +        in "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^
   1.501 +           tack_on rel_gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^
   1.502 +           "<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^
   1.503 +           tack_on rel_gif_path "blue_arrow.gif\
   1.504 +           \\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^
   1.505 +           ".html\">" ^ tname ^ "</A><BR>\n"
   1.506 +        end;
   1.507 +
   1.508 +      val out = TextIO.openOut (tack_on (!index_path) "index.html");
   1.509 +
   1.510 +      (*Find out in which subdirectory of Isabelle's main directory the
   1.511 +        index.html is placed; if original_path is no subdirectory of base_path
   1.512 +        then take the last directory of index_path*)
   1.513 +      val inside_isabelle = (!original_path) subdir_of (!base_path);
   1.514 +      val subdir =
   1.515 +        if inside_isabelle then relative_path (html_path (!base_path)) (!index_path)
   1.516 +        else base_name (!index_path);
   1.517 +      val subdirs = space_explode "/" subdir;
   1.518 +
   1.519 +      (*Look for index.html in superdirectories; stop when Isabelle's
   1.520 +        main directory is reached*)
   1.521 +      fun find_super_index [] n = ("", n)
   1.522 +        | find_super_index (p::ps) n =
   1.523 +          let val index_path = "/" ^ space_implode "/" (rev ps);
   1.524 +          in if file_exists (index_path ^ "/index.html") then (index_path, n)
   1.525 +             else if length subdirs - n > 0 then find_super_index ps (n+1)
   1.526 +             else ("", n)
   1.527 +          end;
   1.528 +      val (super_index, level_diff) =
   1.529 +        find_super_index (rev (space_explode "/" (!index_path))) 1;
   1.530 +      val level = length subdirs - level_diff;
   1.531 +
   1.532 +      (*Add link to current directory to 'super' index.html*)
   1.533 +      fun link_directory () =
   1.534 +        let val old_index = TextIO.openIn (super_index ^ "/index.html");
   1.535 +            val content = rev (explode (TextIO.inputAll old_index));
   1.536 +            val dummy = TextIO.closeIn old_index;
   1.537 +
   1.538 +            val out = TextIO.openAppend (super_index ^ "/index.html");
   1.539 +            val rel_path = space_implode "/" (drop (level, subdirs));
   1.540 +        in 
   1.541 +           TextIO.output (out,
   1.542 +             (if nth_elem (3, content) <> "!" then ""
   1.543 +              else "\n<HR><H3>Subdirectories:</H3>\n") ^
   1.544 +             "<H3><A HREF = \"" ^ rel_path ^ "/index.html\">" ^ rel_path ^
   1.545 +             "</A></H3>\n");
   1.546 +           TextIO.closeOut out
   1.547 +        end;
   1.548 +
   1.549 +     (*If original_path is no subdirectory of base_path then the title should
   1.550 +       not contain the string "Isabelle/"*)
   1.551 +     val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir;
   1.552 +     val rel_graph_path = tack_on (relative_path (!index_path) (graph_path (!original_path)))
   1.553 +                                  "theories.html"
   1.554 +  in TextIO.output (out,
   1.555 +       "<HTML><HEAD><TITLE>" ^ title ^ "</TITLE></HEAD>\n\
   1.556 +       \<BODY><H2>" ^ title ^ "</H2>\n\
   1.557 +       \The name of every theory is linked to its theory file<BR>\n\
   1.558 +       \<IMG SRC = \"" ^ tack_on rel_gif_path "red_arrow.gif\
   1.559 +       \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
   1.560 +       \<IMG SRC = \"" ^ tack_on rel_gif_path "blue_arrow.gif\
   1.561 +       \\" ALT = /\\></A> stands for supertheories (parent theories)<P>\n\
   1.562 +       \View <A HREF=\"" ^ rel_graph_path ^ "\">graph</A> of theories<P>\n" ^
   1.563 +       (if super_index = "" then "" else
   1.564 +        ("<A HREF = \"" ^ relative_path (!index_path) super_index ^ 
   1.565 +         "/index.html\">Back</A> to the index of " ^
   1.566 +         (if not inside_isabelle then
   1.567 +            hd (tl (rev (space_explode "/" (!index_path))))
   1.568 +          else if level = 0 then "Isabelle logics"
   1.569 +          else space_implode "/" (take (level, subdirs))))) ^
   1.570 +       "\n" ^
   1.571 +       (if file_exists (tack_on (!index_path) "README.html") then
   1.572 +          "<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n"
   1.573 +        else if file_exists (tack_on (!index_path) "README") then
   1.574 +          "<BR>View the <A HREF = \"README\">ReadMe</A> file.\n"
   1.575 +        else "") ^
   1.576 +       "<HR>" ^ implode (map main_entry theories) ^ "<!-->");
   1.577 +     TextIO.closeOut out;
   1.578 +     if super_index = "" orelse (inside_isabelle andalso level = 0) then ()
   1.579 +        else link_directory ()
   1.580 +  end;
   1.581 +
   1.582 +
   1.583 +(*Append section heading to HTML file*)
   1.584 +fun section s =
   1.585 +  case !cur_htmlfile of
   1.586 +      Some out => (mk_theorems_title out;
   1.587 +                   TextIO.output (out, "<H3>" ^ s ^ "</H3>\n"))
   1.588 +    | None => ();
   1.589 +
   1.590 +
   1.591 +(*Add theorem to HTML file*)
   1.592 +fun thm_to_html thm name =
   1.593 +  case !cur_htmlfile of
   1.594 +         Some out =>
   1.595 +           (mk_theorems_title out;
   1.596 +            TextIO.output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
   1.597 +                         (implode o escape)
   1.598 +                          (explode 
   1.599 +                           (string_of_thm (#1 (freeze_thaw thm)))) ^
   1.600 +                         "</PRE><P>\n")
   1.601 +           )
   1.602 +       | None => ();
   1.603 +
   1.604 +
   1.605 +(*Close HTML file*)
   1.606 +fun close_html () =
   1.607 +  case !cur_htmlfile of
   1.608 +      Some out => (TextIO.output (out, "<HR></BODY></HTML>\n");
   1.609 +                   TextIO.closeOut out;
   1.610 +                   cur_htmlfile := None)
   1.611 +    | None => () ;
   1.612 +
   1.613 +
   1.614 +(******************** Graph generation functions ************************)
   1.615 +
   1.616 +
   1.617 +(*flag that indicates whether graph files should be generated*)
   1.618 +val make_graph = ref false;
   1.619 +
   1.620 +
   1.621 +(*file to use as basis for new graph files*)
   1.622 +val graph_base_file = ref "";
   1.623 +
   1.624 +
   1.625 +(*directory containing basic theories (gets label "base")*)
   1.626 +val graph_root_dir = ref "";
   1.627 +
   1.628 +
   1.629 +(*name of current graph file*)
   1.630 +val graph_file = ref "";
   1.631 +
   1.632 +
   1.633 +(*name of large graph file which also contains
   1.634 +  theories defined in subdirectories *)
   1.635 +val large_graph_file = ref "";
   1.636 +
   1.637 +
   1.638 +(* initialize graph data generator *)
   1.639 +fun init_graph usedir_arg =
   1.640 +  let
   1.641 +      (*create default graph containing only Pure, CPure and ProtoPure*)
   1.642 +      fun default_graph outfile =
   1.643 +        let val os = TextIO.openOut outfile;
   1.644 +        in (TextIO.output(os,"\"ProtoPure\" \"ProtoPure\" \"Pure\" \"\" ;\n\
   1.645 +                             \\"CPure\" \"CPure\" \"Pure\" \"\" > \"ProtoPure\" ;\n\
   1.646 +                             \\"Pure\" \"Pure\" \"Pure\" \"\" > \"ProtoPure\" ;\n");
   1.647 +            TextIO.closeOut os)
   1.648 +        end;
   1.649 +
   1.650 +      (*copy graph file, adjust relative paths for theory files*)
   1.651 +      fun copy_graph infile outfile unfold =
   1.652 +        let val is = TextIO.openIn infile;
   1.653 +            val (inp_dir, _) = split_filename infile;
   1.654 +            val (outp_dir, _) = split_filename outfile;
   1.655 +            val entries = map (space_explode " ")
   1.656 +                            (space_explode "\n" (TextIO.inputAll is));
   1.657 +
   1.658 +            fun thyfile f = if f = "\"\"" then f else
   1.659 +              let val (dir, name) =
   1.660 +                    split_filename (implode (rev (tl (rev (tl (explode f))))));
   1.661 +                  val abs_path = normalize_path (tack_on inp_dir dir);
   1.662 +                  val rel_path = tack_on (relative_path outp_dir abs_path) name
   1.663 +              in quote rel_path end;
   1.664 +
   1.665 +            fun process_entry (a::b::c::d::e::r) =                        
   1.666 +              if d = "+" then
   1.667 +                a::b::c::((if unfold then "+ " else "") ^ (thyfile e))::r
   1.668 +              else
   1.669 +                a::b::c::(thyfile d)::e::r;
   1.670 +                   
   1.671 +            val _  = TextIO.closeIn is;
   1.672 +            val os = TextIO.openOut outfile;
   1.673 +            val _  = TextIO.output(os, (cat_lines
   1.674 +                          (map ((space_implode " ") o process_entry) entries)) ^ "\n");
   1.675 +            val _  = TextIO.closeOut os;
   1.676 +        in () end;
   1.677 +
   1.678 +      (*create html page which contains graph browser applet*)
   1.679 +      fun mk_applet_page abs_path large other_graph =
   1.680 +        let
   1.681 +          val dir_name =
   1.682 +            (if (!original_path) subdir_of (!base_path) then "Isabelle/" else "") ^
   1.683 +            (relative_path (normalize_path (tack_on (!graph_root_dir) "..")) (pwd ()));
   1.684 +          val rel_codebase = 
   1.685 +            relative_path abs_path (tack_on (normalize_path (!output_dir)) "graph");
   1.686 +          val rel_index_path = tack_on (relative_path
   1.687 +            abs_path (tack_on (normalize_path (!output_dir)) "graph")) "index.html";
   1.688 +          val outfile =
   1.689 +            tack_on abs_path ((if large then "all_" else "") ^ "theories.html");
   1.690 +          val os = TextIO.openOut outfile;
   1.691 +          val _ = TextIO.output(os,
   1.692 +            "<HTML><HEAD><TITLE>" ^ dir_name ^ "</TITLE></HEAD>\n\
   1.693 +            \<BODY><H2>" ^ dir_name ^ "</H2>\n" ^
   1.694 +            (if other_graph then
   1.695 +              (if large then
   1.696 +                 "View <A HREF=\"theories.html\">small graph</A> without \
   1.697 +                 \subdirectories<P>\n"
   1.698 +               else
   1.699 +                 "View <A HREF=\"all_theories.html\">large graph</A> including \
   1.700 +                 \all subdirectories<P>\n")
   1.701 +             else "") ^
   1.702 +            "<A HREF=\"" ^ rel_index_path ^ "\">Back</A> to index\n<HR>\n\
   1.703 +            \<APPLET CODE=\"GraphBrowser/GraphBrowser.class\" \
   1.704 +            \CODEBASE=\"" ^ rel_codebase ^ "\" WIDTH=550 HEIGHT=450>\n\
   1.705 +            \<PARAM NAME=\"graphfile\" VALUE=\"" ^
   1.706 +            (if large then "all_theories.graph" else "theories.graph") ^ "\">\n\
   1.707 +            \</APPLET>\n<HR>\n</BODY></HTML>")
   1.708 +          val _ = TextIO.closeOut os
   1.709 +        in () end;
   1.710 +      
   1.711 +      val gpath = graph_path (pwd ());
   1.712 +
   1.713 +  in
   1.714 +    (make_graph := true;
   1.715 +     base_path := normalize_path (!base_path);
   1.716 +     mkdir gpath;
   1.717 +     original_path := pwd ();
   1.718 +     graph_file := tack_on gpath "theories.graph";
   1.719 +     graph_root_dir := (if usedir_arg = "." then pwd ()
   1.720 +                        else normalize_path (tack_on (pwd ()) ".."));
   1.721 +     (if (!graph_base_file) = "" then
   1.722 +        (large_graph_file := tack_on gpath "all_theories.graph";
   1.723 +         default_graph (!graph_file);
   1.724 +         default_graph (!large_graph_file);
   1.725 +         mk_applet_page gpath false true;
   1.726 +         mk_applet_page gpath true true)
   1.727 +      else
   1.728 +        (if (fst (split_filename (!graph_file))) subdir_of
   1.729 +            (fst (split_filename (!graph_base_file)))
   1.730 +         then
   1.731 +           (copy_graph (!graph_base_file) (!graph_file) true;
   1.732 +            mk_applet_page gpath false false)
   1.733 +         else
   1.734 +           (large_graph_file := tack_on gpath "all_theories.graph";
   1.735 +            mk_applet_page gpath false true;
   1.736 +            mk_applet_page gpath true true;
   1.737 +            copy_graph (!graph_base_file) (!graph_file) false;
   1.738 +            copy_graph (!graph_base_file) (!large_graph_file) false)));
   1.739 +     graph_base_file := (!graph_file))
   1.740 +  end;
   1.741 +
   1.742 +
   1.743 +(*add theory to graph definition file*)
   1.744 +fun mk_graph tname abs_path = if not (!make_graph) then () else
   1.745 +  let val parents =
   1.746 +        map (fn (t, _) => tack_on (path_of t) t)
   1.747 +          (filter (fn (_, ThyInfo {children,...}) => tname mem children)
   1.748 +             (Symtab.dest(!loaded_thys)));
   1.749 +
   1.750 +      val dir_name = relative_path
   1.751 +         (normalize_path (tack_on (!graph_root_dir) "..")) abs_path;
   1.752 +
   1.753 +      val dir_entry = "\"" ^ dir_name ^
   1.754 +         (if (tack_on abs_path "") = (tack_on (!graph_root_dir) "")
   1.755 +          then "/base\" + " else "\" ");
   1.756 +
   1.757 +      val thy_file = (tack_on (html_path abs_path) tname) ^ ".html";
   1.758 +
   1.759 +      val thy_ID = quote (tack_on abs_path tname);
   1.760 +
   1.761 +      val entry_str_1 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^
   1.762 +                (quote (relative_path (fst (split_filename (!graph_file))) thy_file)) ^
   1.763 +                " > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ;
   1.764 +
   1.765 +      val entry_str_2 = (quote tname) ^ " " ^ thy_ID ^ " " ^ dir_entry ^
   1.766 +                (quote (relative_path (fst (split_filename (!large_graph_file))) thy_file)) ^
   1.767 +                " > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ;
   1.768 +
   1.769 +      fun exists_entry id infile =
   1.770 +        let val is = TextIO.openIn(infile);
   1.771 +            val IDs = map (hd o tl o (space_explode " "))
   1.772 +                            (space_explode "\n" (TextIO.inputAll is));
   1.773 +            val _ = TextIO.closeIn is
   1.774 +        in id mem IDs end;
   1.775 +
   1.776 +      fun mk_entry outfile entry_str =
   1.777 +        if exists_entry thy_ID outfile then ()
   1.778 +        else
   1.779 +          let val os = TextIO.openAppend outfile;
   1.780 +              val _ = TextIO.output (os, entry_str);
   1.781 +              val _ = TextIO.closeOut os;
   1.782 +          in () end
   1.783 +
   1.784 +  in (mk_entry (!graph_file) entry_str_1;
   1.785 +      mk_entry (!large_graph_file) entry_str_2) handle _ =>
   1.786 +             (make_graph:=false;
   1.787 +              warning ("Unable to write to graph file " ^ (!graph_file)))
   1.788 +  end;
   1.789 +
   1.790 +end;