--- a/src/Pure/Thy/browser_info.ML Fri Oct 10 15:51:14 1997 +0200
+++ b/src/Pure/Thy/browser_info.ML Fri Oct 10 15:51:38 1997 +0200
@@ -59,7 +59,7 @@
(*Path of Isabelle's main (source) directory
FIXME: this value should be provided by isatool!*)
val base_path = ref (
- "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ())))))));
+ "/" ^ space_implode "/" (rev (tl (tl (rev (BAD_space_explode "/" (OS.FileSys.getDir ())))))));
(* copy contents of file *) (* FIXME: move to library?*)
@@ -479,7 +479,7 @@
fun finish_html () = if not (!make_html) then () else
let val tlist_path = tack_on (!index_path) "theory_list.txt";
val theory_list = TextIO.openIn tlist_path;
- val theories = space_explode "\n" (TextIO.inputAll theory_list);
+ val theories = BAD_space_explode "\n" (TextIO.inputAll theory_list);
val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path);
val rel_gif_path = relative_path (!index_path) (gif_path ());
@@ -509,7 +509,7 @@
val subdir =
if inside_isabelle then relative_path (html_path (!base_path)) (!index_path)
else base_name (!index_path);
- val subdirs = space_explode "/" subdir;
+ val subdirs = BAD_space_explode "/" subdir;
(*Look for index.html in superdirectories; stop when Isabelle's
main directory is reached*)
@@ -521,7 +521,7 @@
else ("", n)
end;
val (super_index, level_diff) =
- find_super_index (rev (space_explode "/" (!index_path))) 1;
+ find_super_index (rev (BAD_space_explode "/" (!index_path))) 1;
val level = length subdirs - level_diff;
(*Add link to current directory to 'super' index.html*)
@@ -559,7 +559,7 @@
("<A HREF = \"" ^ relative_path (!index_path) super_index ^
"/index.html\">Back</A> to the index of " ^
(if not inside_isabelle then
- hd (tl (rev (space_explode "/" (!index_path))))
+ hd (tl (rev (BAD_space_explode "/" (!index_path))))
else if level = 0 then "Isabelle logics"
else space_implode "/" (take (level, subdirs))))) ^
"\n" ^
@@ -647,8 +647,8 @@
let val is = TextIO.openIn infile;
val (inp_dir, _) = split_filename infile;
val (outp_dir, _) = split_filename outfile;
- val entries = map (space_explode " ")
- (space_explode "\n" (TextIO.inputAll is));
+ val entries = map (BAD_space_explode " ")
+ (BAD_space_explode "\n" (TextIO.inputAll is));
fun thyfile f = if f = "\"\"" then f else
let val (dir, name) =
@@ -763,8 +763,8 @@
fun exists_entry id infile =
let val is = TextIO.openIn(infile);
- val IDs = map (hd o tl o (space_explode " "))
- (space_explode "\n" (TextIO.inputAll is));
+ val IDs = map (hd o tl o (BAD_space_explode " "))
+ (BAD_space_explode "\n" (TextIO.inputAll is));
val _ = TextIO.closeIn is
in id mem IDs end;