--- a/src/Pure/Makefile Tue Feb 06 12:42:31 1996 +0100
+++ b/src/Pure/Makefile Tue Feb 06 12:44:31 1996 +0100
@@ -24,7 +24,7 @@
FILES = POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
sequence.ML envir.ML pattern.ML unify.ML logic.ML thm.ML net.ML\
drule.ML tctical.ML tactic.ML goals.ML axclass.ML install_pp.ML\
- ../Provers/simplifier.ML
+ NJ093.ML NJ1xx.ML ../Provers/simplifier.ML
SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\
Syntax/parser.ML Syntax/type_ext.ML Syntax/syn_trans.ML\
@@ -39,14 +39,14 @@
case "$(COMP)" in \
poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
- echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' | $(COMP) $(BIN)/Pure;;\
+ echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
+ | $(COMP) $(BIN)/Pure;;\
sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
then echo Bad value for ISABELLEBIN: \
$(BIN) is not a writable directory; \
exit 1; \
fi;\
- echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;'\
- | $(COMP);;\
+ echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;' | $(COMP);;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml;;\
esac
--- a/src/Pure/NJ.ML Tue Feb 06 12:42:31 1996 +0100
+++ b/src/Pure/NJ.ML Tue Feb 06 12:44:31 1996 +0100
@@ -6,42 +6,19 @@
Compatibility file for Standard ML of New Jersey.
*)
-(*** Poly/ML emulation ***)
-(*To exit the system with an exit code -- an alternative to ^D *)
-val exit = System.Unsafe.CInterface.exit;
-fun quit () = exit 0;
+(*Determine if we are running under 0.93 or a newer version of SML/NJ
+ This is based on the variable "version" defined in 0.93's System structure
+ which is no longer present in 1.09.*)
-(*To change the current directory*)
-val cd = System.Directory.cd;
+local val version = ""; open System in
+ val smlversion = if version <> "" then 93 else 109
+end;
-(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
-fun print_depth n = (System.Control.Print.printDepth := n div 2;
- System.Control.Print.printLength := n);
+use (if smlversion = 93 then "NJ093.ML" else "NJ1xx.ML");
-(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
-
-fun make_pp path pprint =
- let
- open System.PrettyPrint;
-
- fun pp pps obj =
- pprint obj
- (add_string pps, begin_block pps INCONSISTENT,
- fn wd => add_break pps (wd, 0), fn () => add_newline pps,
- fn () => end_block pps);
- in
- (path, pp)
- end;
-
-fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
-
-
-(*** New Jersey ML parameters ***)
-
-(* Suppresses Garbage Collection messages; default was 2 *)
-System.Control.Runtime.gcmessages := 0;
+(** Other functions which are not specific to 0.93 or 1.xx*)
(*redefine to flush its output immediately -- temporary patch suggested
by Kim Dam Petersen*)
@@ -49,72 +26,3 @@
(*Dummy version of the Poly/ML function*)
fun commit() = ();
-
-(*For use in Makefiles -- saves space*)
-fun xML filename banner = (exportML filename; print(banner^"\n"));
-
-(*** Timing functions ***)
-
-(*Print microseconds, suppressing trailing zeroes*)
-fun umakestring 0 = ""
- | umakestring n = chr(ord"0" + n div 100000) ^
- umakestring(10 * (n mod 100000));
-
-(*A conditional timing function: applies f to () and, if the flag is true,
- prints its runtime. *)
-fun cond_timeit flag f =
- if flag then
- let fun string_of_time (System.Timer.TIME {sec, usec}) =
- makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
- open System.Timer;
- val start = start_timer()
- val result = f();
- val nongc = check_timer(start)
- and gc = check_timer_gc(start);
- val both = add_time(nongc, gc)
- in print("Non GC " ^ string_of_time nongc ^
- " GC " ^ string_of_time gc ^
- " both "^ string_of_time both ^ " secs\n");
- result
- end
- else f();
-
-
-(*** File handling ***)
-
-(*Get time of last modification.*)
-local
- open System.Timer;
- open System.Unsafe.SysIO;
-in
- fun file_info "" = ""
- | file_info name = makestring (mtime (PATH name));
-
- val delete_file = unlink;
-end;
-
-(*Get pathname of current working directory *)
-fun pwd () = System.Directory.getWD ();
-
-
-(*** ML command execution ***)
-
-fun use_string commands =
- System.Compile.use_stream (open_string (implode commands));
-
-
-(*** System command execution ***)
-
-(*Execute an Unix command which doesn't take any input from stdin and
- sends its output to stdout.
- This could be done more easily by IO.execute, but that function
- seems to be buggy in SML/NJ 0.93.*)
-fun execute command =
- let val tmp_name = "isa_converted.tmp"
- val is = (System.system (command ^ " > " ^ tmp_name);
- open_in tmp_name);
- val result = input (is, 999999);
- in close_in is;
- delete_file tmp_name;
- result
- end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/NJ093.ML Tue Feb 06 12:44:31 1996 +0100
@@ -0,0 +1,115 @@
+(* Title: Pure/NJ093.ML
+ ID: $Id$
+ Author: Carsten Clasohm, TU Muenchen
+ Copyright 1996 TU Muenchen
+
+Compatibility file for Standard ML of New Jersey version 0.93.
+*)
+
+(*** Poly/ML emulation ***)
+
+
+(*To exit the system with an exit code -- an alternative to ^D *)
+val exit = System.Unsafe.CInterface.exit;
+fun quit () = exit 0;
+
+(*To change the current directory*)
+val cd = System.Directory.cd;
+
+(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
+fun print_depth n = (System.Control.Print.printDepth := n div 2;
+ System.Control.Print.printLength := n);
+
+(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
+
+fun make_pp path pprint =
+ let
+ open System.PrettyPrint;
+
+ fun pp pps obj =
+ pprint obj
+ (add_string pps, begin_block pps INCONSISTENT,
+ fn wd => add_break pps (wd, 0), fn () => add_newline pps,
+ fn () => end_block pps);
+ in
+ (path, pp)
+ end;
+
+fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
+
+
+(*** New Jersey ML parameters ***)
+
+(* Suppresses Garbage Collection messages; default was 2 *)
+System.Control.Runtime.gcmessages := 0;
+
+
+(*** Timing functions ***)
+
+(*Print microseconds, suppressing trailing zeroes*)
+fun umakestring 0 = ""
+ | umakestring n = chr(ord "0" + n div 100000) ^
+ umakestring(10 * (n mod 100000));
+
+(*A conditional timing function: applies f to () and, if the flag is true,
+ prints its runtime. *)
+fun cond_timeit flag f =
+ if flag then
+ let fun string_of_time (System.Timer.TIME {sec, usec}) =
+ makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
+ open System.Timer;
+ val start = start_timer()
+ val result = f();
+ val nongc = check_timer(start)
+ and gc = check_timer_gc(start);
+ val both = add_time(nongc, gc)
+ in print("Non GC " ^ string_of_time nongc ^
+ " GC " ^ string_of_time gc ^
+ " both "^ string_of_time both ^ " secs\n");
+ result
+ end
+ else f();
+
+
+(*** File handling ***)
+
+(*Get time of last modification; if file doesn't exist return an empty string*)
+local
+ open System.Timer;
+ open System.Unsafe.SysIO;
+in
+ fun file_info "" = ""
+ | file_info name = makestring (mtime (PATH name)) handle _ => "";
+
+ val delete_file = unlink;
+end;
+
+(*Get pathname of current working directory *)
+fun pwd () = System.Directory.getWD ();
+
+
+(*** ML command execution ***)
+
+fun use_string commands =
+ System.Compile.use_stream (open_string (implode commands));
+
+
+(*** System command execution ***)
+
+(*Execute an Unix command which doesn't take any input from stdin and
+ sends its output to stdout.
+ This could be done more easily by IO.execute, but that function
+ seems to be buggy in SML/NJ 0.93.*)
+fun execute command =
+ let val tmp_name = "isa_converted.tmp"
+ val is = (System.system (command ^ " > " ^ tmp_name);
+ open_in tmp_name);
+ val result = input (is, 999999);
+ in close_in is;
+ delete_file tmp_name;
+ result
+ end;
+
+
+(*For use in Makefiles -- saves space*)
+fun xML filename banner = (exportML filename; print(banner^"\n"));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/NJ1xx.ML Tue Feb 06 12:44:31 1996 +0100
@@ -0,0 +1,132 @@
+(* Title: Pure/NJ1xx.ML
+ ID: $Id$
+ Author: Carsten Clasohm, TU Muenchen
+ Copyright 1996 TU Muenchen
+
+Compatibility file for Standard ML of New Jersey version 1.xx.
+*)
+
+(*** Poly/ML emulation ***)
+
+
+(*To exit the system with an exit code -- an alternative to ^D *)
+fun exit 0 = OS.Process.exit OS.Process.success
+ | exit _ = OS.Process.exit OS.Process.failure;
+fun quit () = exit 0;
+
+(*To change the current directory*)
+val cd = OS.FileSys.chDir;
+
+(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
+fun print_depth n = (Compiler.Control.Print.printDepth := n div 2;
+ Compiler.Control.Print.printLength := n);
+
+(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
+
+fun make_pp path pprint =
+ let
+ open Compiler.PrettyPrint;
+
+ fun pp pps obj =
+ pprint obj
+ (add_string pps, begin_block pps INCONSISTENT,
+ fn wd => add_break pps (wd, 0), fn () => add_newline pps,
+ fn () => end_block pps);
+ in
+ (path, pp)
+ end;
+
+fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;
+
+
+(*** New Jersey ML parameters ***)
+
+(* Suppresses Garbage Collection messages; doesn't work yet *)
+(*System.Runtime.gc 0;*)
+
+val _ = (Compiler.Control.Print.printLength := 1000;
+ Compiler.Control.Print.printDepth := 350;
+ Compiler.Control.Print.stringDepth := 250;
+ Compiler.Control.Print.signatures := 2);
+
+(*** Character/string functions which are compatibel with 0.93 and Poly/ML ***)
+
+val ord = Char.ord o hd o explode;
+val chr = str o Char.chr;
+val explode = (map str) o String.explode;
+val implode = String.concat;
+
+
+(*** Timing functions ***)
+
+(*A conditional timing function: applies f to () and, if the flag is true,
+ prints its runtime. *)
+fun cond_timeit flag f =
+ if flag then
+ let fun string_of_time t = Time.toString(t)
+ open Timer;
+ open Time;
+ val start = startCPUTimer()
+ val result = f();
+ val {gc=gct,sys=syst,usr=usrt} = checkCPUTimer(start)
+ in print("Non GC " ^ string_of_time usrt ^
+ " GC " ^ string_of_time gct ^
+ " both+sys "^ string_of_time (syst+usrt+gct) ^ " secs\n");
+ result
+ end
+ else f();
+
+
+(*** File handling ***)
+
+(*Get time of last modification; if file doesn't exist return an empty string*)
+local
+ open Timer;
+ open Posix.FileSys;
+in
+ fun file_info "" = ""
+ | file_info name = Time.toString (ST.mtime (stat name)) handle _ => "";
+
+ val delete_file = unlink;
+end;
+
+(*Get pathname of current working directory *)
+fun pwd () = OS.FileSys.getDir ();
+
+
+(*** ML command execution ***)
+
+fun use_string commands =
+ Compiler.Interact.use_stream (open_string (implode commands));
+
+
+(*** System command execution ***)
+
+(*Execute an Unix command which doesn't take any input from stdin and
+ sends its output to stdout.
+ This could be done more easily by Unix.execute, but that function
+ doesn't use the PATH.*)
+fun execute command =
+ let val tmp_name = "isa_converted.tmp"
+ val is = (OS.Process.system (command ^ " > " ^ tmp_name);
+ open_in tmp_name);
+ val result = input (is, 999999);
+ in close_in is;
+ delete_file tmp_name;
+ result
+ end;
+
+
+(*For use in Makefiles -- saves space*)
+fun xML filename banner =
+ let val runtime = List.hd (SMLofNJ.getAllArgs())
+ val exec_file = IO.open_out filename
+ val _ = IO.output (exec_file,
+ String.concat
+ ["#!/bin/sh\n",
+ runtime, " @SMLload=", filename, ".heap\n"])
+ val _ = IO.close_out exec_file;
+ val _ = OS.Process.system ("chmod a+x " ^ filename)
+ in exportML (filename^".heap");
+ print(banner^"\n")
+ end;
--- a/src/Pure/POLY.ML Tue Feb 06 12:42:31 1996 +0100
+++ b/src/Pure/POLY.ML Tue Feb 06 12:44:31 1996 +0100
@@ -66,10 +66,9 @@
in
-(*Get a string containing the time of last modification, attributes, owner
- and size of file (but not the path) *)
+(*Get time of last modification; if file doesn't exist return an empty string*)
fun file_info "" = ""
- | file_info name = radixstring (System.filedate name);
+ | file_info name = radixstring (System.filedate name) handle _ => "";
(*Delete a file *)
fun delete_file name =
--- a/src/Pure/Thy/thy_read.ML Tue Feb 06 12:42:31 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML Tue Feb 06 12:44:31 1996 +0100
@@ -197,9 +197,7 @@
close_in instream
end;
-fun file_exists file =
- let val instream = open_in file in close_in instream; true end
- handle Io _ => false;
+fun file_exists file = (file_info file <> "");
(*Get thy_info for a loaded theory *)
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
@@ -651,6 +649,7 @@
(*Add theory to file listing all loaded theories (for index.html)
and to the sub-charts of its parents*)
+ local exception MK_HTML in
fun mk_html () =
let val new_parents = parents_of_name tname \\ old_parents;
@@ -674,7 +673,7 @@
open_append fname handle Io s =>
(writeln ("Warning: Unable to write to file ." ^
fname); raise Io s)
- else raise Io "File not found";
+ else raise MK_HTML;
in output (out,
" |\n \\__<A HREF=\"" ^
tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^
@@ -694,6 +693,7 @@
robust_seq add_to_parents new_parents
end
+ end
in if thy_uptodate andalso ml_uptodate then ()
else
(if thy_file = "" then ()