File.platform_path;
authorwenzelm
Sun Jun 05 11:31:22 2005 +0200 (2005-06-05)
changeset 16259aed1a8ae4b23
parent 16258 f3d913abf7e5
child 16260 4a1f36eafe17
File.platform_path;
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/res_atp.ML
src/Pure/proof_general.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Sun Jun 05 11:31:21 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Sun Jun 05 11:31:22 2005 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  
     1.5  
     1.6  fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr  (num_of_clauses:int ) = 
     1.7 - let val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar3")));
     1.8 + let val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3")));
     1.9   in
    1.10  SELECT_GOAL
    1.11    (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.12 @@ -72,7 +72,7 @@
    1.13                              if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
    1.14  			    then ( 
    1.15                                      let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    1.16 -                                        val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
    1.17 +                                        val foo =   TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2")));
    1.18                                  
    1.19  			            in 
    1.20  
    1.21 @@ -109,7 +109,7 @@
    1.22                                               then     
    1.23                                                ( 
    1.24                                                   let 
    1.25 -                                               val outfile =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_transfer")));
    1.26 +                                               val outfile =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer")));
    1.27                                                 val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
    1.28                                                 val _ =  TextIO.closeOut outfile;
    1.29                                                 in
    1.30 @@ -129,8 +129,8 @@
    1.31  
    1.32  
    1.33  fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  (num_of_clauses:int )) = 
    1.34 -                                       let val spass_proof_file =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
    1.35 -                                            val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
    1.36 +                                       let val spass_proof_file =  TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "spass_proof")))
    1.37 +                                            val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
    1.38                                              val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm))
    1.39                                               
    1.40                                              val _ =  TextIO.closeOut outfile
    1.41 @@ -142,7 +142,7 @@
    1.42                                             in if ( thisLine = "SPASS beiseite: Proof found.\n" )
    1.43                                                then      
    1.44                                                (  
    1.45 -                                                 let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.46 +                                                 let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                                (*val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.47                                                       val _ = TextIO.output (outfile, (thisLine))
    1.48                                               
    1.49                                                       val _ =  TextIO.closeOut outfile
    1.50 @@ -154,7 +154,7 @@
    1.51                                                     then  
    1.52  
    1.53                                                   (
    1.54 -                                                      let    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.55 +                                                      let    val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof")));                                                                               (* val _ =  Posix.Process.sleep(Time.fromSeconds 3 );*)
    1.56                                                               val _ = TextIO.output (outfile, (thisLine))
    1.57                                               
    1.58                                                               val _ =  TextIO.closeOut outfile
    1.59 @@ -221,7 +221,7 @@
    1.60  fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
    1.61                            then
    1.62                                 let val thisLine = TextIO.inputLine instr 
    1.63 -                                   val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
    1.64 +                                   val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine")));                                                                     val _ = TextIO.output (outfile, (thisLine))
    1.65                                               
    1.66                                     val _ =  TextIO.closeOut outfile
    1.67  			       in 
    1.68 @@ -262,7 +262,7 @@
    1.69  						   let val reconstr = thisLine
    1.70                                                         val thmstring = TextIO.inputLine instr
    1.71                                                         val goalstring = TextIO.inputLine instr
    1.72 -						      val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_getSpass")));
    1.73 +						      val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getSpass")));
    1.74                                      		val _ = TextIO.output (outfile, (thisLine))
    1.75                                       			 val _ =  TextIO.closeOut outfile
    1.76                                                     in
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Sun Jun 05 11:31:21 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Sun Jun 05 11:31:22 2005 +0200
     2.3 @@ -1,7 +1,6 @@
     2.4 -
     2.5  (*  ID:         $Id$
     2.6 - Author:     Claire Quigley
     2.7 - Copyright   2004  University of Cambridge
     2.8 +    Author:     Claire Quigley
     2.9 +    Copyright   2004  University of Cambridge
    2.10  *)
    2.11  
    2.12  (******************)
    2.13 @@ -203,7 +202,7 @@
    2.14  fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    2.15      let val realnums = map subone step_nums	
    2.16  	val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    2.17 -	val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))     
    2.18 +	val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))     
    2.19  	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    2.20  	val _ = TextIO.closeOut(axnums)
    2.21      in
    2.22 @@ -245,7 +244,7 @@
    2.23  
    2.24   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    2.25       let 
    2.26 -	 (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    2.27 +	 (*val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    2.28  	 val _ = TextIO.output (outfile, thmstring)
    2.29  	 
    2.30  	 val _ =  TextIO.closeOut outfile*)
    2.31 @@ -262,7 +261,7 @@
    2.32         (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    2.33  	val clasimp_names = map #1 clasimp_names_cls
    2.34  	val clasimp_cls = map #2 clasimp_names_cls
    2.35 -	val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    2.36 +	val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    2.37  	 val _ = TextIO.output (outfile,clasimp_namestr)
    2.38  	 
    2.39  	 val _ =  TextIO.closeOut outfile
    2.40 @@ -287,11 +286,11 @@
    2.41  	val meta_strs = map ReconOrderClauses.get_meta_lits metas
    2.42         
    2.43  	val metas_and_strs = ListPair.zip (metas,meta_strs)
    2.44 -	 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    2.45 +	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    2.46  	 val _ = TextIO.output (outfile, onestr ax_strs)
    2.47  	 
    2.48  	 val _ =  TextIO.closeOut outfile
    2.49 -	 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    2.50 +	 val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    2.51  	 val _ = TextIO.output (outfile, onestr meta_strs)
    2.52  	 val _ =  TextIO.closeOut outfile
    2.53  
    2.54 @@ -311,14 +310,14 @@
    2.55  				     []
    2.56  
    2.57         (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    2.58 -       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
    2.59 +       val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
    2.60  
    2.61         val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
    2.62         val _ =  TextIO.closeOut outfile
    2.63 -      val foo_metas =  File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
    2.64 -      val foo_metas2 =   File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
    2.65 +      val foo_metas =  File.platform_path(File.tmp_path (Path.basic "foo_metas"))
    2.66 +      val foo_metas2 =   File.platform_path(File.tmp_path (Path.basic "foo_metas2"))
    2.67  	val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
    2.68 -     val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
    2.69 +     val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2")))
    2.70      val ax_metas_str = TextIO.inputLine (infile)
    2.71      val _ = TextIO.closeIn infile
    2.72         val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
    2.73 @@ -345,7 +344,7 @@
    2.74  
    2.75  
    2.76  fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    2.77 -           let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));     						  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
    2.78 +           let val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));     						  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
    2.79                                                    val _ =  TextIO.closeOut outfile
    2.80  
    2.81                                                (***********************************)
    2.82 @@ -355,10 +354,10 @@
    2.83                                                    val tokens = #1(lex proofstr)
    2.84                                                    val proof_steps1 = parse tokens
    2.85                                                    val proof_steps = just_change_space proof_steps1
    2.86 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    2.87 +                                                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
    2.88                                                    val _ =  TextIO.closeOut outfile
    2.89                                                  
    2.90 -                                                  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.91 +                                                  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
    2.92                                                    val _ =  TextIO.closeOut outfile
    2.93                                                (************************************)
    2.94                                                (* recreate original subgoal as thm *)
    2.95 @@ -372,7 +371,7 @@
    2.96  
    2.97                                                    val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
    2.98                                                    val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
    2.99 -                                                  val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   2.100 +                                                  val  outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   2.101                                                    val _ =  TextIO.closeOut outfile
   2.102                                                     
   2.103                                                in 
   2.104 @@ -387,7 +386,7 @@
   2.105                                           	  (* Attempt to prevent several signals from turning up simultaneously *)
   2.106                                           	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   2.107                                                end
   2.108 -                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   2.109 +                                              handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   2.110  
   2.111                                                    val _ = TextIO.output (outfile, ("In exception handler"));
   2.112                                                    val _ =  TextIO.closeOut outfile
   2.113 @@ -406,7 +405,7 @@
   2.114  
   2.115  
   2.116  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   2.117 -      let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   2.118 +      let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   2.119  	  (* val sign = sign_of_thm thm
   2.120  	 val prems = prems_of thm
   2.121  	 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
   2.122 @@ -426,10 +425,10 @@
   2.123  	  val proof_steps1 = parse tokens
   2.124  	  val proof_steps = just_change_space proof_steps1
   2.125  
   2.126 -	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   2.127 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   2.128  	  val _ =  TextIO.closeOut outfile
   2.129  	
   2.130 -	  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.131 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   2.132  	  val _ =  TextIO.closeOut outfile
   2.133        (************************************)
   2.134        (* recreate original subgoal as thm *)
   2.135 @@ -443,16 +442,16 @@
   2.136  	  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   2.137  	  
   2.138  	  (*val numcls_string = numclstr ( vars, numcls) ""*)
   2.139 -	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   2.140 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   2.141  	  val _ =  TextIO.closeOut outfile
   2.142  	    
   2.143        (************************************)
   2.144        (* translate proof                  *)
   2.145        (************************************)
   2.146 -	  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.147 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_steps")));                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   2.148  	  val _ =  TextIO.closeOut outfile
   2.149  	  val (newthm,proof) = translate_proof numcls  proof_steps vars
   2.150 -	  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.151 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_steps2")));                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   2.152  	  val _ =  TextIO.closeOut outfile
   2.153        (***************************************************)
   2.154        (* transfer necessary steps as strings to Isabelle *)
   2.155 @@ -469,7 +468,7 @@
   2.156  	  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   2.157  	  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   2.158  	  val frees_str = "["^(thmvars_to_string frees "")^"]"
   2.159 -	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
   2.160 +	  val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "reconstringfile")));
   2.161  
   2.162  	  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   2.163  	  val _ =  TextIO.closeOut outfile
   2.164 @@ -486,7 +485,7 @@
   2.165  	  (* Attempt to prevent several signals from turning up simultaneously *)
   2.166  	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   2.167        end
   2.168 -      handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   2.169 +      handle _ => (let val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
   2.170  
   2.171  	  val _ = TextIO.output (outfile, ("In exception handler"));
   2.172  	  val _ =  TextIO.closeOut outfile
   2.173 @@ -796,7 +795,7 @@
   2.174  		(isar_lines firststeps "")^
   2.175  		(last_isar_line laststep)^
   2.176  		("qed")
   2.177 -	val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
   2.178 +	val  outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "isar_proof_file")));
   2.179  	
   2.180  	val _ = TextIO.output (outfile, isar_proof)
   2.181  	val _ =  TextIO.closeOut outfile
   2.182 @@ -830,7 +829,7 @@
   2.183  
   2.184                                     val (frees,recon_steps) = parse_step tokens 
   2.185                                     val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   2.186 -                                   val foo =   TextIO.openOut (File.sysify_path(File.tmp_path (Path.basic "foobar")));
   2.187 +                                   val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
   2.188                                 in 
   2.189                                    TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
   2.190                                 end 
     3.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Sun Jun 05 11:31:21 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Sun Jun 05 11:31:22 2005 +0200
     3.3 @@ -418,7 +418,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(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
     3.8 +                               val outfile = TextIO.openOut(File.platform_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 --- a/src/HOL/Tools/res_atp.ML	Sun Jun 05 11:31:21 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Sun Jun 05 11:31:22 2005 +0200
     4.3 @@ -107,7 +107,7 @@
     4.4  	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
     4.5  	val tfree_lits = ResLib.flat_noDup tfree_litss
     4.6  	val tfree_clss = map ResClause.tfree_clause tfree_lits 
     4.7 -        val hypsfile = File.sysify_path hyps_file
     4.8 +        val hypsfile = File.platform_path hyps_file
     4.9  	val out = TextIO.openOut(hypsfile)
    4.10      in
    4.11  	((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 
    4.12 @@ -127,7 +127,7 @@
    4.13          val _ = (warning ("in tptp_inputs_tfrees 2"))
    4.14  	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    4.15           val _ = (warning ("in tptp_inputs_tfrees 3"))
    4.16 -        val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    4.17 +        val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    4.18  	val out = TextIO.openOut(probfile)
    4.19      in
    4.20  	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out;
    4.21 @@ -168,11 +168,11 @@
    4.22  	val no_returns =List.filter   not_newline ( thmproofstring)
    4.23  	val thmstr = implode no_returns
    4.24         
    4.25 -	val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    4.26 -	val axfile = (File.sysify_path axiom_file)
    4.27 -	val hypsfile = (File.sysify_path hyps_file)
    4.28 -	val clasimpfile = (File.sysify_path clasimp_file)
    4.29 -	val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
    4.30 +	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    4.31 +	val axfile = (File.platform_path axiom_file)
    4.32 +	val hypsfile = (File.platform_path hyps_file)
    4.33 +	val clasimpfile = (File.platform_path clasimp_file)
    4.34 +	val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "hellofile")))
    4.35  	val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
    4.36  	val _ = TextIO.flushOut outfile;
    4.37  	val _ =  TextIO.closeOut outfile
    4.38 @@ -298,9 +298,9 @@
    4.39          
    4.40  	(* set up variables for writing out the clasimps to a tptp file *)
    4.41  	val (clause_arr, num_of_clauses) =
    4.42 -	    ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
    4.43 +	    ResClasimp.write_out_clasimp (File.platform_path clasimp_file) 
    4.44  	                                 (ProofContext.theory_of ctxt)
    4.45 -        val _ = warning ("clasimp_file is " ^ File.sysify_path clasimp_file)
    4.46 +        val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file)
    4.47  
    4.48          (* cq: add write out clasimps to file *)
    4.49  
    4.50 @@ -375,7 +375,7 @@
    4.51  	val thms_ss = get_thms_ss delta_ss_thms
    4.52  	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
    4.53  	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
    4.54 -	val ax_file = File.sysify_path axiom_file
    4.55 +	val ax_file = File.platform_path axiom_file
    4.56  	val out = TextIO.openOut ax_file
    4.57      in
    4.58  	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
     5.1 --- a/src/Pure/proof_general.ML	Sun Jun 05 11:31:21 2005 +0200
     5.2 +++ b/src/Pure/proof_general.ML	Sun Jun 05 11:31:22 2005 +0200
     5.3 @@ -322,20 +322,20 @@
     5.4  fun tell_file_loaded path = 
     5.5      if pgip() then
     5.6  	issue_pgipe "informtheoryloaded"  (* FIXME: get thy name from info here? *)
     5.7 -		    [thyname_attr        (XML.text (File.sysify_path path)),
     5.8 -		     localfile_url_attr  (XML.text (File.sysify_path path))]
     5.9 +		    [thyname_attr        (XML.text (File.platform_path path)),
    5.10 +		     localfile_url_attr  (XML.text (File.platform_path path))]
    5.11      else 
    5.12  	emacs_notify ("Proof General, this file is loaded: " 
    5.13 -		      ^ quote (File.sysify_path path));
    5.14 +		      ^ quote (File.platform_path path));
    5.15  
    5.16  fun tell_file_retracted path = 
    5.17      if pgip() then
    5.18  	issue_pgipe "informtheoryretracted"  (* FIXME: get thy name from info here? *)
    5.19 -		    [thyname_attr        (XML.text (File.sysify_path path)),
    5.20 -		     localfile_url_attr  (XML.text (File.sysify_path path))]
    5.21 +		    [thyname_attr        (XML.text (File.platform_path path)),
    5.22 +		     localfile_url_attr  (XML.text (File.platform_path path))]
    5.23      else 
    5.24  	emacs_notify ("Proof General, you can unlock the file " 
    5.25 -		      ^ quote (File.sysify_path path));
    5.26 +		      ^ quote (File.platform_path path));
    5.27  
    5.28  
    5.29  (* theory / proof state output *)
    5.30 @@ -1158,7 +1158,7 @@
    5.31  
    5.32    fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
    5.33        case Url.unpack url of
    5.34 -	  (Url.File path) => File.sysify_path path
    5.35 +	  (Url.File path) => File.platform_path path
    5.36  	| _ => error ("Cannot access non-local URL " ^ url)
    5.37  
    5.38    val fileurl_of = localfile_of_url o (xmlattr "url")