src/Pure/POLY.ML
author wenzelm
Mon Oct 04 15:36:31 1993 +0100 (1993-10-04 ago)
changeset 19 929ad32d63fc
parent 0 a5a9c433f639
child 58 b30802dfbe80
permissions -rw-r--r--
Pure/ROOT.ML
cleaned comments;
removed extraneous 'print_depth 1';
replaced Basic_Syntax by BasicSyntax
added 'use "install_pp.ML"';

Pure/README
fixed comments;

Pure/POLY.ML
Pure/NJ.ML
make_pp: added fbrk;

Pure/install_pp.ML
replaced "Ast" by "Syntax";

Pure/sign.ML
added 'quote' to some error msgs;
clasohm@0
     1
(*  Title:      Pure/POLY
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Compatibility file for Poly/ML (AHL release 1.88)
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open PolyML ExtendedIO;
clasohm@0
    10
clasohm@0
    11
clasohm@0
    12
(*A conditional timing function: applies f to () and, if the flag is true,
clasohm@0
    13
  prints its runtime.*)
clasohm@0
    14
clasohm@0
    15
fun cond_timeit flag f =
clasohm@0
    16
  if flag then
clasohm@0
    17
    let val before = System.processtime()
clasohm@0
    18
        val result = f()
clasohm@0
    19
        val both = real(System.processtime() - before) / 10.0
clasohm@0
    20
    in  output(std_out, "Process time (incl GC): "^
clasohm@0
    21
                         makestring both ^ " secs\n");
clasohm@0
    22
        result
clasohm@0
    23
    end
clasohm@0
    24
  else f();
clasohm@0
    25
clasohm@0
    26
clasohm@0
    27
(*Save function: in Poly/ML, ignores filename and commits to present file*)
clasohm@0
    28
clasohm@0
    29
fun xML filename banner = commit();
clasohm@0
    30
clasohm@0
    31
clasohm@0
    32
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
clasohm@0
    33
clasohm@0
    34
fun make_pp _ pprint (str, blk, brk, en) obj =
wenzelm@19
    35
  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
wenzelm@19
    36
    fn () => brk (99999, 0), en);
clasohm@0
    37
clasohm@0
    38
clasohm@0
    39
(*** File information ***)
clasohm@0
    40
clasohm@0
    41
(*Get time of last modification.*)
clasohm@0
    42
fun file_info "" = ""
clasohm@0
    43
  | file_info name =
clasohm@0
    44
        let val (is, os) = ExtendedIO.execute ("ls -l " ^ name)
clasohm@0
    45
            val result = ExtendedIO.input_line is;
clasohm@0
    46
            val dummy = close_in is;
clasohm@0
    47
            val dummy = close_out os;
clasohm@0
    48
        in result end;
clasohm@0
    49