# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1428787149 -3600
# Node ID 69e7fe18b7db43c3967e62008d40a68259c5cd5b
# Parent  065ecea354d08faee8027040e23b3beec1f41260# Parent  6e6cc8c012a2424e17fa5768066863e348dad712
Merge

diff -r 065ecea354d0 -r 69e7fe18b7db .hgtags
--- 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
diff -r 065ecea354d0 -r 69e7fe18b7db ANNOUNCE
--- 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/
diff -r 065ecea354d0 -r 69e7fe18b7db Admin/Windows/Cygwin/README
--- 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)
diff -r 065ecea354d0 -r 69e7fe18b7db CONTRIBUTORS
--- 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
diff -r 065ecea354d0 -r 69e7fe18b7db src/Pure/System/isabelle_system.ML
--- 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);
diff -r 065ecea354d0 -r 69e7fe18b7db src/Pure/System/isabelle_system.scala
--- 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)
   }