Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
authorwenzelm
Sun Mar 13 16:01:00 2011 +0100 (2011-03-13 ago)
changeset 41944b97091ae583a
parent 41943 12f24ad566ea
child 41945 8e32c3992cb3
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
NEWS
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/sat_solver.ML
src/Pure/General/file.ML
src/Pure/General/path.ML
src/Pure/Isar/isar_syn.ML
src/Pure/System/isabelle_system.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_load.ML
src/Pure/pure_setup.ML
src/Tools/Code/code_runtime.ML
     1.1 --- a/NEWS	Sun Mar 13 15:16:37 2011 +0100
     1.2 +++ b/NEWS	Sun Mar 13 16:01:00 2011 +0100
     1.3 @@ -43,6 +43,12 @@
     1.4  subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
     1.5  
     1.6  
     1.7 +*** ML ***
     1.8 +
     1.9 +* Path.print is the official way to show file-system paths to users
    1.10 +(including quotes etc.).
    1.11 +
    1.12 +
    1.13  
    1.14  New in Isabelle2011 (January 2011)
    1.15  ----------------------------------
     2.1 --- a/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Mar 13 15:16:37 2011 +0100
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Mar 13 16:01:00 2011 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4    let
     2.5      val ext = "b2i"
     2.6      fun check_ext path = snd (Path.split_ext path) = ext orelse
     2.7 -      error ("Bad file ending of file " ^ quote (Path.implode path) ^ ", " ^
     2.8 +      error ("Bad file ending of file " ^ Path.print path ^ ", " ^
     2.9          "expected file ending " ^ quote ext)
    2.10  
    2.11      val base_path = Path.explode base_name |> tap check_ext
     3.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Mar 13 15:16:37 2011 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Mar 13 16:01:00 2011 +0100
     3.3 @@ -100,9 +100,9 @@
     3.4      \TPTP syntax. To install it, download and extract the package \
     3.5      \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
     3.6      \\"spass-3.7\" directory's absolute path to " ^
     3.7 -    quote (Path.implode (Path.expand (Path.appends
     3.8 +    Path.print (Path.expand (Path.appends
     3.9                 (Path.variable "ISABELLE_HOME_USER" ::
    3.10 -                map Path.basic ["etc", "components"])))) ^
    3.11 +                map Path.basic ["etc", "components"]))) ^
    3.12      " on a line of its own."
    3.13    | string_for_failure VampireTooOld =
    3.14      "Isabelle requires a more recent version of Vampire. To install it, follow \
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Mar 13 15:16:37 2011 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Mar 13 16:01:00 2011 +0100
     4.3 @@ -164,10 +164,10 @@
     4.4  fun install_kodkodi_message () =
     4.5    "Nitpick requires the external Java program Kodkodi. To install it, download \
     4.6    \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
     4.7 -  \directory's full path to \"" ^
     4.8 -  Path.implode (Path.expand (Path.appends
     4.9 +  \directory's full path to " ^
    4.10 +  Path.print (Path.expand (Path.appends
    4.11        (Path.variable "ISABELLE_HOME_USER" ::
    4.12 -       map Path.basic ["etc", "components"]))) ^ "\" on a line of its own."
    4.13 +       map Path.basic ["etc", "components"]))) ^ " on a line of its own."
    4.14  
    4.15  val max_unsound_delay_ms = 200
    4.16  val max_unsound_delay_percent = 2
     5.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Sun Mar 13 15:16:37 2011 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Sun Mar 13 16:01:00 2011 +0100
     5.3 @@ -279,7 +279,7 @@
     5.4  
     5.5      val certs_filename =
     5.6        (case get_certificates_path ctxt of
     5.7 -        SOME path => Path.implode path
     5.8 +        SOME path => Path.print path
     5.9        | NONE => "(disabled)")
    5.10    in
    5.11      Pretty.writeln (Pretty.big_list "SMT setup:" [
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Mar 13 15:16:37 2011 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Mar 13 16:01:00 2011 +0100
     6.3 @@ -426,7 +426,7 @@
     6.4                       | result => result)
     6.5            in ((pool, conjecture_shape, fact_names), result) end
     6.6          else
     6.7 -          error ("Bad executable: " ^ Path.implode command ^ ".")
     6.8 +          error ("Bad executable: " ^ Path.print command ^ ".")
     6.9  
    6.10      (* If the problem file has not been exported, remove it; otherwise, export
    6.11         the proof file too. *)
     7.1 --- a/src/HOL/Tools/sat_solver.ML	Sun Mar 13 15:16:37 2011 +0100
     7.2 +++ b/src/HOL/Tools/sat_solver.ML	Sun Mar 13 16:01:00 2011 +0100
     7.3 @@ -578,8 +578,8 @@
     7.4      val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " -t " ^ File.shell_path proofpath ^ "> /dev/null"
     7.5      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
     7.6      fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
     7.7 -    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
     7.8 -    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
     7.9 +    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
    7.10 +    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
    7.11      val cnf        = Prop_Logic.defcnf fm
    7.12      val result     = SatSolver.make_external_solver cmd writefn readfn cnf
    7.13      val _          = try File.rm inpath
    7.14 @@ -763,8 +763,8 @@
    7.15      val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null"
    7.16      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
    7.17      fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
    7.18 -    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
    7.19 -    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
    7.20 +    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
    7.21 +    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
    7.22      val result     = SatSolver.make_external_solver cmd writefn readfn fm
    7.23      val _          = try File.rm inpath
    7.24      val _          = try File.rm outpath
    7.25 @@ -922,8 +922,8 @@
    7.26      val cmd        = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
    7.27      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
    7.28      fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
    7.29 -    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
    7.30 -    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
    7.31 +    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
    7.32 +    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
    7.33      val result     = SatSolver.make_external_solver cmd writefn readfn fm
    7.34      val _          = try File.rm inpath
    7.35      val _          = try File.rm outpath
    7.36 @@ -949,8 +949,8 @@
    7.37      val cmd        = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
    7.38      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
    7.39      fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
    7.40 -    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
    7.41 -    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
    7.42 +    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
    7.43 +    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
    7.44      val result     = SatSolver.make_external_solver cmd writefn readfn fm
    7.45      val _          = try File.rm inpath
    7.46      val _          = try File.rm outpath
    7.47 @@ -975,8 +975,8 @@
    7.48      val cmd        = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
    7.49      fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
    7.50      fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
    7.51 -    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
    7.52 -    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
    7.53 +    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
    7.54 +    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
    7.55      val result     = SatSolver.make_external_solver cmd writefn readfn fm
    7.56      val _          = try File.rm inpath
    7.57      val _          = try File.rm outpath
     8.1 --- a/src/Pure/General/file.ML	Sun Mar 13 15:16:37 2011 +0100
     8.2 +++ b/src/Pure/General/file.ML	Sun Mar 13 16:01:00 2011 +0100
     8.3 @@ -68,7 +68,7 @@
     8.4  
     8.5  fun check path =
     8.6    if exists path then ()
     8.7 -  else error ("No such file or directory: " ^ quote (Path.implode path));
     8.8 +  else error ("No such file or directory: " ^ Path.print path);
     8.9  
    8.10  val rm = OS.FileSys.remove o platform_path;
    8.11  
     9.1 --- a/src/Pure/General/path.ML	Sun Mar 13 15:16:37 2011 +0100
     9.2 +++ b/src/Pure/General/path.ML	Sun Mar 13 16:01:00 2011 +0100
     9.3 @@ -20,6 +20,7 @@
     9.4    val append: T -> T -> T
     9.5    val appends: T list -> T
     9.6    val make: string list -> T
     9.7 +  val print: T -> string
     9.8    val implode: T -> string
     9.9    val explode: string -> T
    9.10    val dir: T -> T
    9.11 @@ -119,6 +120,8 @@
    9.12  
    9.13  end;
    9.14  
    9.15 +val print = quote o implode_path;
    9.16 +
    9.17  
    9.18  (* explode *)
    9.19  
    10.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 13 15:16:37 2011 +0100
    10.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 13 16:01:00 2011 +0100
    10.3 @@ -946,7 +946,7 @@
    10.4  val _ =
    10.5    Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
    10.6      (Scan.succeed (Toplevel.no_timing o
    10.7 -      Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())))));
    10.8 +      Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
    10.9  
   10.10  val _ =
   10.11    Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
    11.1 --- a/src/Pure/System/isabelle_system.ML	Sun Mar 13 15:16:37 2011 +0100
    11.2 +++ b/src/Pure/System/isabelle_system.ML	Sun Mar 13 16:01:00 2011 +0100
    11.3 @@ -56,7 +56,7 @@
    11.4    let
    11.5      val path = File.tmp_path (Path.basic (name ^ serial_string ()));
    11.6      val _ = File.exists path andalso
    11.7 -      raise Fail ("Temporary file already exists: " ^ quote (Path.implode path));
    11.8 +      raise Fail ("Temporary file already exists: " ^ Path.print path);
    11.9    in path end;
   11.10  
   11.11  fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
    12.1 --- a/src/Pure/Thy/present.ML	Sun Mar 13 15:16:37 2011 +0100
    12.2 +++ b/src/Pure/Thy/present.ML	Sun Mar 13 16:01:00 2011 +0100
    12.3 @@ -258,7 +258,7 @@
    12.4  
    12.5  fun update_index dir name = CRITICAL (fn () =>
    12.6    (case try get_entries dir of
    12.7 -    NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
    12.8 +    NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir)
    12.9    | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
   12.10  
   12.11  
   12.12 @@ -503,7 +503,7 @@
   12.13        in
   12.14          if File.exists path then
   12.15            (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
   12.16 -        else error ("Bad file: " ^ quote (Path.implode path))
   12.17 +        else error ("Bad file: " ^ Path.print path)
   12.18        end;
   12.19      val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
   12.20  
    13.1 --- a/src/Pure/Thy/thy_header.ML	Sun Mar 13 15:16:37 2011 +0100
    13.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Mar 13 16:01:00 2011 +0100
    13.3 @@ -75,11 +75,10 @@
    13.4  fun split_thy_path path =
    13.5    (case Path.split_ext path of
    13.6      (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
    13.7 -  | _ => error ("Bad theory file specification: " ^ Path.implode path));
    13.8 +  | _ => error ("Bad theory file specification: " ^ Path.print path));
    13.9  
   13.10  fun consistent_name name name' =
   13.11    if name = name' then ()
   13.12 -  else error ("Bad file name " ^ quote (Path.implode (thy_path name)) ^
   13.13 -    " for theory " ^ quote name');
   13.14 +  else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
   13.15  
   13.16  end;
    14.1 --- a/src/Pure/Thy/thy_load.ML	Sun Mar 13 15:16:37 2011 +0100
    14.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Mar 13 16:01:00 2011 +0100
    14.3 @@ -70,7 +70,7 @@
    14.4                        ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path);
    14.5                  in
    14.6                    if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
    14.7 -                  else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
    14.8 +                  else error ("Failed to identify file " ^ Path.print path ^ " by " ^ cmd)
    14.9                  end))))
   14.10    end;
   14.11  
   14.12 @@ -107,13 +107,13 @@
   14.13  fun require src_path =
   14.14    map_files (fn (master_dir, imports, required, provided) =>
   14.15      if member (op =) required src_path then
   14.16 -      error ("Duplicate source file dependency: " ^ Path.implode src_path)
   14.17 +      error ("Duplicate source file dependency: " ^ Path.print src_path)
   14.18      else (master_dir, imports, src_path :: required, provided));
   14.19  
   14.20  fun provide (src_path, path_id) =
   14.21    map_files (fn (master_dir, imports, required, provided) =>
   14.22      if AList.defined (op =) provided src_path then
   14.23 -      error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
   14.24 +      error ("Duplicate resolution of source file dependency: " ^ Path.print src_path)
   14.25      else (master_dir, imports, required, (src_path, path_id) :: provided));
   14.26  
   14.27  
   14.28 @@ -145,8 +145,7 @@
   14.29  fun check_file dir file =
   14.30    (case get_file dir file of
   14.31      SOME path_id => path_id
   14.32 -  | NONE => error ("Could not find file " ^ quote (Path.implode file) ^
   14.33 -      "\nin " ^ quote (Path.implode dir)));
   14.34 +  | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir));
   14.35  
   14.36  fun check_thy dir name =
   14.37    check_file dir (Thy_Header.thy_path name);
   14.38 @@ -176,11 +175,11 @@
   14.39      val _ =
   14.40        (case subtract (op =) provided_paths required of
   14.41          [] => NONE
   14.42 -      | bad => error ("Pending source file dependencies: " ^ commas (map Path.implode (rev bad))));
   14.43 +      | bad => error ("Pending source file dependencies: " ^ commas (map Path.print (rev bad))));
   14.44      val _ =
   14.45        (case subtract (op =) required provided_paths of
   14.46          [] => NONE
   14.47 -      | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.implode (rev bad))));
   14.48 +      | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.print (rev bad))));
   14.49    in () end;
   14.50  
   14.51  fun all_current thy =
    15.1 --- a/src/Pure/pure_setup.ML	Sun Mar 13 15:16:37 2011 +0100
    15.2 +++ b/src/Pure/pure_setup.ML	Sun Mar 13 16:01:00 2011 +0100
    15.3 @@ -31,7 +31,7 @@
    15.4  toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
    15.5  toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    15.6  toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
    15.7 -toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
    15.8 +toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
    15.9  toplevel_pp ["Thy_Load", "file_ident"] "Thy_Load.pretty_file_ident";
   15.10  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
   15.11  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
    16.1 --- a/src/Tools/Code/code_runtime.ML	Sun Mar 13 15:16:37 2011 +0100
    16.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Mar 13 16:01:00 2011 +0100
    16.3 @@ -436,7 +436,7 @@
    16.4      val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;
    16.5      val _ = if null superfluous then ()
    16.6        else error ("Value binding(s) " ^ commas_quote superfluous
    16.7 -        ^ " found in external file " ^ quote (Path.implode filepath)
    16.8 +        ^ " found in external file " ^ Path.print filepath
    16.9          ^ " not present among the given contants binding(s).");
   16.10      val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names;
   16.11      val thy'' = fold add_definiendum these_definienda thy';