src/Pure/Thy/thy_read.ML
changeset 1378 042899454032
parent 1368 f00280dff0dc
child 1386 cf066d9b4c4f
     1.1 --- a/src/Pure/Thy/thy_read.ML	Fri Dec 01 12:22:07 1995 +0100
     1.2 +++ b/src/Pure/Thy/thy_read.ML	Fri Dec 01 12:24:06 1995 +0100
     1.3 @@ -1104,8 +1104,7 @@
     1.4        val subdirs = space_explode "/" subdir;
     1.5  
     1.6        (*Look for index.html in superdirectories*)
     1.7 -      fun find_super_index [] _ =
     1.8 -            error "finish_html: Unable to find super index file."
     1.9 +      fun find_super_index [] n = ("", n)
    1.10          | find_super_index (p::ps) n =
    1.11            let val index_path = "/" ^ space_implode "/" (rev ps);
    1.12            in if file_exists (index_path ^ "/index.html") then (index_path, n)
    1.13 @@ -1138,11 +1137,12 @@
    1.14         \<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
    1.15         \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
    1.16         \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
    1.17 -       \\" ALT = /\\></A> stands for supertheories (parent theories)\
    1.18 -       \<P>\n<A HREF = \"" ^ relative_path (!index_path) super_index ^ 
    1.19 -       "/index.html\">Back</A> to the index of " ^
    1.20 -       (if level = 0 then "Isabelle logics"
    1.21 -        else space_implode "/" (take (level, subdirs))) ^
    1.22 +       \\" ALT = /\\></A> stands for supertheories (parent theories)" ^
    1.23 +       (if super_index = "" then "" else
    1.24 +        ("<P>\n<A HREF = \"" ^ relative_path (!index_path) super_index ^ 
    1.25 +         "/index.html\">Back</A> to the index of " ^
    1.26 +         (if level = 0 then "Isabelle logics"
    1.27 +          else space_implode "/" (take (level, subdirs))))) ^
    1.28         "\n" ^
    1.29         (if file_exists (tack_on (!index_path) "README.html") then
    1.30            "<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n"
    1.31 @@ -1151,7 +1151,7 @@
    1.32          else "") ^
    1.33         "<HR>" ^ implode (map main_entry theories) ^ "<!-->");
    1.34       close_out out;
    1.35 -     if level = 0 then () else link_directory ()
    1.36 +     if super_index = "" orelse level = 0 then () else link_directory ()
    1.37    end;
    1.38  
    1.39  
    1.40 @@ -1180,9 +1180,7 @@
    1.41                     thy_ss = thy_ss, simpset = simpset,
    1.42                     datatypes = (name, cons) :: datatypes}
    1.43        | None => error "store_datatype: theory not found";
    1.44 -  in
    1.45 -writeln ("*** Storing datatype " ^ name ^ " (" ^ commas cons ^ ") for theory " ^ (!cur_thyname));
    1.46 -     loaded_thys := Symtab.update ((!cur_thyname, tinfo), !loaded_thys) end;
    1.47 +  in loaded_thys := Symtab.update ((!cur_thyname, tinfo), !loaded_thys) end;
    1.48  
    1.49  fun datatypes_of thy =
    1.50    let val (_, ThyInfo {datatypes, ...}) = thyinfo_of_sign (sign_of thy);