--- a/.hgtags Sat Apr 11 22:18:33 2015 +0100
+++ b/.hgtags Sat Apr 11 22:19:09 2015 +0100
@@ -29,3 +29,4 @@
9c1f2136532626c7cb5fae14a2aeac53be3aeb67 Isabelle2013-1
4dd08fe126bad63aa05741d55fb3e86a2dbfc795 Isabelle2013-2
8f4a332500e41bb67efc3e141608829473606a72 Isabelle2014
+42d34eeb283c645de7792a327e86d846f9cfb5f9 Isabelle2015-RC0
--- a/ANNOUNCE Sat Apr 11 22:18:33 2015 +0100
+++ b/ANNOUNCE Sat Apr 11 22:19:09 2015 +0100
@@ -1,40 +1,15 @@
-Subject: Announcing Isabelle2014
+Subject: Announcing Isabelle2015
To: isabelle-users@cl.cam.ac.uk
-Isabelle2014 is now available.
-
-This version significantly improves upon Isabelle2013-2, see the NEWS
-file in the distribution for more details. Some highlights are:
-
-* Improved Isabelle/jEdit Prover IDE: navigation, completion,
- spell-checking, Query panel, Simplifier Trace panel.
-
-* Support for auxiliary files within the Prover IDE, notably
- Isabelle/ML.
-
-* Support for official Standard ML within the Prover IDE,
- independently of Isabelle theory and proof development.
+Isabelle2015 is now available.
-* HOL: BNF datatypes and codatatypes within theory Main, with numerous
- add-on tools.
-
-* HOL tool enhancements: Nitpick, Sledgehammer.
-
-* HOL: internal SAT solver "cdclite" with models and proof traces.
+This version improves upon Isabelle2014 in many ways, see the NEWS file in
+the distribution for more details. Important points are:
-* HOL: updated SMT module, with support for SMT-LIB 2 and recent
- versions of Z3, as well as CVC3, CVC4.
-
-* HOL: numerous library enhancements: main HOL, HOL-Word,
- HOL-Multivariate_Analysis, HOL-Probability.
-
-* System integration: improved support of LaTeX on Windows platform.
-
-* Updated and extended manuals: codegen, datatypes, implementation,
- isar-ref, jedit, system.
+* FIXME
-You may get Isabelle2014 from the following mirror sites:
+You may get Isabelle2015 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
--- a/Admin/Windows/Cygwin/README Sat Apr 11 22:18:33 2015 +0100
+++ b/Admin/Windows/Cygwin/README Sat Apr 11 22:19:09 2015 +0100
@@ -11,5 +11,6 @@
http://isabelle.in.tum.de/cygwin_2013 (Isabelle2013)
http://isabelle.in.tum.de/cygwin_2013-1 (Isabelle2013-1 and Isabelle2013-2)
http://isabelle.in.tum.de/cygwin_2014 (Isabelle2014)
+ http://isabelle.in.tum.de/cygwin_2015 (Isabelle2015)
* Quasi-component: "isabelle makedist_cygwin" (as administrator)
--- a/CONTRIBUTORS Sat Apr 11 22:18:33 2015 +0100
+++ b/CONTRIBUTORS Sat Apr 11 22:19:09 2015 +0100
@@ -3,8 +3,8 @@
who is listed as an author in one of the source files of this Isabelle
distribution.
-Contributions to this Isabelle version
---------------------------------------
+Contributions to Isabelle2015
+-----------------------------
* March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII,
and Dmitriy Traytel, TUM
--- a/src/Pure/System/isabelle_system.ML Sat Apr 11 22:18:33 2015 +0100
+++ b/src/Pure/System/isabelle_system.ML Sat Apr 11 22:19:09 2015 +0100
@@ -58,7 +58,10 @@
(* directory operations *)
-fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
+fun mkdirs path =
+ if #rc (Bash.process ("mkdir -p " ^ File.shell_path path)) <> 0 then
+ error ("Failed to create directory: " ^ Path.print path)
+ else ();
fun mkdir path =
if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
--- a/src/Pure/System/isabelle_system.scala Sat Apr 11 22:18:33 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Apr 11 22:19:09 2015 +0100
@@ -256,11 +256,9 @@
/* mkdirs */
- def mkdirs(path: Path)
- {
- path.file.mkdirs
- if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path)))
- }
+ def mkdirs(path: Path): Unit =
+ if (bash("mkdir -p " + shell_path(path)).rc != 0)
+ error("Failed to create directory: " + quote(platform_path(path)))
@@ -388,7 +386,7 @@
private def isabelle_tmp_prefix(): JFile =
{
val path = Path.explode("$ISABELLE_TMP_PREFIX")
- mkdirs(path)
+ path.file.mkdirs // low-level mkdirs
platform_file(path)
}