# HG changeset patch # User wenzelm # Date 1117963882 -7200 # Node ID aed1a8ae4b239ee6376ab27a26e57553cefc1fd2 # Parent f3d913abf7e5ceb8499179c7e3b18d282b61e496 File.platform_path; diff -r f3d913abf7e5 -r aed1a8ae4b23 src/HOL/Tools/ATP/SpassCommunication.ML --- 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 diff -r f3d913abf7e5 -r aed1a8ae4b23 src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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 diff -r f3d913abf7e5 -r aed1a8ae4b23 src/HOL/Tools/ATP/recon_translate_proof.ML --- 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 diff -r f3d913abf7e5 -r aed1a8ae4b23 src/HOL/Tools/res_atp.ML --- 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) diff -r f3d913abf7e5 -r aed1a8ae4b23 src/Pure/proof_general.ML --- 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")