# HG changeset patch
# User clasohm
# Date 817475833 -3600
# Node ID f00280dff0dc4bb38e9d3058d58d05729bbdc12b
# Parent  78bdb2d047710cfe25a0c6d61e2478d2fc4ac1d2
renamed make_chart to finish_html

diff -r 78bdb2d04771 -r f00280dff0dc src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Fri Nov 24 11:46:23 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML	Mon Nov 27 13:37:13 1995 +0100
@@ -82,7 +82,7 @@
   val pure_subchart : string option ref
   val make_html     : bool ref
   val init_html     : unit -> unit
-  val make_chart    : unit -> unit
+  val finish_html   : unit -> unit
 end;
 
 
@@ -1045,6 +1045,11 @@
       val rel_gif_path = relative_path cwd (!gif_path);
       val package = relative_path (!base_path) cwd;
 
+      val dummy = if (explode (!base_path)) prefix (explode cwd) then ()
+        else error "The current working directory seems to be no \
+                   \subdirectory of\nIsabelle's main directory. \
+                   \Please ensure that base_path's value is correct.";
+
       (*Make new HTML files for Pure and CPure*)
       fun init_pure_html () =
         let val pure_out = open_out ".Pure_sub.html";
@@ -1070,7 +1075,7 @@
   end;
 
 (*Generate index.html*)
-fun make_chart () = if not (!make_html) then () else
+fun finish_html () = if not (!make_html) then () else
   let val tlist_path = tack_on (!index_path) ".theory_list.txt";
       val theory_list = open_in tlist_path;
       val theories = space_explode "\n" (input (theory_list, 999999));
@@ -1100,7 +1105,7 @@
 
       (*Look for index.html in superdirectories*)
       fun find_super_index [] _ =
-            error "make_chart: Unable to find super index file."
+            error "finish_html: Unable to find super index file."
         | find_super_index (p::ps) n =
           let val index_path = "/" ^ space_implode "/" (rev ps);
           in if file_exists (index_path ^ "/index.html") then (index_path, n)
@@ -1200,12 +1205,12 @@
   (cd dirname;
    if !make_html then init_html() else ();
    use "ROOT.ML";
-   make_chart());
+   finish_html());
 
 fun exit_use_dir dirname =
   (cd dirname;
    if !make_html then init_html() else ();
    exit_use "ROOT.ML";
-   make_chart());
+   finish_html());
 
 end;