checkpoint -- basic functionality only;
authorwenzelm
Tue Mar 09 12:19:25 1999 +0100 (1999-03-09)
changeset 6330e1faf0f6f2b8
parent 6329 bbd03b119f36
child 6331 fb7b8d6c2bd1
checkpoint -- basic functionality only;
src/Pure/Thy/browser_info.ML
     1.1 --- a/src/Pure/Thy/browser_info.ML	Tue Mar 09 12:18:46 1999 +0100
     1.2 +++ b/src/Pure/Thy/browser_info.ML	Tue Mar 09 12:19:25 1999 +0100
     1.3 @@ -1,227 +1,219 @@
     1.4 -(*  Title:      Pure/Thy/thy_browser_info.ML
     1.5 +(*  Title:      Pure/Thy/browser_info.ML
     1.6      ID:         $Id$
     1.7 -    Author:     Stefan Berghofer and Carsten Clasohm
     1.8 -    Copyright   1994, 1997 TU Muenchen
     1.9 +    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    1.10 +
    1.11 +Theory browsing information (HTML and graph files).
    1.12 +
    1.13 +TODO:
    1.14 +  - Contents: theories, sessions;
    1.15 +  - symlink ".parent", ".top" (URLs!?);
    1.16 +  - extend parent index: maintain "<!--insert--here-->" marker (!?);
    1.17 +  - proper handling of out of context theorems / sections (!?);
    1.18 +  - usedir: exclude arrow gifs;
    1.19 +*)
    1.20  
    1.21 -The first design of the text-based html browser is due to Mateja Jamnik.
    1.22 +signature BASIC_BROWSER_INFO =
    1.23 +sig
    1.24 +  val section: string -> unit
    1.25 +end;
    1.26  
    1.27 -Functions for generating theory browsing information
    1.28 -(i.e. *.html and *.graph - files).
    1.29 -*)
    1.30 +signature BROWSER_INFO =
    1.31 +sig
    1.32 +  include BASIC_BROWSER_INFO
    1.33 +  val init: bool -> string -> string list -> string -> string -> unit
    1.34 +  val finish: unit -> unit
    1.35 +  val theory_source: string -> (string, 'a) Source.source -> unit
    1.36 +  val begin_theory: string -> string list -> (Path.T * bool) list -> unit
    1.37 +  val end_theory: string -> unit
    1.38 +  val theorem: string -> thm -> unit
    1.39 +end;
    1.40 +
    1.41 +structure BrowserInfo: BROWSER_INFO =
    1.42 +struct
    1.43  
    1.44  
    1.45 -(** filenames and paths **)             (* FIXME FIXME FIXME eliminate!!! *)
    1.46 +(** global browser info state **)
    1.47 +
    1.48 +(* type theory_info *)
    1.49 +
    1.50 +type theory_info = {source: Buffer.T, html: Buffer.T, graph: Buffer.T};
    1.51  
    1.52 -(*BAD_space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*)
    1.53 -fun BAD_space_explode sep s =
    1.54 -  let fun divide [] "" = []
    1.55 -        | divide [] part = [part]
    1.56 -        | divide (c::s) part =
    1.57 -            if c = sep then
    1.58 -              (if part = "" then divide s "" else part :: divide s "")
    1.59 -            else divide s (part ^ c)
    1.60 -  in divide (explode s) "" end;
    1.61 +fun make_theory_info (source, html, graph) =
    1.62 +  {source = source, html = html, graph = graph}: theory_info;
    1.63 +
    1.64 +val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty);
    1.65 +fun map_theory_info f {source, html, graph} = make_theory_info (f (source, html, graph));
    1.66  
    1.67 -(*Convert UNIX filename of the form "path/file" to "path/" and "file";
    1.68 -  if filename contains no slash, then it returns "" and "file"*)
    1.69 -val split_filename =
    1.70 -  (pairself implode) o take_suffix (not_equal "/") o explode;
    1.71  
    1.72 -val base_name = #2 o split_filename;
    1.73 +(* type browser_info *)
    1.74 +
    1.75 +type browser_info = {theories: theory_info Symtab.table, index: Buffer.T};
    1.76  
    1.77 -(*Merge splitted filename (path and file);
    1.78 -  if path does not end with one a slash is appended*)
    1.79 -fun tack_on "" name = name
    1.80 -  | tack_on path name =
    1.81 -      if last_elem (explode path) = "/" then path ^ name
    1.82 -      else path ^ "/" ^ name;
    1.83 +fun make_browser_info (theories, index) =
    1.84 +  {theories = theories, index = index}: browser_info;
    1.85  
    1.86 -(*Remove the extension of a filename, i.e. the part after the last '.'*)
    1.87 -val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode;
    1.88 +val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty);
    1.89 +fun map_browser_info f {theories, index} = make_browser_info (f (theories, index));
    1.90 +
    1.91  
    1.92 -(*Make relative path to reach an absolute location from a different one*)
    1.93 -fun relative_path cur_path dest_path =
    1.94 -  let (*Remove common beginning of both paths and make relative path*)
    1.95 -      fun mk_relative [] [] = []
    1.96 -        | mk_relative [] ds = ds
    1.97 -        | mk_relative cs [] = map (fn _ => "..") cs
    1.98 -        | mk_relative (c::cs) (d::ds) =
    1.99 -            if c = d then mk_relative cs ds
   1.100 -            else ".." :: map (fn _ => "..") cs @ (d::ds);
   1.101 -  in if cur_path = "" orelse hd (explode cur_path) <> "/" orelse
   1.102 -        dest_path = "" orelse hd (explode dest_path) <> "/" then
   1.103 -       error "Relative or empty path passed to relative_path"
   1.104 -     else ();
   1.105 -     space_implode "/" (mk_relative (BAD_space_explode "/" cur_path)
   1.106 -                                    (BAD_space_explode "/" dest_path))
   1.107 -  end;
   1.108 +(* state *)
   1.109 +
   1.110 +val browser_info = ref empty_browser_info;
   1.111 +
   1.112 +fun change_browser_info f = browser_info := map_browser_info f (! browser_info);
   1.113 +
   1.114 +fun init_theory_info name info = change_browser_info (fn (theories, index) =>
   1.115 +  (Symtab.update ((name, info), theories), index));
   1.116  
   1.117 -(*Determine if absolute path1 is a subdirectory of absolute path2*)
   1.118 -fun subdir_of (path1, path2) =
   1.119 -  if hd (explode path1) <> "/" orelse hd (explode path2) <> "/" then
   1.120 -    error "Relative or empty path passed to subdir_of"
   1.121 -  else (BAD_space_explode "/" path2) prefix (BAD_space_explode "/" path1);
   1.122 +fun change_theory_info name f = change_browser_info (fn (theories, index) =>
   1.123 +  (case Symtab.lookup (theories, name) of
   1.124 +    None => (warning ("Browser info: cannot access theory document " ^ quote name);
   1.125 +      (theories, index))
   1.126 +  | Some info => (Symtab.update ((name, map_theory_info f info), theories), index)));
   1.127 +
   1.128  
   1.129 -fun absolute_path cwd file =
   1.130 -  let fun rm_points [] result = rev result
   1.131 -        | rm_points (".."::ds) result = rm_points ds (tl result)
   1.132 -        | rm_points ("."::ds) result = rm_points ds result
   1.133 -        | rm_points (d::ds) result = rm_points ds (d::result);
   1.134 -  in if file = "" then ""
   1.135 -     else if hd (explode file) = "/" then file
   1.136 -     else "/" ^ space_implode "/"
   1.137 -                  (rm_points (BAD_space_explode "/" (tack_on cwd file)) [])
   1.138 -  end;
   1.139 +fun add_source name txt = change_theory_info name (fn (source, html, graph) =>
   1.140 +  (Buffer.add txt source, html, graph));
   1.141 +
   1.142 +fun add_html name txt = change_theory_info name (fn (source, html, graph) =>
   1.143 +  (source, Buffer.add txt html, graph));
   1.144 +
   1.145 +fun add_graph name txt = change_theory_info name (fn (source, html, graph) =>
   1.146 +  (source, html, Buffer.add txt graph));
   1.147  
   1.148  
   1.149  
   1.150 -signature BROWSER_INFO =
   1.151 -sig
   1.152 -  val output_dir       : string ref
   1.153 -  val home_path        : string ref
   1.154 -  val base_path        : string ref
   1.155 -  val make_graph       : bool ref
   1.156 -  val init_graph       : string -> unit
   1.157 -  val mk_graph         : string -> string -> unit
   1.158 -  val cur_thyname      : string ref
   1.159 -  val make_html        : bool ref
   1.160 -  val mk_html          : string -> string -> string list -> unit
   1.161 -  val thyfile2html     : string -> string -> unit
   1.162 -  val init_html        : unit -> unit
   1.163 -  val finish_html      : unit -> unit
   1.164 -  val section          : string -> unit
   1.165 -  val thm_to_html      : thm -> string -> unit
   1.166 -  val close_html       : unit -> unit
   1.167 +(** global session state **)
   1.168 +
   1.169 +(* paths *)
   1.170 +
   1.171 +val output_path = Path.variable "ISABELLE_BROWSER_INFO";
   1.172 +
   1.173 +fun top_path sess_path = Path.append (Path.appends (replicate (length sess_path) Path.parent));
   1.174 +val parent_path = Path.append Path.parent;
   1.175 +
   1.176 +val html_ext = Path.ext "html";
   1.177 +val html_path = html_ext o Path.basic;
   1.178 +val graph_path = Path.ext "graph" o Path.basic;
   1.179 +val index_path = Path.basic "index.html";
   1.180 +
   1.181 +
   1.182 +(* session_info *)
   1.183 +
   1.184 +type session_info =
   1.185 +  {session: string, path: string list, parent: string, name: string,
   1.186 +    html_prefix: Path.T, graph_prefix: Path.T};
   1.187 +
   1.188 +fun make_session_info (session, path, parent, name, html_prefix, graph_prefix) =
   1.189 +  {session = session, path = path, parent = parent, name = name,
   1.190 +    html_prefix = html_prefix, graph_prefix = graph_prefix}: session_info;
   1.191 +
   1.192 +val session_info = ref (None: session_info option);
   1.193 +
   1.194 +fun in_context f = f (PureThy.get_name (Context.the_context ()));
   1.195 +fun conditional f = (case ! session_info of None => () | Some info => f info);
   1.196 +
   1.197 +
   1.198 +(* init session *)
   1.199 +
   1.200 +fun init false _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
   1.201 +  | init true session path parent name =
   1.202 +      let
   1.203 +        val out_path = Path.expand output_path;
   1.204 +        val sess_prefix = Path.make path;
   1.205 +        val html_prefix = Path.append out_path sess_prefix;
   1.206 +        val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix];
   1.207 +      in
   1.208 +        File.mkdir html_prefix;
   1.209 +        File.mkdir graph_prefix;
   1.210 +        browser_info := empty_browser_info;
   1.211 +        session_info :=
   1.212 +          Some (make_session_info (session, path, parent, name, html_prefix, graph_prefix))
   1.213 +      end;
   1.214 +
   1.215 +
   1.216 +(* finish session *)
   1.217 +
   1.218 +fun finish_node html_prefix graph_prefix (name, {source = _, html, graph}) =
   1.219 + (Buffer.write (Path.append html_prefix (html_path name)) (Buffer.add HTML.conclude_theory html);
   1.220 +  Buffer.write (Path.append graph_prefix (graph_path name)) graph);
   1.221 +
   1.222 +fun finish () = conditional (fn {html_prefix, graph_prefix, ...} =>
   1.223 +  let val {theories, index} = ! browser_info in
   1.224 +    seq (finish_node html_prefix graph_prefix) (Symtab.dest theories);
   1.225 +    Buffer.write (Path.append html_prefix index_path) index;
   1.226 +    browser_info := empty_browser_info;
   1.227 +    session_info := None
   1.228 +  end);
   1.229 +
   1.230 +
   1.231 +
   1.232 +(** HTML output **)
   1.233 +
   1.234 +fun theory_source name src = conditional (fn _ =>
   1.235 +  (init_theory_info name empty_theory_info; add_source name (HTML.source src)));
   1.236 +
   1.237 +fun begin_theory name parents orig_files = conditional (fn {session, html_prefix, ...} =>
   1.238 +  let
   1.239 +    val ml_path = ThyLoad.ml_path name;
   1.240 +    val files = orig_files @		(* FIXME improve!? *)
   1.241 +      (if is_some (ThyLoad.check_file ml_path) then [(ml_path, true)] else []);
   1.242 +    val files_html = map (fn (p, loadit) => ((p, html_ext p), loadit)) files;
   1.243 +
   1.244 +    fun prep_file raw_path =
   1.245 +      (case ThyLoad.check_file raw_path of
   1.246 +        Some (path, _) =>
   1.247 +          let val base = Path.base path in
   1.248 +            File.write (Path.append html_prefix (html_ext base))
   1.249 +              (HTML.ml_file base (File.read path))
   1.250 +          end
   1.251 +      | None => warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path)));
   1.252 +
   1.253 +    fun prep_source (source, html, graph) =
   1.254 +      let val txt =
   1.255 +        HTML.begin_theory (index_path, session) name parents files_html (Buffer.content source)
   1.256 +        in (Buffer.empty, Buffer.add txt html, graph) end;
   1.257 +  in
   1.258 +    seq (prep_file o #1) files;
   1.259 +    change_theory_info name prep_source
   1.260 +  end);
   1.261 +
   1.262 +fun end_theory name = conditional (fn _ => add_html name HTML.end_theory);
   1.263 +
   1.264 +fun theorem name thm = conditional (fn _ => in_context add_html (HTML.theorem name thm));
   1.265 +fun section s = conditional (fn _ => in_context add_html (HTML.section s));
   1.266 +
   1.267 +
   1.268  end;
   1.269  
   1.270  
   1.271 -structure BrowserInfo : BROWSER_INFO =
   1.272 -struct
   1.273 -
   1.274 -open ThyInfo;
   1.275 -
   1.276 -
   1.277 -(*directory where to put html and graph files*)
   1.278 -val output_dir = ref "";
   1.279 -
   1.280 -
   1.281 -(*path of user home directory*)
   1.282 -val home_path = ref "";
   1.283 -
   1.284 -
   1.285 -(*normalize a path
   1.286 -  FIXME: move to library?*)
   1.287 -fun normalize_path p =
   1.288 -   let val curr_dir = pwd ();
   1.289 -       val _ = cd p;
   1.290 -       val norm_path = pwd ();
   1.291 -       val _ = cd curr_dir
   1.292 -   in norm_path end;
   1.293 -
   1.294 -
   1.295 -(*create directory
   1.296 -  FIXME: move to library?*)
   1.297 -fun mkdir path = (execute ("mkdir -p " ^ path); ());
   1.298 -
   1.299 -
   1.300 -(*Path of Isabelle's main (source) directory
   1.301 -  FIXME: this value should be provided by isatool!*)
   1.302 -val base_path = ref (
   1.303 -  "/" ^ space_implode "/" (rev (tl (tl (rev (BAD_space_explode "/" (OS.FileSys.getDir ())))))));
   1.304  
   1.305  
   1.306  
   1.307 -(******************** HTML generation functions *************************)
   1.308 -
   1.309 -(*Set location of graphics for HTML files*)
   1.310 -fun gif_path () = tack_on (normalize_path (!output_dir)) "gif";
   1.311 -
   1.312 +(* FIXME
   1.313  
   1.314 -(*Name of theory currently being read*)
   1.315 -val cur_thyname = ref "";
   1.316 -
   1.317 -
   1.318 -(*Name of current logic*)
   1.319 -val package = ref "";
   1.320 -
   1.321 +(* head of HTML dependency chart *)
   1.322  
   1.323 -(* Return path of directory where to store html / graph data
   1.324 -   corresponding to theory with given path *)
   1.325 -local
   1.326 -  fun make_path q p =
   1.327 -    let val outp_dir = normalize_path (!output_dir);
   1.328 -        val base = if q = "" then outp_dir else tack_on outp_dir q;
   1.329 -        val rpath = if subdir_of (p, !base_path) then relative_path (!base_path) p
   1.330 -                    else relative_path (normalize_path (!home_path)) p;
   1.331 -    in tack_on base rpath end
   1.332 -in
   1.333 -  val html_path = make_path "";
   1.334 -  val graph_path = make_path "graph/data"
   1.335 -end;
   1.336 -
   1.337 +fun mk_charthead name title repeats top_path index_path parent =
   1.338 +  "<html><head><title>" ^ title ^ " of " ^ name ^
   1.339 +  "</title></head>\n<h2>" ^ title ^ " of theory " ^ name ^
   1.340 +  "</h2>\nThe name of every theory is linked to its theory file<br>\n" ^
   1.341 +  "<img src=" ^ htmlify (top_path red_arrow_path) ^
   1.342 +  " alt =\"\\/\"></a> stands for subtheories (child theories)<br>\n\
   1.343 +  \<img src=" ^ htmlify (top_path blue_arrow_path) ^
   1.344 +  " alt =\"/\\\"></a> stands for supertheories (parent theories)\n" ^
   1.345 +  (if not repeats then "" else "<br><tt>...</tt> stands for repeated subtrees") ^
   1.346 +  "<p>\n<a href=" ^ htmlify index_path ^ ">Back</a> to " ^ parent ^ "\n<hr>\n";
   1.347  
   1.348 -(*Location of theory-list.txt and index.html (set by init_html)*)
   1.349 -val index_path = ref "";
   1.350 -
   1.351 -
   1.352 -(*Original path of ROOT.ML*)
   1.353 -val original_path = ref "";
   1.354 -
   1.355 -
   1.356 -(*Location of Pure_sub.html and CPure_sub.html*)
   1.357 -val pure_subchart = ref (None : string option);
   1.358 -
   1.359 -
   1.360 -(*Controls whether HTML files should be generated*)
   1.361 -val make_html = ref false;
   1.362 +(* FIXME "<pre>"  *)
   1.363  
   1.364  
   1.365 -(*HTML file of theory currently being read
   1.366 -  (Initialized by thyfile2html; used by use_thy and store_thm)*)
   1.367 -val cur_htmlfile = ref None : TextIO.outstream option ref;
   1.368 -
   1.369 -
   1.370 -(*Boolean variable which indicates if the title "Theorems proved in foo.ML"
   1.371 -  has already been inserted into the current HTML file*)
   1.372 -val cur_has_title = ref false;
   1.373 -
   1.374 +(* theory_file *)
   1.375  
   1.376 -(*Make head of HTML dependency charts
   1.377 -  Parameters are:
   1.378 -    file: HTML file
   1.379 -    tname: theory name
   1.380 -    suffix: suffix of complementary chart
   1.381 -            (sup if this head is for a sub-chart, sub if it is for a sup-chart;
   1.382 -             empty for Pure and CPure sub-charts)
   1.383 -    gif_path: relative path to directory containing GIFs
   1.384 -    index_path: relative path to directory containing main theory chart
   1.385 -*)
   1.386 -fun mk_charthead file tname title repeats gif_path index_path package =
   1.387 -  TextIO.output (file,
   1.388 -   "<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^
   1.389 -   "</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^
   1.390 -   "</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^
   1.391 -   "<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
   1.392 -   \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
   1.393 -   \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
   1.394 -   \\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^
   1.395 -   (if not repeats then "" else
   1.396 -      "<BR><TT>...</TT> stands for repeated subtrees") ^
   1.397 -   "<P>\n<A HREF = \"" ^ tack_on index_path "index.html\
   1.398 -   \\">Back</A> to the index of " ^ package ^ "\n<HR>\n<PRE>");
   1.399 +(*convert .thy file to HTML and make chart of its super-theories*)
   1.400  
   1.401 +(* FIXME include ML file (!?!?) *)
   1.402  
   1.403 -(*Convert special HTML characters ('&', '>', and '<')*)
   1.404 -fun escape []       = []
   1.405 -  | escape ("<"::s) = "&lt;" :: escape s
   1.406 -  | escape (">"::s) = "&gt;" :: escape s
   1.407 -  | escape ("&"::s) = "&amp;" :: escape s
   1.408 -  | escape (c::s)   = c :: escape s;
   1.409 -
   1.410 -
   1.411 -(*Convert .thy file to HTML and make chart of its super-theories*)
   1.412 -fun thyfile2html tname thy_path = if not (!make_html) then () else
   1.413 -  let
   1.414      (* path of directory, where corresponding HTML file is stored *)
   1.415      val tpath = html_path thy_path;
   1.416  
   1.417 @@ -242,10 +234,38 @@
   1.418      val (theories, thy_files) =
   1.419        list_theories (Symtab.dest (!loaded_thys)) [] [];
   1.420  
   1.421 -    (*convert ML file to html *)
   1.422 +
   1.423 +fun file_name path = "<tt>" ^ Path.pack src_path ^ "</tt>";
   1.424 +
   1.425 +fun ml_file src_path = conditional (fn () =>
   1.426 +  (case ThyLoad.check_file src_path of
   1.427 +    None => file_name src_path
   1.428 +  | Some (path, _) =>
   1.429 +      let
   1.430 +        val base_path = Path.base path;
   1.431 +        val html_base_path = html_ext base_path;
   1.432 +        val name = Path.pack base_path;
   1.433 +        val txt = implode (html_escape (explode (File.read path)));
   1.434 +        val html_txt =
   1.435 +          "<html><head><title>" ^ name ^ "</title></head>\n\n<body>\n" ^
   1.436 +          "<h2>File " ^ name ^ "</h2>\n<hr>\n\n<pre>\n" ^ txt ^ "</pre><hr></body></html>";
   1.437 +      in
   1.438 +        File.write (output_path html_base_path) html_text;
   1.439 +        "<a href=" ^ htmlify html_base_path ^ ">" ^ file_name src_path ^ "</a>"
   1.440 +        "file <a href=" ^ "<tt>" ^ Path.pack src_path ^ "</tt>"
   1.441 +        
   1.442 +
   1.443 +fun theory_header name parents files =
   1.444 +  FIXME;
   1.445 +
   1.446 +
   1.447 +
   1.448 +
   1.449 +fun theory_file name text = conditional (fn () =>
   1.450 +  let
   1.451      fun ml2html name abs_path =
   1.452        let val is  = TextIO.openIn (tack_on abs_path (name ^ ".ML"));
   1.453 -          val inp = implode (escape (explode (TextIO.inputAll is)));
   1.454 +          val inp = implode (html_escape (explode (TextIO.inputAll is)));
   1.455            val _   = TextIO.closeIn is;
   1.456            val os  = TextIO.openOut (tack_on (html_path abs_path) (name ^ "_ML.html"));
   1.457            val _   = TextIO.output (os,
   1.458 @@ -263,26 +283,9 @@
   1.459          val file =
   1.460            let val is  = TextIO.openIn thy_file;
   1.461                val inp = TextIO.inputAll is;
   1.462 -          in (TextIO.closeIn is; escape (explode inp)) end;
   1.463 +          in (TextIO.closeIn is; html_escape (explode inp)) end;
   1.464  
   1.465  
   1.466 -        (*Isolate first (possibly nested) comment;
   1.467 -          skip all leading whitespaces*)
   1.468 -        val (comment, file') =
   1.469 -          let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs)
   1.470 -                | first_comment ("*" :: ")" :: cs) co d =
   1.471 -                    first_comment cs (co ^ "*)") (d-1)
   1.472 -                | first_comment ("(" :: "*" :: cs) co d =
   1.473 -                    first_comment cs (co ^ "(*") (d+1)
   1.474 -                | first_comment (" "  :: cs) "" 0 = first_comment cs "" 0
   1.475 -                | first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0
   1.476 -                | first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0
   1.477 -                | first_comment cs           "" 0 = ("", cs)
   1.478 -                | first_comment (c :: cs) co d =
   1.479 -                    first_comment cs (co ^ implode [c]) d
   1.480 -                | first_comment [] co _ =
   1.481 -                    error ("Unexpected end of file " ^ tname ^ ".thy.");
   1.482 -          in first_comment file "" 0 end;
   1.483  
   1.484          (*Process line defining theory's ancestors;
   1.485            convert valid theory names to links to their HTML file*)
   1.486 @@ -388,7 +391,7 @@
   1.487       else ();
   1.488       cur_htmlfile := Some (TextIO.openOut (tack_on tpath (tname ^ ".html")));
   1.489       cur_has_title := false;
   1.490 -     if File.exists (tack_on thy_path (tname ^ ".ML")) 
   1.491 +     if File.exists (tack_on thy_path (tname ^ ".ML"))
   1.492         then ml2html tname thy_path else ();
   1.493       TextIO.output (the (!cur_htmlfile), gettext (tack_on thy_path tname ^ ".thy"));
   1.494  
   1.495 @@ -442,7 +445,7 @@
   1.496            let val path = if t = "Pure" orelse t = "CPure" then
   1.497                             (the (!pure_subchart))
   1.498                           else html_path (path_of t);
   1.499 - 
   1.500 +
   1.501                val rel_gif_path = relative_path path (gif_path ());
   1.502                val rel_path = relative_path path (html_path abs_path);
   1.503                val tpath = tack_on rel_path tname;
   1.504 @@ -464,7 +467,7 @@
   1.505                 tack_on rel_gif_path "blue_arrow.gif\" ALT = /\\></A>\n");
   1.506               TextIO.closeOut out
   1.507            end;
   1.508 - 
   1.509 +
   1.510          val theory_list =
   1.511            TextIO.openAppend (tack_on (!index_path) "theory_list.txt")
   1.512              handle _ => (make_html := false;
   1.513 @@ -475,7 +478,7 @@
   1.514                                  \writeable directory to reactivate it.");
   1.515                           raise MK_HTML)
   1.516      in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n");
   1.517 -       TextIO.closeOut theory_list; 
   1.518 +       TextIO.closeOut theory_list;
   1.519         robust_seq add_to_parents new_parents
   1.520      end
   1.521    ) handle MK_HTML => ();
   1.522 @@ -595,7 +598,7 @@
   1.523  
   1.524              val out = TextIO.openAppend (super_index ^ "/index.html");
   1.525              val rel_path = space_implode "/" (drop (level, subdirs));
   1.526 -        in 
   1.527 +        in
   1.528             TextIO.output (out,
   1.529               (if nth_elem (3, content) <> "!" then ""
   1.530                else "\n<HR><H3>Subdirectories:</H3>\n") ^
   1.531 @@ -619,7 +622,7 @@
   1.532         \\" ALT = /\\></A> stands for supertheories (parent theories)<P>\n\
   1.533         \View <A HREF=\"" ^ rel_graph_path ^ "\">graph</A> of theories<P>\n" ^
   1.534         (if super_index = "" then "" else
   1.535 -        ("<A HREF = \"" ^ relative_path (!index_path) super_index ^ 
   1.536 +        ("<A HREF = \"" ^ relative_path (!index_path) super_index ^
   1.537           "/index.html\">Back</A> to the index of " ^
   1.538           (if not inside_isabelle then
   1.539              hd (tl (rev (BAD_space_explode "/" (!index_path))))
   1.540 @@ -652,8 +655,8 @@
   1.541           Some out =>
   1.542             (mk_theorems_title out;
   1.543              TextIO.output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^
   1.544 -                         (implode o escape)
   1.545 -                          (explode 
   1.546 +                         (implode o html_escape)
   1.547 +                          (explode
   1.548                             (string_of_thm (#1 (freeze_thaw thm)))) ^
   1.549                           "</PRE><P>\n")
   1.550             )
   1.551 @@ -668,6 +671,9 @@
   1.552                     cur_htmlfile := None)
   1.553      | None => () ;
   1.554  
   1.555 +*)
   1.556 +
   1.557 +(* FIXME
   1.558  
   1.559  (******************** Graph generation functions ************************)
   1.560  
   1.561 @@ -720,12 +726,12 @@
   1.562                    val rel_path = tack_on (relative_path outp_dir abs_path) name
   1.563                in quote rel_path end;
   1.564  
   1.565 -            fun process_entry (a::b::c::d::e::r) =                        
   1.566 +            fun process_entry (a::b::c::d::e::r) =
   1.567                if d = "+" then
   1.568                  a::b::c::((if unfold then "+ " else "") ^ (thyfile e))::r
   1.569                else
   1.570                  a::b::c::(thyfile d)::e::r;
   1.571 -                   
   1.572 +
   1.573              val _  = TextIO.closeIn is;
   1.574              val os = TextIO.openOut outfile;
   1.575              val _  = TextIO.output(os, (cat_lines
   1.576 @@ -739,7 +745,7 @@
   1.577            val dir_name =
   1.578              (if subdir_of (!original_path, !base_path) then "Isabelle/" else "") ^
   1.579              (relative_path (normalize_path (tack_on (!graph_root_dir) "..")) (pwd ()));
   1.580 -          val rel_codebase = 
   1.581 +          val rel_codebase =
   1.582              relative_path abs_path (tack_on (normalize_path (!output_dir)) "graph");
   1.583            val rel_index_path = tack_on (relative_path
   1.584              abs_path (tack_on (normalize_path (!output_dir)) "graph")) "index.html";
   1.585 @@ -765,7 +771,7 @@
   1.586              \</APPLET>\n<HR>\n</BODY></HTML>")
   1.587            val _ = TextIO.closeOut os
   1.588          in () end;
   1.589 -      
   1.590 +
   1.591        val gpath = graph_path (pwd ());
   1.592  
   1.593    in
   1.594 @@ -844,6 +850,4 @@
   1.595               (make_graph:=false;
   1.596                warning ("Unable to write to graph file " ^ (!graph_file)))
   1.597    end;
   1.598 -
   1.599 -
   1.600 -end;
   1.601 +*)