watcher.ML and watcher.sig changed. Debug files now write to tmp.
authorquigley
Wed Apr 06 12:01:37 2005 +0200 (2005-04-06 ago)
changeset 156582edb384bf61f
parent 15657 bd946fbc7c2b
child 15659 043c460af14d
watcher.ML and watcher.sig changed. Debug files now write to tmp.
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/remchars.pl
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/ATP/watcher.sig
     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
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 05 16:32:47 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Apr 06 12:01:37 2005 +0200
     2.3 @@ -254,7 +254,7 @@
     2.4  fun select_literal i cl = negate_head (make_last i cl);
     2.5  
     2.6   fun get_axioms_used proof_steps thmstring = let 
     2.7 -                                             val  outfile = TextIO.openOut("foo_ax_thmstr");                                                                       
     2.8 +                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
     2.9                                               val _ = TextIO.output (outfile, thmstring)
    2.10                                               
    2.11                                               val _ =  TextIO.closeOut outfile
    2.12 @@ -282,11 +282,11 @@
    2.13                                              val meta_strs = map get_meta_lits metas
    2.14                                             
    2.15                                              val metas_and_strs = zip  metas meta_strs
    2.16 -                                             val  outfile = TextIO.openOut("foo_clauses");                                                                       
    2.17 +                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    2.18                                               val _ = TextIO.output (outfile, (onestr ax_strs ""))
    2.19                                               
    2.20                                               val _ =  TextIO.closeOut outfile
    2.21 -                                             val  outfile = TextIO.openOut("foo_metastrs");                                                                       
    2.22 +                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    2.23                                               val _ = TextIO.output (outfile, (onestr meta_strs ""))
    2.24                                               val _ =  TextIO.closeOut outfile
    2.25  
    2.26 @@ -306,12 +306,14 @@
    2.27                                                                           []
    2.28  
    2.29                                             (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    2.30 -                                           val  outfile = TextIO.openOut("foo_metas")
    2.31 +                                           val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
    2.32  
    2.33                                             val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
    2.34                                             val _ =  TextIO.closeOut outfile
    2.35 -                                            val execperl = Unix.execute("/usr/bin/perl", ["remchars2.pl <foo_metas >foo_metas2"])
    2.36 -                                         val infile = TextIO.openIn("foo_metas2")
    2.37 +                                          val foo_metas =  File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
    2.38 +                                          val foo_metas2 =   File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
    2.39 +                                            val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
    2.40 +                                         val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
    2.41                                          val ax_metas_str = TextIO.inputLine (infile)
    2.42                                          val _ = TextIO.closeIn infile
    2.43                                             val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
    2.44 @@ -400,7 +402,7 @@
    2.45  
    2.46  
    2.47  fun spassString_to_reconString proofstr thmstring = 
    2.48 -                                              let val  outfile = TextIO.openOut("thmstringfile");                                                                                      val _= warning("proofstr is: "^proofstr);
    2.49 +                                              let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                                                                      val _= warning("proofstr is: "^proofstr);
    2.50                                                    val _ = warning ("thmstring is: "^thmstring);
    2.51                                                    val _ = TextIO.output (outfile, (thmstring))
    2.52                                                    val _ =  TextIO.closeOut outfile
    2.53 @@ -414,10 +416,10 @@
    2.54                                                    val proof_steps1 = parse tokens
    2.55                                                    val proof_steps = just_change_space proof_steps1
    2.56  
    2.57 -                                                  val  outfile = TextIO.openOut("foo_parse");                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    2.58 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    2.59                                                    val _ =  TextIO.closeOut outfile
    2.60                                                  
    2.61 -                                                  val  outfile = TextIO.openOut("foo_thmstring_at_parse");                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
    2.62 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
    2.63                                                    val _ =  TextIO.closeOut outfile
    2.64                                                (************************************)
    2.65                                                (* recreate original subgoal as thm *)
    2.66 @@ -427,16 +429,16 @@
    2.67                                                    val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thmstring
    2.68                                                    
    2.69                                                    (*val numcls_string = numclstr ( vars, numcls) ""*)
    2.70 -                                                  val  outfile = TextIO.openOut("foo_axiom");                                                                            val _ = TextIO.output (outfile,"got axioms")
    2.71 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
    2.72                                                    val _ =  TextIO.closeOut outfile
    2.73                                                      
    2.74                                                (************************************)
    2.75                                                (* translate proof                  *)
    2.76                                                (************************************)
    2.77 -                                                  val  outfile = TextIO.openOut("foo_steps");                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
    2.78 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps")));                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
    2.79                                                    val _ =  TextIO.closeOut outfile
    2.80                                                    val (newthm,proof) = translate_proof numcls  proof_steps vars
    2.81 -                                                  val  outfile = TextIO.openOut("foo_steps2");                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
    2.82 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps2")));                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
    2.83                                                    val _ =  TextIO.closeOut outfile
    2.84                                                (***************************************************)
    2.85                                                (* transfer necessary steps as strings to Isabelle *)
    2.86 @@ -453,14 +455,14 @@
    2.87                                                    val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
    2.88                                                    val reconExtraAxStr = extraAxs_to_string ( zip extra_nums extra_with_vars) ""
    2.89                                                    val frees_str = "["^(thmvars_to_string frees "")^"]"
    2.90 -                                                  val  outfile = TextIO.openOut("reconstringfile");
    2.91 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
    2.92  
    2.93                                                    val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
    2.94                                                    val _ =  TextIO.closeOut outfile
    2.95                                                in 
    2.96                                                     (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
    2.97                                                end
    2.98 -                                              handle _ => (let val  outfile = TextIO.openOut("foo_handler");
    2.99 +                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   2.100  
   2.101                                                    val _ = TextIO.output (outfile, ("In exception handler"));
   2.102                                                    val _ =  TextIO.closeOut outfile
   2.103 @@ -765,7 +767,7 @@
   2.104                             (isar_lines firststeps "")^
   2.105                             (last_isar_line laststep)^
   2.106                             ("qed")
   2.107 -                          val  outfile = TextIO.openOut("isar_proof_file");
   2.108 +                          val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
   2.109  
   2.110                                                    val _ = TextIO.output (outfile, isar_proof)
   2.111                                                    val _ =  TextIO.closeOut outfile
   2.112 @@ -801,7 +803,7 @@
   2.113  
   2.114                                     val (frees,recon_steps) = parse_step tokens 
   2.115                                     val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   2.116 -                                   val foo =   TextIO.openOut "foobar";
   2.117 +                                   val foo =   TextIO.openOut (File.sysify_path(File.tmp_path (Path.basic "foobar")));
   2.118                                 in 
   2.119                                    TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
   2.120                                 end 
     3.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue Apr 05 16:32:47 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Wed Apr 06 12:01:37 2005 +0200
     3.3 @@ -437,7 +437,7 @@
     3.4                                val thmproofstring = proofstring ( thmstring)
     3.5                              val no_returns =List.filter  not_newline ( thmproofstring)
     3.6                              val thmstr = implode no_returns
     3.7 -                               val outfile = TextIO.openOut("thml_file")
     3.8 +                               val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
     3.9                                 val _ = TextIO.output(outfile, "thmstr is "^thmstr)
    3.10                                 val _ = TextIO.flushOut outfile;
    3.11                                 val _ =  TextIO.closeOut outfile
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/ATP/remchars.pl	Wed Apr 06 12:01:37 2005 +0200
     4.3 @@ -0,0 +1,31 @@
     4.4 +#!/usr/bin/perl
     4.5 +#
     4.6 +# isa2tex.pl - Converts isabelle formulae into LaTeX
     4.7 +# A complete hack - needs more work.
     4.8 +#
     4.9 +# by Michael Dales (michael@dcs.gla.ac.uk)
    4.10 +
    4.11 +# Begin math mode
    4.12 +#printf "\$";
    4.13 +#ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa# | P x)((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((AL#L x::'a::type. ~ P x) | ~ P (xb::'a::type))
    4.14 +#perhaps change to all chars not in alphanumeric or a few symbols?
    4.15 +
    4.16 +while (<STDIN>)
    4.17 +{
    4.18 +
    4.19 +    #chop();
    4.20 +    s%\n$%%;
    4.21 +    s%%%g;
    4.22 +    s%%%g;
    4.23 +    s%%%g;
    4.24 +    s%%%g;
    4.25 +    s%%%g;
    4.26 +    s%%%g;
    4.27 +    
    4.28 +    #printf "$_\\newline\n";
    4.29 +    printf "$_";
    4.30 +}
    4.31 +
    4.32 +# End math mode
    4.33 +#printf "\$\n";
    4.34 +#printf "\\end{tabbing}\n";
     5.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue Apr 05 16:32:47 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Wed Apr 06 12:01:37 2005 +0200
     5.3 @@ -97,7 +97,7 @@
     5.4                                                       let 
     5.5                                                          val dfg_dir = File.tmp_path (Path.basic "dfg");
     5.6                                                          (* need to check here if the directory exists and, if not, create it*)
     5.7 -                                                         val  outfile = TextIO.openAppend("thmstring_in_watcher");                                                                                    
     5.8 +                                                         val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                                    
     5.9                                                           val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    5.10                                                           val _ =  TextIO.closeOut outfile
    5.11                                                           val dfg_create =if File.exists dfg_dir 
    5.12 @@ -172,7 +172,7 @@
    5.13                                val settings = getSettings settings []
    5.14                                val (file, rest) =  takeUntil "*" rest []
    5.15                                val file = implode file
    5.16 -                              val  outfile = TextIO.openOut("sep_comms");                                                                                    
    5.17 +                              val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "sep_comms")));                                                                                    
    5.18                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
    5.19                                val _ =  TextIO.closeOut outfile
    5.20                                
    5.21 @@ -248,7 +248,7 @@
    5.22  
    5.23  
    5.24  
    5.25 -fun setupWatcher (the_goal) = let
    5.26 +fun setupWatcher () = let
    5.27            (** pipes for communication between parent and watcher **)
    5.28            val p1 = Posix.IO.pipe ()
    5.29            val p2 = Posix.IO.pipe ()
    5.30 @@ -275,10 +275,10 @@
    5.31                        val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    5.32                        val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    5.33                        val toParentStr = openOutFD ("_exec_out_parent", toParent)
    5.34 -                      val goalstr = string_of_thm (the_goal)
    5.35 -                       val  outfile = TextIO.openOut("goal_in_watcher");  
    5.36 +                      (*val goalstr = string_of_thm (the_goal)
    5.37 +                       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    5.38                        val _ = TextIO.output (outfile,goalstr )
    5.39 -                      val _ =  TextIO.closeOut outfile
    5.40 +                      val _ =  TextIO.closeOut outfile*)
    5.41                        fun killChildren [] = ()
    5.42                     |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
    5.43  
    5.44 @@ -354,7 +354,7 @@
    5.45                                                  val prover = cmdProver childProc
    5.46                                                  val thmstring = cmdThm childProc
    5.47                                                  val goalstring = cmdGoal childProc
    5.48 -                                                val  outfile = TextIO.openOut("child_comms");  
    5.49 +                                                val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
    5.50                                                  val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
    5.51                                                  val _ =  TextIO.closeOut outfile
    5.52                                              in 
    5.53 @@ -362,7 +362,7 @@
    5.54                                                then 
    5.55                                                    (* check here for prover label on child*)
    5.56                                                     
    5.57 -                                                  let val  outfile = TextIO.openOut("child_incoming");  
    5.58 +                                                  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
    5.59                                                  val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
    5.60                                                  val _ =  TextIO.closeOut outfile
    5.61                                                val childDone = (case prover of
    5.62 @@ -385,7 +385,7 @@
    5.63                                                           (childProc::(checkChildren (otherChildren, toParentStr)))
    5.64                                                   end
    5.65                                                 else
    5.66 -                                                   let val  outfile = TextIO.openAppend("child_incoming");  
    5.67 +                                                   let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
    5.68                                                  val _ = TextIO.output (outfile,"No child output " )
    5.69                                                  val _ =  TextIO.closeOut outfile
    5.70                                                   in
    5.71 @@ -578,7 +578,7 @@
    5.72  (**********************************************************)
    5.73  fun killWatcher pid= killChild pid;
    5.74  
    5.75 -fun createWatcher (the_goal) = let val mychild = childInfo (setupWatcher(the_goal))
    5.76 +fun createWatcher () = let val mychild = childInfo (setupWatcher())
    5.77  			   val streams =snd mychild
    5.78                             val childin = fst streams
    5.79                             val childout = snd streams
    5.80 @@ -590,7 +590,7 @@
    5.81                            
    5.82                            (* fun spass_proofHandler (n:int) = (
    5.83                                                        let val (reconstr, thmstring, goalstring) = getSpassInput childin
    5.84 -                                                          val  outfile = TextIO.openOut("foo_signal");
    5.85 +                                                          val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
    5.86  
    5.87                                                           val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring))
    5.88                                                           val _ =  TextIO.closeOut outfile
    5.89 @@ -605,12 +605,12 @@
    5.90  (*
    5.91  
    5.92  fun spass_proofHandler (n:int) = (
    5.93 -                                                      let  val  outfile = TextIO.openOut("foo_signal1");
    5.94 +                                                      let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
    5.95  
    5.96                                                           val _ = TextIO.output (outfile, ("In signal handler now\n"))
    5.97                                                           val _ =  TextIO.closeOut outfile
    5.98                                                            val (reconstr, thmstring, goalstring) = getSpassInput childin
    5.99 -                                                         val  outfile = TextIO.openOut("foo_signal");
   5.100 +                                                         val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   5.101  
   5.102                                                           val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring^goalstring))
   5.103                                                           val _ =  TextIO.closeOut outfile
   5.104 @@ -637,11 +637,11 @@
   5.105  *)
   5.106  
   5.107  fun spass_proofHandler (n:int) = (
   5.108 -                                 let  val  outfile = TextIO.openOut("foo_signal1");
   5.109 +                                 let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
   5.110                                        val _ = TextIO.output (outfile, ("In signal handler now\n"))
   5.111                                        val _ =  TextIO.closeOut outfile
   5.112                                        val (reconstr, thmstring, goalstring) = getSpassInput childin
   5.113 -                                      val  outfile = TextIO.openAppend("foo_signal");
   5.114 +                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   5.115  
   5.116                                        val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   5.117                                        val _ =  TextIO.closeOut outfile
   5.118 @@ -658,7 +658,7 @@
   5.119                                                           
   5.120                                                                   if ((!goals_being_watched) = 0)
   5.121                                                                   then 
   5.122 -                                                                    (let val  outfile = TextIO.openOut("foo_reap_found");
   5.123 +                                                                    (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
   5.124                                                                           val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   5.125                                                                           val _ =  TextIO.closeOut outfile
   5.126                                                                       in
   5.127 @@ -677,7 +677,7 @@
   5.128                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
   5.129                                                                        if (!goals_being_watched = 0)
   5.130                                                                        then 
   5.131 -                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
   5.132 +                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   5.133                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   5.134                                                                                 val _ =  TextIO.closeOut outfile
   5.135                                                                             in
   5.136 @@ -696,7 +696,7 @@
   5.137                                                                        Pretty.writeln(Pretty.str  (oct_char "361"));
   5.138                                                                        if (!goals_being_watched = 0)
   5.139                                                                        then 
   5.140 -                                                                          (let val  outfile = TextIO.openOut("foo_reap_comp");
   5.141 +                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   5.142                                                                                 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   5.143                                                                                 val _ =  TextIO.closeOut outfile
   5.144                                                                             in
     6.1 --- a/src/HOL/Tools/ATP/watcher.sig	Tue Apr 05 16:32:47 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/watcher.sig	Wed Apr 06 12:01:37 2005 +0200
     6.3 @@ -37,7 +37,7 @@
     6.4  (* Start a watcher and set up signal handlers             *)
     6.5  (**********************************************************)
     6.6  
     6.7 -val createWatcher : thm  -> TextIO.instream * TextIO.outstream * Posix.Process.pid
     6.8 +val createWatcher : unit -> TextIO.instream * TextIO.outstream * Posix.Process.pid
     6.9  
    6.10  
    6.11