Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;

--- 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)
 ----------------------------------

--- 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

--- 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 \

--- 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

--- 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:" [

--- 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. *)

--- 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

--- 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;
 

--- 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 *)
 

--- 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

--- 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);

--- 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));
 

--- 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;

--- 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 =

--- 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 \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";

--- 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';