# HG changeset patch # User clasohm # Date 817817046 -3600 # Node ID 0428994540327b6efd0b7d728f4efa9567f588eb # Parent f800f533aa83b8c2e66070473b7699fe34729b37 removed debugging message; link to non-existing super index is now omitted silently diff -r f800f533aa83 -r 042899454032 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Fri Dec 01 12:22:07 1995 +0100 +++ b/src/Pure/Thy/thy_read.ML Fri Dec 01 12:24:06 1995 +0100 @@ -1104,8 +1104,7 @@ val subdirs = space_explode "/" subdir; (*Look for index.html in superdirectories*) - fun find_super_index [] _ = - error "finish_html: Unable to find super index file." + fun find_super_index [] n = ("", n) | 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) @@ -1138,11 +1137,12 @@ \\\/ stands for subtheories (child theories)
\n\ \/\\ stands for supertheories (parent theories)\ - \

\nBack to the index of " ^ - (if level = 0 then "Isabelle logics" - else space_implode "/" (take (level, subdirs))) ^ + \\" ALT = /\\> stands for supertheories (parent theories)" ^ + (if super_index = "" then "" else + ("

\nBack to the index of " ^ + (if level = 0 then "Isabelle logics" + else space_implode "/" (take (level, subdirs))))) ^ "\n" ^ (if file_exists (tack_on (!index_path) "README.html") then "
View the ReadMe file.\n" @@ -1151,7 +1151,7 @@ else "") ^ "


" ^ implode (map main_entry theories) ^ ""); close_out out; - if level = 0 then () else link_directory () + if super_index = "" orelse level = 0 then () else link_directory () end; @@ -1180,9 +1180,7 @@ thy_ss = thy_ss, simpset = simpset, datatypes = (name, cons) :: datatypes} | None => error "store_datatype: theory not found"; - in -writeln ("*** Storing datatype " ^ name ^ " (" ^ commas cons ^ ") for theory " ^ (!cur_thyname)); - loaded_thys := Symtab.update ((!cur_thyname, tinfo), !loaded_thys) end; + in loaded_thys := Symtab.update ((!cur_thyname, tinfo), !loaded_thys) end; fun datatypes_of thy = let val (_, ThyInfo {datatypes, ...}) = thyinfo_of_sign (sign_of thy);