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