# 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 "") ^
"