diff -r 000000000000 -r a5a9c433f639 src/Pure/Thy/read.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/read.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,61 @@
+(*  Title:      Pure/Thy/read
+    ID:         $Id$
+    Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
+    Copyright   1992  TU Muenchen
+
+Reading and writing the theory definition files.
+
+For theory XXX, the  input file is called XXX.thy
+                the output file is called .XXX.thy.ML
+                and it then tries to read XXX.ML
+*)
+
+signature READTHY =
+sig
+  val split_filename : string -> string * string
+  val time_use_thy   : string -> unit
+  val use_thy        : string -> unit
+end;
+
+
+functor ReadthyFUN (ThySyn: THYSYN): READTHY =
+struct
+
+(*Convert Unix filename of the form path/file to "path/" and "file" ;
+  if filename contains no slash, then it returns "" and "file" *)
+fun split_filename name =
+  let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name))
+  in  (implode(rev path), implode(rev file)) end;
+
+(*create name of the output ML file for the theory*)
+fun out_name thy = "." ^ thy ^ ".thy.ML";
+
+fun read_thy path thy =
+    let val instream  = open_in (path ^ thy ^ ".thy")
+        val outstream = open_out (path ^ out_name thy)
+    in  output (outstream, ThySyn.read (explode(input(instream, 999999))));
+        close_out outstream;
+        close_in instream
+    end;
+
+fun file_exists file =
+  let val instream = open_in file in close_in instream; true end
+    handle Io _ => false;
+
+(*Use the file if it exists*)
+fun try_use file =
+  if file_exists file then use file else ();
+
+(*Read and convert the theory to a .XXX.thy.ML file and also try to read XXX.ML*)
+fun use_thy name =
+    let val (path,thy) = split_filename name
+    in  read_thy path thy;
+        use (path ^ out_name thy);
+        try_use (path ^ thy ^ ".ML")
+    end;
+
+fun time_use_thy tname = timeit(fn()=>
+   (writeln("\n**** Starting Theory " ^ tname ^ " ****");  use_thy tname;
+    writeln("\n**** Finished Theory " ^ tname ^ " ****")));
+
+end;