src/Pure/Thy/browser_info.ML

 
 
 (*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?*)
 
 fun copy_file infile outfile =

 
 (*Generate index.html*)
 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 ());
 
       (*Make entry for main chart of all theories.*)

         then take the last directory of index_path*)
       val inside_isabelle = (!original_path) subdir_of (!base_path);
       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*)
       fun find_super_index [] n = ("", n)
         | find_super_index (p::ps) n =

           in if file_exists (index_path ^ "/index.html") then (index_path, n)
              else if length subdirs - n > 0 then find_super_index ps (n+1)
              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*)
       fun link_directory () =
         let val old_index = TextIO.openIn (super_index ^ "/index.html");

        \View <A HREF=\"" ^ rel_graph_path ^ "\">graph</A> of theories<P>\n" ^
        (if super_index = "" then "" else
         ("<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" ^
        (if file_exists (tack_on (!index_path) "README.html") then
           "<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n"

       (*copy graph file, adjust relative paths for theory files*)
       fun copy_graph infile outfile unfold =
         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) =
                     split_filename (implode (rev (tl (rev (tl (explode f))))));
                   val abs_path = normalize_path (tack_on inp_dir dir);

                 (quote (relative_path (fst (split_filename (!large_graph_file))) thy_file)) ^
                 " > " ^ (space_implode " " (map quote parents)) ^ " ;\n" ;
 
       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;
 
       fun mk_entry outfile entry_str =
         if exists_entry thy_ID outfile then ()