src/Pure/Thy/thy_read.ML

 
 
 (*Read a file specified by thy_file containing theory tname*)
 fun read_thy tname thy_file =
   let
-    val intext = read_file thy_file;
+    val intext = File.read thy_file;
     val outext = ThySyn.parse tname intext;
   in
-    write_file (out_name tname) outext
+    File.write (out_name tname) outext
   end;
 
 
 (*Check if a theory was completly loaded *)
 fun already_loaded thy =

 
 (*Find a file using a list of paths if no absolute or relative path is
   specified.*)
 fun find_file "" name =
       let fun find_it (cur :: paths) =
-                if file_exists (tack_on cur name) then
+                if File.exists (tack_on cur name) then
                   (if cur = "." then name else tack_on cur name)
                 else
                   find_it paths
            | find_it [] = ""
       in find_it (!tmp_loadpath @ !loadpath) end
   | find_file path name =
-      if file_exists (tack_on path name) then tack_on path name
+      if File.exists (tack_on path name) then tack_on path name
                                          else "";
 
 
 (*Get absolute pathnames for a new or already loaded theory *)
 fun get_filenames path name =

             val absolute_path = absolute_path (OS.FileSys.getDir ());
             val thy_file = absolute_path found;
             val (thy_path, _) = split_filename thy_file;
             val found = find_file path (name ^ ".ML");
             val ml_file = if thy_file = "" then absolute_path found
-                          else if file_exists (tack_on thy_path (name ^ ".ML"))
+                          else if File.exists (tack_on thy_path (name ^ ".ML"))
                           then tack_on thy_path (name ^ ".ML")
                           else "";
             val searched_dirs = if path = "" then (!tmp_loadpath @ !loadpath)
                                              else [path]
         in if thy_file = "" andalso ml_file = "" then

        else
          (writeln ("Reading \"" ^ name ^ ".thy\"");
 
           init_thyinfo ();
           read_thy tname thy_file;
-          SymbolInput.use (out_name tname);
+          Use.use (out_name tname);
 
           if not (!delete_tmpfiles) then ()
           else OS.FileSys.remove (out_name tname);
 
           thyfile2html tname abs_path

        set_info tname (Some (file_info thy_file)) None;
                                        (*mark thy_file as successfully loaded*)
 
        if ml_file = "" then ()
        else (writeln ("Reading \"" ^ name ^ ".ML\"");
-             SymbolInput.use ml_file);
+             Use.use ml_file);
 
        (*Store theory again because it could have been redefined*)
        use_strings
          ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
 

        OS.FileSys.chDir old_dir
     end;
 
 in
 
-  val use_dir = gen_use_dir use;
-  val exit_use_dir = gen_use_dir exit_use;
+  val use_dir = gen_use_dir Use.use;
+  val exit_use_dir = gen_use_dir Use.exit_use;
 
 end
 
 end;