# HG changeset patch # User clasohm # Date 823607071 -3600 # Node ID 85ecd3439e019e3b268cc60494aeaa8229c19063 # Parent 21eb5e156d919036afb0d395d161ff235537558e made Isabelle compatible with SML/NJ 1.09 diff -r 21eb5e156d91 -r 85ecd3439e01 src/Pure/Makefile --- 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 diff -r 21eb5e156d91 -r 85ecd3439e01 src/Pure/NJ.ML --- 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; diff -r 21eb5e156d91 -r 85ecd3439e01 src/Pure/NJ093.ML --- /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")); diff -r 21eb5e156d91 -r 85ecd3439e01 src/Pure/NJ1xx.ML --- /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; diff -r 21eb5e156d91 -r 85ecd3439e01 src/Pure/POLY.ML --- 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 = diff -r 21eb5e156d91 -r 85ecd3439e01 src/Pure/Thy/thy_read.ML --- 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 \\__" ^ 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 ()