# HG changeset patch # User paulson # Date 1114070706 -7200 # Node ID 8fad4bd4e53cf227e86c5f78330148aba1970b5e # Parent 81e9f17823eac71499f182ee670911b9b2eee8d3 improved SML/NJ compatibility, etc. diff -r 81e9f17823ea -r 8fad4bd4e53c src/HOL/Tools/ATP/SpassCommunication.ML --- 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" ) diff -r 81e9f17823ea -r 8fad4bd4e53c src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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 diff -r 81e9f17823ea -r 8fad4bd4e53c src/HOL/Tools/ATP/watcher.ML --- 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