improved SML/NJ compatibility, etc.
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Wed Apr 20 22:43:52 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Thu Apr 21 10:05:06 2005 +0200
@@ -90,7 +90,7 @@
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
(* Attempt to prevent several signals from turning up simultaneously *)
- OS.Process.sleep(Time.fromSeconds 1)
+ Posix.Process.sleep(Time.fromSeconds 1); ()
end
@@ -153,7 +153,7 @@
in if ( thisLine = "SPASS beiseite: Proof found.\n" )
then
(
- let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -165,7 +165,7 @@
then
(
- let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = OS.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -189,7 +189,7 @@
TextIO.flushOut toParent;
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
(* Attempt to prevent several signals from turning up simultaneously *)
- OS.Process.sleep(Time.fromSeconds 1);
+ Posix.Process.sleep(Time.fromSeconds 1);
true
end)
else if ( thisLine = "SPASS beiseite: Ran out of time.\n" )
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Apr 20 22:43:52 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Apr 21 10:05:06 2005 +0200
@@ -15,7 +15,7 @@
(* Versions that include type information *)
fun string_of_thm thm = let val _ = set show_sorts
- val str = string_of_thm thm
+ val str = Display.string_of_thm thm
val no_returns =List.filter not_newline (explode str)
val _ = reset show_sorts
in
@@ -222,9 +222,6 @@
(distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
end
-fun thmstrings [] str = str
-| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
-
fun numclstr (vars, []) str = str
| numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
in
--- a/src/HOL/Tools/ATP/watcher.ML Wed Apr 20 22:43:52 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Thu Apr 21 10:05:06 2005 +0200
@@ -108,7 +108,7 @@
in
goals_being_watched := (!goals_being_watched) + 1;
- OS.Process.sleep(Time.fromSeconds 1);
+ Posix.Process.sleep(Time.fromSeconds 1);
(warning ("probfile is: "^probfile));
(warning("dfg file is: "^newfile));
(warning ("wholefile is: "^(File.sysify_path wholefile)));
@@ -483,7 +483,7 @@
val parentID = Posix.ProcEnv.getppid()
val newProcList' =checkChildren (newProcList, toParentStr)
in
- (*OS.Process.sleep (Time.fromSeconds 1);*)
+ (*Posix.Process.sleep (Time.fromSeconds 1);*)
loop (newProcList')
end
)
@@ -495,7 +495,7 @@
val parentID = Posix.ProcEnv.getppid()
val newProcList' =checkChildren (newProcList, toParentStr)
in
- (*OS.Process.sleep (Time.fromSeconds 1);*)
+ (*Posix.Process.sleep (Time.fromSeconds 1);*)
loop (newProcList')
end
)
@@ -508,7 +508,7 @@
(******************************)
( let val newProcList = checkChildren ((procList), toParentStr)
in
- OS.Process.sleep (Time.fromSeconds 1);
+ Posix.Process.sleep (Time.fromSeconds 1);
loop (newProcList)
end