--- a/NEWS Mon Oct 26 21:35:39 2020 +0100
+++ b/NEWS Tue Oct 27 22:34:37 2020 +0100
@@ -184,6 +184,9 @@
registered Isabelle/Scala functions (of type String => String):
invocation works via the PIDE protocol.
+* Path.append is available as overloaded "+" operator, similar to
+corresponding Isabelle/Scala operation.
+
*** System ***
--- a/src/HOL/Library/code_test.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Library/code_test.ML Tue Oct 27 22:34:37 2020 +0100
@@ -140,7 +140,7 @@
val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)
fun with_debug_dir name f =
- Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
+ (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
|> Isabelle_System.make_directory
|> Exn.capture f
|> Exn.release;
@@ -290,9 +290,9 @@
fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir =
let
- val code_path = Path.append dir (Path.basic "generated.sml")
- val driver_path = Path.append dir (Path.basic "driver.sml")
- val out_path = Path.append dir (Path.basic "out")
+ val code_path = dir + Path.basic "generated.sml"
+ val driver_path = dir + Path.basic "driver.sml"
+ val out_path = dir + Path.basic "out"
val code = #2 (the_single code_files)
val driver = \<^verbatim>\<open>
@@ -337,9 +337,9 @@
val driverN = "driver.sml"
val projectN = "test"
- val code_path = Path.append dir (Path.basic generatedN)
- val driver_path = Path.append dir (Path.basic driverN)
- val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb"))
+ val code_path = dir + Path.basic generatedN
+ val driver_path = dir + Path.basic driverN
+ val basis_path = dir + Path.basic (projectN ^ ".mlb")
val driver = \<^verbatim>\<open>
fun format (true, _) = \<close> ^ ML_Syntax.print_string success ^ \<^verbatim>\<open> ^ "\n"
| format (false, NONE) = \<close> ^ ML_Syntax.print_string failure ^ \<^verbatim>\<open> ^ "\n"
@@ -355,7 +355,7 @@
val _ = File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN)
in
compile compiler ("\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path);
- evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN)))
+ evaluate compiler (File.bash_path (dir + Path.basic projectN))
end
@@ -370,8 +370,8 @@
val generatedN = "generated.sml"
val driverN = "driver.sml"
- val code_path = Path.append dir (Path.basic generatedN)
- val driver_path = Path.append dir (Path.basic driverN)
+ val code_path = dir + Path.basic generatedN
+ val driver_path = dir + Path.basic driverN
val driver = \<^verbatim>\<open>
structure Test =
struct
@@ -407,8 +407,8 @@
let
val compiler = ocamlN
- val code_path = Path.append dir (Path.basic "generated.ml")
- val driver_path = Path.append dir (Path.basic "driver.ml")
+ val code_path = dir + Path.basic "generated.ml"
+ val driver_path = dir + Path.basic "driver.ml"
val driver =
"let format_term = function\n" ^
" | None -> \"\"\n" ^
@@ -422,7 +422,7 @@
" let _ = List.map (fun x -> print_string (format x)) result in\n" ^
" print_string \"" ^ end_marker ^ "\";;\n" ^
"main ();;"
- val compiled_path = Path.append dir (Path.basic "test")
+ val compiled_path = dir + Path.basic "test"
val _ = check_settings compiler ISABELLE_OCAMLFIND "ocamlfind executable"
val _ = List.app (File.write code_path o snd) code_files
@@ -446,7 +446,7 @@
val compiler = ghcN
val modules = map fst code_files
- val driver_path = Path.append dir (Path.basic "Main.hs")
+ val driver_path = dir + Path.basic "Main.hs"
val driver =
"module Main where {\n" ^
implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
@@ -465,10 +465,10 @@
"}\n"
val _ = check_settings compiler ISABELLE_GHC "GHC executable"
- val _ = List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files
+ val _ = List.app (fn (name, code) => File.write (dir + Path.basic name) code) code_files
val _ = File.write driver_path driver
- val compiled_path = Path.append dir (Path.basic "test")
+ val compiled_path = dir + Path.basic "test"
val cmd =
"\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
Config.get ctxt ghc_options ^ " -o " ^
@@ -487,9 +487,9 @@
val generatedN = "Generated_Code"
val driverN = "Driver.scala"
- val code_path = Path.append dir (Path.basic (generatedN ^ ".scala"))
- val driver_path = Path.append dir (Path.basic driverN)
- val out_path = Path.append dir (Path.basic "out")
+ val code_path = dir + Path.basic (generatedN ^ ".scala")
+ val driver_path = dir + Path.basic driverN
+ val out_path = dir + Path.basic "out"
val code = #2 (the_single code_files)
val driver = \<^verbatim>\<open>
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Tue Oct 27 22:34:37 2020 +0100
@@ -18,7 +18,7 @@
(TPTP_Interpret.interpret_file
false
[Path.explode "$TPTP"]
- (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
+ (tptp_probs_dir + Path.explode "LCL/LCL825-1.p")
[]
[])
@{theory}
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Tue Oct 27 22:34:37 2020 +0100
@@ -782,9 +782,9 @@
| dest_fn_type ty = ([], ty)
fun resolve_include_path path_prefixes path_suffix =
- case find_first (fn prefix => File.exists (Path.append prefix path_suffix))
+ case find_first (fn prefix => File.exists (prefix + path_suffix))
path_prefixes of
- SOME prefix => Path.append prefix path_suffix
+ SOME prefix => prefix + path_suffix
| NONE => error ("Cannot find include file " ^ Path.print path_suffix)
fun is_type_type (Fmla_type (Atom (THF_Atom_term (Term_FuncG (TypeSymbol Type_Type, [], []))))) =
--- a/src/HOL/TPTP/TPTP_Test.thy Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy Tue Oct 27 22:34:37 2020 +0100
@@ -89,7 +89,7 @@
ML \<open>
- fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
+ fun situate file_name = tptp_probs_dir + Path.explode file_name;
fun parser_test ctxt = (*FIXME argument order*)
test_fn ctxt
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Oct 27 22:34:37 2020 +0100
@@ -209,7 +209,7 @@
{line = 0, file = "generated code", verbose = verbose, debug = false} code)
fun with_overlord_dir name f =
- Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
+ (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
|> Isabelle_System.make_directory
|> Exn.capture f
|> Exn.release
@@ -258,7 +258,7 @@
[(narrowing_engine_file,
if contains_existentials then pnf_narrowing_engine else narrowing_engine),
(code_file, code), (main_file, main)])
- val executable = Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")
+ val executable = in_path + Path.basic "isabelle_quickcheck_narrowing"
val cmd =
"exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
(space_implode " "
--- a/src/HOL/Tools/SMT/smt_config.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Tue Oct 27 22:34:37 2020 +0100
@@ -234,8 +234,7 @@
fun select_certificates name context = context |> Data.map (put_certs (
if name = "" then NONE
else
- Path.explode name
- |> Path.append (Resources.master_directory (Context.theory_of context))
+ (Resources.master_directory (Context.theory_of context) + Path.explode name)
|> SOME o Cache_IO.unsynchronized_init))
val setup_certificates =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Oct 27 22:34:37 2020 +0100
@@ -155,7 +155,7 @@
if dest_dir = "" then
File.tmp_path problem_file_name
else if File.exists (Path.explode dest_dir) then
- Path.append (Path.explode dest_dir) problem_file_name
+ Path.explode dest_dir + problem_file_name
else
error ("No such directory: " ^ quote dest_dir)
val exec = exec full_proofs
--- a/src/Pure/General/file.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/General/file.ML Tue Oct 27 22:34:37 2020 +0100
@@ -60,17 +60,16 @@
let
val path' = Path.expand path;
val _ = Path.is_current path' andalso error "Bad file specification";
- val path'' = Path.append dir path';
+ val path'' = dir + path';
in
if Path.is_absolute path'' then path''
- else Path.append (Path.explode (ML_System.standard_path (OS.FileSys.getDir ()))) path''
+ else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path''
end;
(* tmp_path *)
-fun tmp_path path =
- Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
+fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path;
(* directory entries *)
--- a/src/Pure/General/path.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/General/path.ML Tue Oct 27 22:34:37 2020 +0100
@@ -294,3 +294,5 @@
val explode = explode_path;
end;
+
+ML_system_overload (uncurry Path.append) "+";
--- a/src/Pure/General/url.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/General/url.ML Tue Oct 27 22:34:37 2020 +0100
@@ -32,10 +32,10 @@
(* append *)
-fun append (File p) (File p') = File (Path.append p p')
- | append (Http (h, p)) (File p') = Http (h, Path.append p p')
- | append (Https (h, p)) (File p') = Https (h, Path.append p p')
- | append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p')
+fun append (File p) (File p') = File (p + p')
+ | append (Http (h, p)) (File p') = Http (h, p + p')
+ | append (Https (h, p)) (File p') = Https (h, p + p')
+ | append (Ftp (h, p)) (File p') = Ftp (h, p + p')
| append _ url = url;
@@ -67,7 +67,7 @@
Scan.this_string "file:///" |-- scan_path_root >> File ||
Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
Scan.this_string "file://" |-- scan_host -- scan_path
- >> (fn (h, p) => File (Path.append (Path.named_root h) p)) ||
+ >> (fn (h, p) => File (Path.named_root h + p)) ||
Scan.this_string "file:/" |-- scan_path_root >> File ||
Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
Scan.this_string "https://" |-- scan_host -- scan_path >> Https ||
--- a/src/Pure/PIDE/resources.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/PIDE/resources.ML Tue Oct 27 22:34:37 2020 +0100
@@ -155,7 +155,7 @@
val dirs = Symtab.lookup_list (get_session_base #session_directories) session;
in
dirs |> get_first (fn dir =>
- let val path = Path.append dir thy_file
+ let val path = dir + thy_file
in if File.is_file path then SOME path else NONE end)
end;
@@ -257,7 +257,7 @@
(case opt_dir of
SOME dir => dir
| NONE => master_directory (Proof_Context.theory_of ctxt));
- val path = Path.append dir (Path.explode name) handle ERROR msg => err msg;
+ val path = dir + Path.explode name handle ERROR msg => err msg;
val _ = Path.expand path handle ERROR msg => err msg;
val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
val _ = check_file path handle ERROR msg => err msg;
--- a/src/Pure/System/isabelle_system.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/System/isabelle_system.ML Tue Oct 27 22:34:37 2020 +0100
@@ -83,7 +83,7 @@
let
val src = Path.expand src0;
val dst = Path.expand dst0;
- val target = if File.is_dir dst then Path.append dst (Path.base src) else dst;
+ val target = if File.is_dir dst then dst + Path.base src else dst;
in
if File.eq (src, target) then ()
else
@@ -97,7 +97,7 @@
val _ =
if Path.starts_basic src then ()
else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
- in copy_file (Path.append base_dir src) (make_directory (Path.append target_dir src_dir)) end;
+ in copy_file (base_dir + src) (make_directory (target_dir + src_dir)) end;
(* tmp files *)
--- a/src/Pure/Thy/export.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Thy/export.ML Tue Oct 27 22:34:37 2020 +0100
@@ -27,7 +27,7 @@
let
val theory_name = Context.theory_long_name thy;
val (path, pos) = Path.dest_binding binding;
- val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path));
+ val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
in Context_Position.report_generic (Context.Theory thy) pos markup end;
type params =
@@ -63,7 +63,7 @@
fun markup thy path =
let
- val thy_path = Path.append (Path.basic (Context.theory_long_name thy)) path;
+ val thy_path = Path.basic (Context.theory_long_name thy) + path;
val name = (Markup.nameN, Path.implode thy_path);
in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;
--- a/src/Pure/Thy/present.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Thy/present.ML Tue Oct 27 22:34:37 2020 +0100
@@ -205,7 +205,7 @@
val script =
"isabelle document -d " ^ File.bash_path dir ^ " -n " ^ Bash.string doc_name ^
(if tags = "" then "" else " -t " ^ Bash.string tags);
- val doc_path = Path.appends [dir, Path.parent, document_path doc_name];
+ val doc_path = dir + Path.parent + document_path doc_name;
val _ = if verbose then writeln script else ();
val {out, err, rc, ...} = Bash.process script;
val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
@@ -219,7 +219,7 @@
fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
fun write_tex src name path =
- File.write_buffer (Path.append path (tex_path name)) src;
+ File.write_buffer (path + tex_path name) src;
fun write_tex_index tex_index path =
write_tex (index_buffer tex_index) doc_indexN path;
@@ -231,16 +231,15 @@
val {theories, tex_index, html_index} = Synchronized.value browser_info;
val thys = Symtab.dest theories;
- val session_prefix =
- Path.append (Path.append info_path (Path.basic chapter)) (Path.basic name);
+ val session_prefix = info_path + Path.basic chapter + Path.basic name;
fun finish_html (a, {html_source, ...}: theory_info) =
- File.write (Path.append session_prefix (html_path a)) html_source;
+ File.write (session_prefix + html_path a) html_source;
val _ =
if info then
(Isabelle_System.make_directory session_prefix;
- File.write_buffer (Path.append session_prefix index_path)
+ File.write_buffer (session_prefix + index_path)
(index_buffer html_index |> Buffer.add HTML.end_document);
(case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
List.app finish_html thys;
@@ -251,15 +250,15 @@
fun document_job doc_prefix backdrop (doc_name, tags) =
let
- val doc_dir = Path.append doc_prefix (Path.basic doc_name);
+ val doc_dir = doc_prefix + Path.basic doc_name;
fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else ();
val _ = purge ();
val _ = Isabelle_System.make_directory doc_dir;
val _ =
Isabelle_System.bash ("isabelle latex -o sty " ^
- File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
+ File.bash_path (doc_dir + Path.basic "root.tex"));
val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
- val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
+ val _ = Isabelle_System.copy_file graph_file (doc_dir + session_graph_path);
val _ = write_tex_index tex_index doc_dir;
val _ =
List.app (fn (a, {tex_source, ...}) =>
@@ -303,9 +302,9 @@
in
if curr_session = session then SOME link
else if curr_chapter = chapter then
- SOME (Path.appends [Path.parent, Path.basic session, link])
+ SOME (Path.parent + Path.basic session + link)
else if chapter = Context.PureN then NONE
- else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
+ else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link)
end;
fun begin_theory bibtex_entries update_time mk_text thy =
--- a/src/Pure/Thy/thy_info.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Oct 27 22:34:37 2020 +0100
@@ -67,7 +67,7 @@
else
let
val thy_name = Context.theory_name thy;
- val document_path = Path.append (Path.basic "document") (Present.tex_path thy_name);
+ val document_path = Path.basic "document" + Present.tex_path thy_name;
val latex = Latex.isabelle_body thy_name body;
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
@@ -416,7 +416,7 @@
Position.here require_pos ^ required_by "\n" initiators);
val qualifier' = Resources.theory_qualifier theory_name;
- val dir' = Path.append dir (master_dir_deps (Option.map #1 deps));
+ val dir' = dir + master_dir_deps (Option.map #1 deps);
val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
val (parents_current, tasks') =
--- a/src/Pure/Tools/generated_files.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Tools/generated_files.ML Tue Oct 27 22:34:37 2020 +0100
@@ -146,7 +146,7 @@
fun write_file dir (file: file) =
let
- val path = Path.expand (Path.append dir (#path file));
+ val path = Path.expand (dir + #path file);
val _ = Isabelle_System.make_directory (Path.dir path);
val _ = File.generate path (#content file);
in () end;
@@ -298,7 +298,7 @@
val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
val (path, pos) = Path.dest_binding binding;
val content =
- (case try File.read (Path.append dir path) of
+ (case try File.read (dir + path) of
SOME context => context
| NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
val _ = Export.report_export thy export_prefix;
--- a/src/Pure/Tools/ghc.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Tools/ghc.ML Tue Oct 27 22:34:37 2020 +0100
@@ -81,7 +81,7 @@
fun new_project dir {name, depends, modules} =
let
- val template_path = Path.append dir (Path.basic name |> Path.ext "hsfiles");
+ val template_path = dir + (Path.basic name |> Path.ext "hsfiles");
val _ = File.write template_path (project_template {depends = depends, modules = modules});
val {rc, err, ...} =
Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^
--- a/src/Tools/Code/code_ml.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Tools/Code/code_ml.ML Tue Oct 27 22:34:37 2020 +0100
@@ -879,14 +879,14 @@
(Code_Target.add_language
(target_SML, {serializer = serializer_sml, literals = literals_sml,
check = {env_var = "",
- make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
+ make_destination = fn p => p + Path.explode "ROOT.ML",
make_command = fn _ =>
"isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure"},
evaluation_args = []})
#> Code_Target.add_language
(target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
check = {env_var = "ISABELLE_OCAMLFIND",
- make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
+ make_destination = fn p => p + Path.explode "ROOT.ml"
(*extension demanded by OCaml compiler*),
make_command = fn _ =>
"\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"},
--- a/src/Tools/Code/code_scala.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Tools/Code/code_scala.ML Tue Oct 27 22:34:37 2020 +0100
@@ -465,7 +465,7 @@
(Code_Target.add_language
(target, { serializer = serializer, literals = literals,
check = { env_var = "SCALA_HOME",
- make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
+ make_destination = fn p => p + Path.explode "ROOT.scala",
make_command = fn _ =>
"isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"},
evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"})
--- a/src/Tools/Code/code_target.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Tools/Code/code_target.ML Tue Oct 27 22:34:37 2020 +0100
@@ -304,7 +304,7 @@
Singleton (ext, p) => export (binding (Path.ext ext prefix)) (format p)
| Hierarchy modules =>
fold (fn (names, p) =>
- export (binding (Path.append prefix (Path.make names))) (format p)) modules)
+ export (binding (prefix + Path.make names)) (format p)) modules)
#> tap code_export_message
end;