standardized use of Path operations;
authorwenzelm
Thu Jun 30 13:21:41 2011 +0200 (2011-06-30 ago)
changeset 436028c89a1fb30f2
parent 43601 fd650d659275
child 43603 8f777c2e4638
standardized use of Path operations;
src/HOL/Matrix/Compute_Oracle/am_ghc.ML
src/HOL/Matrix/Cplex_tools.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/ex/atp_export.ML
src/Tools/WWW_Find/unicode_symbols.ML
     1.1 --- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Thu Jun 30 11:15:36 2011 +0200
     1.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Thu Jun 30 13:21:41 2011 +0200
     1.3 @@ -210,7 +210,7 @@
     1.4          string_of_int (Time.toMicroseconds (Time.now ())) ^ string_of_int c
     1.5      end
     1.6  
     1.7 -fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
     1.8 +fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
     1.9  fun wrap s = "\""^s^"\""
    1.10  
    1.11  fun writeTextFile name s = File.write (Path.explode name) s
     2.1 --- a/src/HOL/Matrix/Cplex_tools.ML	Thu Jun 30 11:15:36 2011 +0200
     2.2 +++ b/src/HOL/Matrix/Cplex_tools.ML	Thu Jun 30 13:21:41 2011 +0200
     2.3 @@ -1129,7 +1129,7 @@
     2.4  
     2.5  exception Execute of string;
     2.6  
     2.7 -fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
     2.8 +fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
     2.9  fun wrap s = "\""^s^"\"";
    2.10  
    2.11  fun solve_glpk prog =
     3.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Jun 30 11:15:36 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Jun 30 13:21:41 2011 +0200
     3.3 @@ -142,9 +142,7 @@
     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 -    Path.print (Path.expand (Path.appends
     3.8 -               (Path.variable "ISABELLE_HOME_USER" ::
     3.9 -                map Path.basic ["etc", "components"]))) ^
    3.10 +    Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
    3.11      " on a line of its own."
    3.12    | string_for_failure VampireTooOld =
    3.13      "Isabelle requires a more recent version of Vampire. To install it, follow \
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jun 30 11:15:36 2011 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jun 30 13:21:41 2011 +0200
     4.3 @@ -183,9 +183,8 @@
     4.4    "Nitpick requires the external Java program Kodkodi. To install it, download \
     4.5    \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
     4.6    \directory's full path to " ^
     4.7 -  Path.print (Path.expand (Path.appends
     4.8 -      (Path.variable "ISABELLE_HOME_USER" ::
     4.9 -       map Path.basic ["etc", "components"]))) ^ " on a line of its own."
    4.10 +  Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^
    4.11 +  " on a line of its own."
    4.12  
    4.13  val max_unsound_delay_ms = 200
    4.14  val max_unsound_delay_percent = 2
     5.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 30 11:15:36 2011 +0200
     5.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 30 13:21:41 2011 +0200
     5.3 @@ -206,7 +206,8 @@
     5.4  
     5.5  fun with_overlord_dir name f =
     5.6    let
     5.7 -    val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
     5.8 +    val path =
     5.9 +      Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
    5.10      val _ = Isabelle_System.mkdirs path;
    5.11    in Exn.release (Exn.capture f path) end;
    5.12  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jun 30 11:15:36 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jun 30 13:21:41 2011 +0200
     6.3 @@ -703,7 +703,7 @@
     6.4              |> fold maybe_run_slice actual_slices
     6.5            end
     6.6          else
     6.7 -          error ("Bad executable: " ^ Path.print 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/ex/atp_export.ML	Thu Jun 30 11:15:36 2011 +0200
     7.2 +++ b/src/HOL/ex/atp_export.ML	Thu Jun 30 13:21:41 2011 +0200
     7.3 @@ -112,7 +112,7 @@
     7.4  fun run_some_atp ctxt problem =
     7.5    let
     7.6      val thy = Proof_Context.theory_of ctxt
     7.7 -    val prob_file = Path.explode "/tmp/prob.tptp"
     7.8 +    val prob_file = Path.explode "/tmp/prob.tptp"  (* FIXME File.tmp_path (?) *)
     7.9      val {exec, arguments, proof_delims, known_failures, ...} =
    7.10        get_atp thy spassN
    7.11      val _ = problem |> tptp_lines_for_atp_problem FOF
     8.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Thu Jun 30 11:15:36 2011 +0200
     8.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Thu Jun 30 13:21:41 2011 +0200
     8.3 @@ -135,11 +135,6 @@
     8.4  
     8.5  val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
     8.6  
     8.7 -val symbols_path =
     8.8 -  [getenv "ISABELLE_HOME", "etc", "symbols"]
     8.9 -  |> map Path.explode
    8.10 -  |> Path.appends;
    8.11 -
    8.12  end;
    8.13  
    8.14  local (* build tables *)
    8.15 @@ -164,8 +159,7 @@
    8.16  fun read_symbols path =
    8.17    let
    8.18      val parsed_lines =
    8.19 -      File.read path
    8.20 -      |> (fn x => Symbol_Pos.explode (x, Position.file (Path.implode path)))
    8.21 +      Symbol_Pos.explode (File.read path, Path.position path)
    8.22        |> tokenize
    8.23        |> filter is_proper
    8.24        |> Scan.finite stopper (Scan.repeat line)
    8.25 @@ -179,7 +173,7 @@
    8.26  end;
    8.27  
    8.28  local
    8.29 -val (fromsym, fromabbr, tosym, toabbr) = read_symbols symbols_path;
    8.30 +val (fromsym, fromabbr, tosym, toabbr) = read_symbols (Path.explode "~~/etc/symbols");
    8.31  in
    8.32  val symbol_to_unicode = Symtab.lookup fromsym;
    8.33  val abbrev_to_unicode = Symtab.lookup fromabbr;