src/HOL/Tools/ATP/SpassCommunication.ML
changeset 15658 2edb384bf61f
parent 15642 028059faa963
child 15684 5ec4d21889d6
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Tue Apr 05 16:32:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Wed Apr 06 12:01:37 2005 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  			    then ( 
     1.5                                      let val proofextract = extract_proof (currentString^thisLine)
     1.6                                          val reconstr = spassString_to_reconString (currentString^thisLine) thmstring
     1.7 -                                        val foo =   TextIO.openOut "foobar2";
     1.8 +                                        val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
     1.9                                 in
    1.10                                           TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
    1.11                                     
    1.12 @@ -92,8 +92,8 @@
    1.13                                       (*  end*)
    1.14  
    1.15  fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd) = 
    1.16 -                                       let val spass_proof_file =  TextIO.openAppend("spass_proof")
    1.17 -                                            val  outfile = TextIO.openOut("foo_checkspass");                                                                            
    1.18 +                                       let val spass_proof_file =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
    1.19 +                                            val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
    1.20                                              val _ = TextIO.output (outfile, "checking proof found")
    1.21                                               
    1.22                                              val _ =  TextIO.closeOut outfile
    1.23 @@ -105,7 +105,7 @@
    1.24                                             in if ( thisLine = "SPASS beiseite: Proof found.\n" )
    1.25                                                then      
    1.26                                                (  
    1.27 -                                                 let val  outfile = TextIO.openOut("foo_proof");                                                                                (*val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
    1.28 +                                                 let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
    1.29                                                       val _ = TextIO.output (outfile, (thisLine))
    1.30                                               
    1.31                                                       val _ =  TextIO.closeOut outfile
    1.32 @@ -117,7 +117,7 @@
    1.33                                                     then  
    1.34  
    1.35                                                   (
    1.36 -                                                      let    val  outfile = TextIO.openOut("foo_proof");                                                                               (* val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
    1.37 +                                                      let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  OS.Process.sleep(Time.fromSeconds 3 );*)
    1.38                                                               val _ = TextIO.output (outfile, (thisLine))
    1.39                                               
    1.40                                                               val _ =  TextIO.closeOut outfile
    1.41 @@ -214,7 +214,7 @@
    1.42  fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
    1.43                            then
    1.44                                 let val thisLine = TextIO.inputLine instr 
    1.45 -                                   val  outfile = TextIO.openOut("foo_thisLine");                                                                     val _ = TextIO.output (outfile, (thisLine))
    1.46 +                                   val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
    1.47                                               
    1.48                                     val _ =  TextIO.closeOut outfile
    1.49  			       in 
    1.50 @@ -243,7 +243,7 @@
    1.51  						   let val reconstr = thisLine
    1.52                                                         val thmstring = TextIO.inputLine instr
    1.53                                                         val goalstring = TextIO.inputLine instr
    1.54 -						      val  outfile = TextIO.openOut("foo_getSpass");
    1.55 +						      val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_getSpass")));
    1.56                                      		val _ = TextIO.output (outfile, (thisLine))
    1.57                                       			 val _ =  TextIO.closeOut outfile
    1.58                                                     in