improved SML/NJ compatibility, etc.
authorpaulson
Thu Apr 21 10:05:06 2005 +0200 (2005-04-21)
changeset 157878fad4bd4e53c
parent 15786 81e9f17823ea
child 15788 ebcbffebdf97
improved SML/NJ compatibility, etc.
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Wed Apr 20 22:43:52 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Apr 21 10:05:06 2005 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4                                            
     1.5                                           Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
     1.6                                           (* Attempt to prevent several signals from turning up simultaneously *)
     1.7 -                                         OS.Process.sleep(Time.fromSeconds 1)
     1.8 +                                         Posix.Process.sleep(Time.fromSeconds 1); ()
     1.9                                                 
    1.10                                      end
    1.11                                        
    1.12 @@ -153,7 +153,7 @@
    1.13                                             in if ( thisLine = "SPASS beiseite: Proof found.\n" )
    1.14                                                then      
    1.15                                                (  
    1.16 -                                                 let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                      (*val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
    1.17 +                                                 let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.18                                                       val _ = TextIO.output (outfile, (thisLine))
    1.19                                               
    1.20                                                       val _ =  TextIO.closeOut outfile
    1.21 @@ -165,7 +165,7 @@
    1.22                                                     then  
    1.23  
    1.24                                                   (
    1.25 -                                                      let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                       (* val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
    1.26 +                                                      let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.27                                                               val _ = TextIO.output (outfile, (thisLine))
    1.28                                               
    1.29                                                               val _ =  TextIO.closeOut outfile
    1.30 @@ -189,7 +189,7 @@
    1.31                                                         TextIO.flushOut toParent;
    1.32                                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.33                                                         (* Attempt to prevent several signals from turning up simultaneously *)
    1.34 -                                                       OS.Process.sleep(Time.fromSeconds 1);
    1.35 +                                                       Posix.Process.sleep(Time.fromSeconds 1);
    1.36                                                          true  
    1.37                                                        end) 
    1.38                                                       else if ( thisLine = "SPASS beiseite: Ran out of time.\n" ) 
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Apr 20 22:43:52 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Apr 21 10:05:06 2005 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  (* Versions that include type information *)
     2.5   
     2.6  fun string_of_thm thm = let val _ = set show_sorts
     2.7 -                                val str = string_of_thm thm
     2.8 +                                val str = Display.string_of_thm thm
     2.9                                  val no_returns =List.filter not_newline (explode str)
    2.10                                  val _ = reset show_sorts
    2.11                              in 
    2.12 @@ -222,9 +222,6 @@
    2.13                                              (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
    2.14                                           end
    2.15                                          
    2.16 -fun thmstrings [] str = str
    2.17 -|   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
    2.18 -
    2.19  fun numclstr (vars, []) str = str
    2.20  |   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
    2.21                                 in
     3.1 --- a/src/HOL/Tools/ATP/watcher.ML	Wed Apr 20 22:43:52 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Apr 21 10:05:06 2005 +0200
     3.3 @@ -108,7 +108,7 @@
     3.4                                         
     3.5                                                        in   
     3.6                                                           goals_being_watched := (!goals_being_watched) + 1;
     3.7 -                                                         OS.Process.sleep(Time.fromSeconds 1); 
     3.8 +                                                         Posix.Process.sleep(Time.fromSeconds 1); 
     3.9                       					(warning ("probfile is: "^probfile));
    3.10                                                           (warning("dfg file is: "^newfile));
    3.11                                                           (warning ("wholefile is: "^(File.sysify_path wholefile)));
    3.12 @@ -483,7 +483,7 @@
    3.13                                                      val parentID = Posix.ProcEnv.getppid()
    3.14                                                      val newProcList' =checkChildren (newProcList, toParentStr) 
    3.15                                                    in
    3.16 -                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
    3.17 +                                                    (*Posix.Process.sleep (Time.fromSeconds 1);*)
    3.18                                                      loop (newProcList') 
    3.19                                                    end
    3.20                                                    )
    3.21 @@ -495,7 +495,7 @@
    3.22                                                      val parentID = Posix.ProcEnv.getppid()
    3.23                                                      val newProcList' =checkChildren (newProcList, toParentStr) 
    3.24                                                    in
    3.25 -                                                    (*OS.Process.sleep (Time.fromSeconds 1);*)
    3.26 +                                                    (*Posix.Process.sleep (Time.fromSeconds 1);*)
    3.27                                                      loop (newProcList') 
    3.28                                                    end
    3.29                                                    )
    3.30 @@ -508,7 +508,7 @@
    3.31                                                                                            (******************************)
    3.32                                          (    let val newProcList = checkChildren ((procList), toParentStr)
    3.33                                               in
    3.34 -                                               OS.Process.sleep (Time.fromSeconds 1);
    3.35 +                                               Posix.Process.sleep (Time.fromSeconds 1);
    3.36                                                 loop (newProcList)
    3.37                                               end
    3.38