--- a/src/HOL/Tools/ATP/SpassCommunication.ML Sun Jun 05 11:31:21 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Sun Jun 05 11:31:22 2005 +0200
@@ -52,7 +52,7 @@
fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr (num_of_clauses:int ) =
- let val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar3")));
+ let val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar3")));
in
SELECT_GOAL
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
@@ -72,7 +72,7 @@
if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
then (
let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
- val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
+ val foo = TextIO.openOut( File.platform_path(File.tmp_path (Path.basic"foobar2")));
in
@@ -109,7 +109,7 @@
then
(
let
- val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_transfer")));
+ val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_transfer")));
val _= TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
val _ = TextIO.closeOut outfile;
in
@@ -129,8 +129,8 @@
fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr, (num_of_clauses:int )) =
- let val spass_proof_file = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));
+ let val spass_proof_file = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "spass_proof")))
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_checkspass")));
val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm))
val _ = TextIO.closeOut outfile
@@ -142,7 +142,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 _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (*val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -154,7 +154,7 @@
then
(
- let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
+ let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*)
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
@@ -221,7 +221,7 @@
fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
then
let val thisLine = TextIO.inputLine instr
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine))
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thisLine"))); val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
in
@@ -262,7 +262,7 @@
let val reconstr = thisLine
val thmstring = TextIO.inputLine instr
val goalstring = TextIO.inputLine instr
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_getSpass")));
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_getSpass")));
val _ = TextIO.output (outfile, (thisLine))
val _ = TextIO.closeOut outfile
in
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Sun Jun 05 11:31:21 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Sun Jun 05 11:31:22 2005 +0200
@@ -1,7 +1,6 @@
-
(* ID: $Id$
- Author: Claire Quigley
- Copyright 2004 University of Cambridge
+ Author: Claire Quigley
+ Copyright 2004 University of Cambridge
*)
(******************)
@@ -203,7 +202,7 @@
fun get_clasimp_cls clause_arr clasimp_num step_nums =
let val realnums = map subone step_nums
val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
- val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))
+ val axnums = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "axnums")))
val _ = TextIO.output(axnums,(numstr clasimp_nums))
val _ = TextIO.closeOut(axnums)
in
@@ -245,7 +244,7 @@
fun get_axioms_used proof_steps thms clause_arr num_of_clauses =
let
- (*val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
+ (*val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
val _ = TextIO.output (outfile, thmstring)
val _ = TextIO.closeOut outfile*)
@@ -262,7 +261,7 @@
(* val clasimp_names_cls = get_clasimp_cls clause_arr num_of_clauses step_nums
val clasimp_names = map #1 clasimp_names_cls
val clasimp_cls = map #2 clasimp_names_cls
- val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names
+ val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names
val _ = TextIO.output (outfile,clasimp_namestr)
val _ = TextIO.closeOut outfile
@@ -287,11 +286,11 @@
val meta_strs = map ReconOrderClauses.get_meta_lits metas
val metas_and_strs = ListPair.zip (metas,meta_strs)
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_clauses")));
val _ = TextIO.output (outfile, onestr ax_strs)
val _ = TextIO.closeOut outfile
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metastrs")));
val _ = TextIO.output (outfile, onestr meta_strs)
val _ = TextIO.closeOut outfile
@@ -311,14 +310,14 @@
[]
(* val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_metas")))
val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
val _ = TextIO.closeOut outfile
- val foo_metas = File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
- val foo_metas2 = File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
+ val foo_metas = File.platform_path(File.tmp_path (Path.basic "foo_metas"))
+ val foo_metas2 = File.platform_path(File.tmp_path (Path.basic "foo_metas2"))
val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", " <", foo_metas, " >", foo_metas2])
- val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
+ val infile = TextIO.openIn(File.platform_path(File.tmp_path (Path.basic "foo_metas2")))
val ax_metas_str = TextIO.inputLine (infile)
val _ = TextIO.closeIn infile
val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
@@ -345,7 +344,7 @@
fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses =
- 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)))
+ 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)))
val _ = TextIO.closeOut outfile
(***********************************)
@@ -355,10 +354,10 @@
val tokens = #1(lex proofstr)
val proof_steps1 = parse tokens
val proof_steps = just_change_space proof_steps1
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
val _ = TextIO.closeOut outfile
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
val _ = TextIO.closeOut outfile
(************************************)
(* recreate original subgoal as thm *)
@@ -372,7 +371,7 @@
val (axiom_names) = get_axiom_names proof_steps thms clause_arr num_of_clauses
val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
- val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile"))); val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^" "^goalstring))
+ val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "reconstrfile"))); val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^" "^goalstring))
val _ = TextIO.closeOut outfile
in
@@ -387,7 +386,7 @@
(* Attempt to prevent several signals from turning up simultaneously *)
Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
end
- handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
+ handle _ => (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
val _ = TextIO.output (outfile, ("In exception handler"));
val _ = TextIO.closeOut outfile
@@ -406,7 +405,7 @@
fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses =
- let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));
+ let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thmstringfile")));
(* val sign = sign_of_thm thm
val prems = prems_of thm
val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
@@ -426,10 +425,10 @@
val proof_steps1 = parse tokens
val proof_steps = just_change_space proof_steps1
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_parse"))); val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
val _ = TextIO.closeOut outfile
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_thmstring_at_parse"))); val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
val _ = TextIO.closeOut outfile
(************************************)
(* recreate original subgoal as thm *)
@@ -443,16 +442,16 @@
val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr num_of_clauses
(*val numcls_string = numclstr ( vars, numcls) ""*)
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms")
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_axiom"))); val _ = TextIO.output (outfile,"got axioms")
val _ = TextIO.closeOut outfile
(************************************)
(* translate proof *)
(************************************)
- 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 "")))
+ 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 "")))
val _ = TextIO.closeOut outfile
val (newthm,proof) = translate_proof numcls proof_steps vars
- 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 "")))
+ 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 "")))
val _ = TextIO.closeOut outfile
(***************************************************)
(* transfer necessary steps as strings to Isabelle *)
@@ -469,7 +468,7 @@
val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
val frees_str = "["^(thmvars_to_string frees "")^"]"
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "reconstringfile")));
val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
val _ = TextIO.closeOut outfile
@@ -486,7 +485,7 @@
(* Attempt to prevent several signals from turning up simultaneously *)
Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
end
- handle _ => (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
+ handle _ => (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_handler")));
val _ = TextIO.output (outfile, ("In exception handler"));
val _ = TextIO.closeOut outfile
@@ -796,7 +795,7 @@
(isar_lines firststeps "")^
(last_isar_line laststep)^
("qed")
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "isar_proof_file")));
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "isar_proof_file")));
val _ = TextIO.output (outfile, isar_proof)
val _ = TextIO.closeOut outfile
@@ -830,7 +829,7 @@
val (frees,recon_steps) = parse_step tokens
val isar_str = to_isar_proof (frees, recon_steps, goalstring)
- val foo = TextIO.openOut (File.sysify_path(File.tmp_path (Path.basic "foobar")));
+ val foo = TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
in
TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str isar_str); ()
end
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Sun Jun 05 11:31:21 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Sun Jun 05 11:31:22 2005 +0200
@@ -418,7 +418,7 @@
val thmproofstring = proofstring ( thmstring)
val no_returns =List.filter not_newline ( thmproofstring)
val thmstr = implode no_returns
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thml_file")))
val _ = TextIO.output(outfile, "thmstr is "^thmstr)
val _ = TextIO.flushOut outfile;
val _ = TextIO.closeOut outfile
--- a/src/HOL/Tools/res_atp.ML Sun Jun 05 11:31:21 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Sun Jun 05 11:31:22 2005 +0200
@@ -107,7 +107,7 @@
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
val tfree_lits = ResLib.flat_noDup tfree_litss
val tfree_clss = map ResClause.tfree_clause tfree_lits
- val hypsfile = File.sysify_path hyps_file
+ val hypsfile = File.platform_path hyps_file
val out = TextIO.openOut(hypsfile)
in
((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits)
@@ -127,7 +127,7 @@
val _ = (warning ("in tptp_inputs_tfrees 2"))
val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
val _ = (warning ("in tptp_inputs_tfrees 3"))
- val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
+ val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
val out = TextIO.openOut(probfile)
in
(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out;
@@ -168,11 +168,11 @@
val no_returns =List.filter not_newline ( thmproofstring)
val thmstr = implode no_returns
- val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
- val axfile = (File.sysify_path axiom_file)
- val hypsfile = (File.sysify_path hyps_file)
- val clasimpfile = (File.sysify_path clasimp_file)
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile")))
+ val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
+ val axfile = (File.platform_path axiom_file)
+ val hypsfile = (File.platform_path hyps_file)
+ val clasimpfile = (File.platform_path clasimp_file)
+ val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "hellofile")))
val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
val _ = TextIO.flushOut outfile;
val _ = TextIO.closeOut outfile
@@ -298,9 +298,9 @@
(* set up variables for writing out the clasimps to a tptp file *)
val (clause_arr, num_of_clauses) =
- ResClasimp.write_out_clasimp (File.sysify_path clasimp_file)
+ ResClasimp.write_out_clasimp (File.platform_path clasimp_file)
(ProofContext.theory_of ctxt)
- val _ = warning ("clasimp_file is " ^ File.sysify_path clasimp_file)
+ val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file)
(* cq: add write out clasimps to file *)
@@ -375,7 +375,7 @@
val thms_ss = get_thms_ss delta_ss_thms
val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
- val ax_file = File.sysify_path axiom_file
+ val ax_file = File.platform_path axiom_file
val out = TextIO.openOut ax_file
in
(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
--- a/src/Pure/proof_general.ML Sun Jun 05 11:31:21 2005 +0200
+++ b/src/Pure/proof_general.ML Sun Jun 05 11:31:22 2005 +0200
@@ -322,20 +322,20 @@
fun tell_file_loaded path =
if pgip() then
issue_pgipe "informtheoryloaded" (* FIXME: get thy name from info here? *)
- [thyname_attr (XML.text (File.sysify_path path)),
- localfile_url_attr (XML.text (File.sysify_path path))]
+ [thyname_attr (XML.text (File.platform_path path)),
+ localfile_url_attr (XML.text (File.platform_path path))]
else
emacs_notify ("Proof General, this file is loaded: "
- ^ quote (File.sysify_path path));
+ ^ quote (File.platform_path path));
fun tell_file_retracted path =
if pgip() then
issue_pgipe "informtheoryretracted" (* FIXME: get thy name from info here? *)
- [thyname_attr (XML.text (File.sysify_path path)),
- localfile_url_attr (XML.text (File.sysify_path path))]
+ [thyname_attr (XML.text (File.platform_path path)),
+ localfile_url_attr (XML.text (File.platform_path path))]
else
emacs_notify ("Proof General, you can unlock the file "
- ^ quote (File.sysify_path path));
+ ^ quote (File.platform_path path));
(* theory / proof state output *)
@@ -1158,7 +1158,7 @@
fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
case Url.unpack url of
- (Url.File path) => File.sysify_path path
+ (Url.File path) => File.platform_path path
| _ => error ("Cannot access non-local URL " ^ url)
val fileurl_of = localfile_of_url o (xmlattr "url")