# HG changeset patch
# User clasohm
# Date 819026139 -3600
# Node ID e9ca85a3713c8c12e6c4d495b467791ebc4b0269
# Parent  57c3f6d2e69264814e7fc2022fe226dc4bbd1621
init_html now makes sure that base_path contains a physical path and no
symbolic links

diff -r 57c3f6d2e692 -r e9ca85a3713c src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Dec 14 12:49:32 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML	Fri Dec 15 12:15:39 1995 +0100
@@ -1045,17 +1045,12 @@
       val theory_list = close_out (open_out ".theory_list.txt");
 
       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";
             val cpure_out = open_out ".CPure_sub.html";
+            val package = relative_path (!base_path) cwd;
         in mk_charthead pure_out "Pure" "Children" false rel_gif_path ""
                         package;
            mk_charthead cpure_out "CPure" "Children" false rel_gif_path ""
@@ -1069,6 +1064,17 @@
   in make_html := true;
      index_path := cwd;
 
+     (*Make sure that base_path contains the physical path and no
+       symbolic links*)
+     cd (!base_path);
+     base_path := pwd();
+     cd cwd;
+
+     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.";
+
      writeln ("Setting path for index.html to " ^ quote cwd ^
               "\nGIF path has been set to " ^ quote (!gif_path));