src/Pure/Thy/read.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 74 208ab8773a73
permissions -rw-r--r--
Initial revision
     1 (*  Title:      Pure/Thy/read
     2     ID:         $Id$
     3     Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
     4     Copyright   1992  TU Muenchen
     5 
     6 Reading and writing the theory definition files.
     7 
     8 For theory XXX, the  input file is called XXX.thy
     9                 the output file is called .XXX.thy.ML
    10                 and it then tries to read XXX.ML
    11 *)
    12 
    13 signature READTHY =
    14 sig
    15   val split_filename : string -> string * string
    16   val time_use_thy   : string -> unit
    17   val use_thy        : string -> unit
    18 end;
    19 
    20 
    21 functor ReadthyFUN (ThySyn: THYSYN): READTHY =
    22 struct
    23 
    24 (*Convert Unix filename of the form path/file to "path/" and "file" ;
    25   if filename contains no slash, then it returns "" and "file" *)
    26 fun split_filename name =
    27   let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name))
    28   in  (implode(rev path), implode(rev file)) end;
    29 
    30 (*create name of the output ML file for the theory*)
    31 fun out_name thy = "." ^ thy ^ ".thy.ML";
    32 
    33 fun read_thy path thy =
    34     let val instream  = open_in (path ^ thy ^ ".thy")
    35         val outstream = open_out (path ^ out_name thy)
    36     in  output (outstream, ThySyn.read (explode(input(instream, 999999))));
    37         close_out outstream;
    38         close_in instream
    39     end;
    40 
    41 fun file_exists file =
    42   let val instream = open_in file in close_in instream; true end
    43     handle Io _ => false;
    44 
    45 (*Use the file if it exists*)
    46 fun try_use file =
    47   if file_exists file then use file else ();
    48 
    49 (*Read and convert the theory to a .XXX.thy.ML file and also try to read XXX.ML*)
    50 fun use_thy name =
    51     let val (path,thy) = split_filename name
    52     in  read_thy path thy;
    53         use (path ^ out_name thy);
    54         try_use (path ^ thy ^ ".ML")
    55     end;
    56 
    57 fun time_use_thy tname = timeit(fn()=>
    58    (writeln("\n**** Starting Theory " ^ tname ^ " ****");  use_thy tname;
    59     writeln("\n**** Finished Theory " ^ tname ^ " ****")));
    60 
    61 end;