# HG changeset patch # User wenzelm # Date 1300028460 -3600 # Node ID b97091ae583ab810af14f013b8e2f75ea7a4aa49 # Parent 12f24ad566ea20e2c1ffee67049f31c9d8d08205 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype; diff -r 12f24ad566ea -r b97091ae583a NEWS --- a/NEWS Sun Mar 13 15:16:37 2011 +0100 +++ b/NEWS Sun Mar 13 16:01:00 2011 +0100 @@ -43,6 +43,12 @@ subscripted form x\<^isub>1, y\<^isub>2\<^isub>3. +*** ML *** + +* Path.print is the official way to show file-system paths to users +(including quotes etc.). + + New in Isabelle2011 (January 2011) ---------------------------------- diff -r 12f24ad566ea -r b97091ae583a src/HOL/Boogie/Tools/boogie_commands.ML --- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sun Mar 13 16:01:00 2011 +0100 @@ -18,7 +18,7 @@ let val ext = "b2i" fun check_ext path = snd (Path.split_ext path) = ext orelse - error ("Bad file ending of file " ^ quote (Path.implode path) ^ ", " ^ + error ("Bad file ending of file " ^ Path.print path ^ ", " ^ "expected file ending " ^ quote ext) val base_path = Path.explode base_name |> tap check_ext diff -r 12f24ad566ea -r b97091ae583a src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Sun Mar 13 16:01:00 2011 +0100 @@ -100,9 +100,9 @@ \TPTP syntax. To install it, download and extract the package \ \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \ \\"spass-3.7\" directory's absolute path to " ^ - quote (Path.implode (Path.expand (Path.appends + Path.print (Path.expand (Path.appends (Path.variable "ISABELLE_HOME_USER" :: - map Path.basic ["etc", "components"])))) ^ + map Path.basic ["etc", "components"]))) ^ " on a line of its own." | string_for_failure VampireTooOld = "Isabelle requires a more recent version of Vampire. To install it, follow \ diff -r 12f24ad566ea -r b97091ae583a src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Mar 13 16:01:00 2011 +0100 @@ -164,10 +164,10 @@ fun install_kodkodi_message () = "Nitpick requires the external Java program Kodkodi. To install it, download \ \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \ - \directory's full path to \"" ^ - Path.implode (Path.expand (Path.appends + \directory's full path to " ^ + Path.print (Path.expand (Path.appends (Path.variable "ISABELLE_HOME_USER" :: - map Path.basic ["etc", "components"]))) ^ "\" on a line of its own." + map Path.basic ["etc", "components"]))) ^ " on a line of its own." val max_unsound_delay_ms = 200 val max_unsound_delay_percent = 2 diff -r 12f24ad566ea -r b97091ae583a src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/HOL/Tools/SMT/smt_config.ML Sun Mar 13 16:01:00 2011 +0100 @@ -279,7 +279,7 @@ val certs_filename = (case get_certificates_path ctxt of - SOME path => Path.implode path + SOME path => Path.print path | NONE => "(disabled)") in Pretty.writeln (Pretty.big_list "SMT setup:" [ diff -r 12f24ad566ea -r b97091ae583a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun Mar 13 16:01:00 2011 +0100 @@ -426,7 +426,7 @@ | result => result) in ((pool, conjecture_shape, fact_names), result) end else - error ("Bad executable: " ^ Path.implode command ^ ".") + error ("Bad executable: " ^ Path.print command ^ ".") (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) diff -r 12f24ad566ea -r b97091ae583a src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/HOL/Tools/sat_solver.ML Sun Mar 13 16:01:00 2011 +0100 @@ -578,8 +578,8 @@ val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " -t " ^ File.shell_path proofpath ^ "> /dev/null" fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val cnf = Prop_Logic.defcnf fm val result = SatSolver.make_external_solver cmd writefn readfn cnf val _ = try File.rm inpath @@ -763,8 +763,8 @@ val cmd = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null" fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val result = SatSolver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath @@ -922,8 +922,8 @@ val cmd = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val result = SatSolver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath @@ -949,8 +949,8 @@ val cmd = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val result = SatSolver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath @@ -975,8 +975,8 @@ val cmd = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () + val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else () val result = SatSolver.make_external_solver cmd writefn readfn fm val _ = try File.rm inpath val _ = try File.rm outpath diff -r 12f24ad566ea -r b97091ae583a src/Pure/General/file.ML --- a/src/Pure/General/file.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/General/file.ML Sun Mar 13 16:01:00 2011 +0100 @@ -68,7 +68,7 @@ fun check path = if exists path then () - else error ("No such file or directory: " ^ quote (Path.implode path)); + else error ("No such file or directory: " ^ Path.print path); val rm = OS.FileSys.remove o platform_path; diff -r 12f24ad566ea -r b97091ae583a src/Pure/General/path.ML --- a/src/Pure/General/path.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/General/path.ML Sun Mar 13 16:01:00 2011 +0100 @@ -20,6 +20,7 @@ val append: T -> T -> T val appends: T list -> T val make: string list -> T + val print: T -> string val implode: T -> string val explode: string -> T val dir: T -> T @@ -119,6 +120,8 @@ end; +val print = quote o implode_path; + (* explode *) diff -r 12f24ad566ea -r b97091ae583a src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sun Mar 13 16:01:00 2011 +0100 @@ -946,7 +946,7 @@ val _ = Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag (Scan.succeed (Toplevel.no_timing o - Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ()))))); + Toplevel.imperative (fn () => writeln (Path.print (File.pwd ()))))); val _ = Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control diff -r 12f24ad566ea -r b97091ae583a src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/System/isabelle_system.ML Sun Mar 13 16:01:00 2011 +0100 @@ -56,7 +56,7 @@ let val path = File.tmp_path (Path.basic (name ^ serial_string ())); val _ = File.exists path andalso - raise Fail ("Temporary file already exists: " ^ quote (Path.implode path)); + raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path); diff -r 12f24ad566ea -r b97091ae583a src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/Thy/present.ML Sun Mar 13 16:01:00 2011 +0100 @@ -258,7 +258,7 @@ fun update_index dir name = CRITICAL (fn () => (case try get_entries dir of - NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir)) + NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir) | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir))); @@ -503,7 +503,7 @@ in if File.exists path then (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1) - else error ("Bad file: " ^ quote (Path.implode path)) + else error ("Bad file: " ^ Path.print path) end; val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0)); diff -r 12f24ad566ea -r b97091ae583a src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/Thy/thy_header.ML Sun Mar 13 16:01:00 2011 +0100 @@ -75,11 +75,10 @@ fun split_thy_path path = (case Path.split_ext path of (path', "thy") => (Path.dir path', Path.implode (Path.base path')) - | _ => error ("Bad theory file specification: " ^ Path.implode path)); + | _ => error ("Bad theory file specification: " ^ Path.print path)); fun consistent_name name name' = if name = name' then () - else error ("Bad file name " ^ quote (Path.implode (thy_path name)) ^ - " for theory " ^ quote name'); + else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name'); end; diff -r 12f24ad566ea -r b97091ae583a src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/Thy/thy_load.ML Sun Mar 13 16:01:00 2011 +0100 @@ -70,7 +70,7 @@ ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path); in if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id) - else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd) + else error ("Failed to identify file " ^ Path.print path ^ " by " ^ cmd) end)))) end; @@ -107,13 +107,13 @@ fun require src_path = map_files (fn (master_dir, imports, required, provided) => if member (op =) required src_path then - error ("Duplicate source file dependency: " ^ Path.implode src_path) + error ("Duplicate source file dependency: " ^ Path.print src_path) else (master_dir, imports, src_path :: required, provided)); fun provide (src_path, path_id) = map_files (fn (master_dir, imports, required, provided) => if AList.defined (op =) provided src_path then - error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path) + error ("Duplicate resolution of source file dependency: " ^ Path.print src_path) else (master_dir, imports, required, (src_path, path_id) :: provided)); @@ -145,8 +145,7 @@ fun check_file dir file = (case get_file dir file of SOME path_id => path_id - | NONE => error ("Could not find file " ^ quote (Path.implode file) ^ - "\nin " ^ quote (Path.implode dir))); + | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir)); fun check_thy dir name = check_file dir (Thy_Header.thy_path name); @@ -176,11 +175,11 @@ val _ = (case subtract (op =) provided_paths required of [] => NONE - | bad => error ("Pending source file dependencies: " ^ commas (map Path.implode (rev bad)))); + | bad => error ("Pending source file dependencies: " ^ commas (map Path.print (rev bad)))); val _ = (case subtract (op =) required provided_paths of [] => NONE - | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.implode (rev bad)))); + | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.print (rev bad)))); in () end; fun all_current thy = diff -r 12f24ad566ea -r b97091ae583a src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/pure_setup.ML Sun Mar 13 16:01:00 2011 +0100 @@ -31,7 +31,7 @@ toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; -toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; +toplevel_pp ["Path", "T"] "Pretty.str o Path.print"; toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident"; toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"\")"; toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; diff -r 12f24ad566ea -r b97091ae583a src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Tools/Code/code_runtime.ML Sun Mar 13 16:01:00 2011 +0100 @@ -436,7 +436,7 @@ val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names; val _ = if null superfluous then () else error ("Value binding(s) " ^ commas_quote superfluous - ^ " found in external file " ^ quote (Path.implode filepath) + ^ " found in external file " ^ Path.print filepath ^ " not present among the given contants binding(s)."); val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names; val thy'' = fold add_definiendum these_definienda thy';