# HG changeset patch
# User wenzelm
# Date 1428833272 -7200
# Node ID 9f5b287279c812bc5fc4a2379eb1499e7a397d64
# Parent  41d81b4a0a213a0716d7d9d8ee8b52d2eb66aad9# Parent  b2acd53016158446647cd79dd6dfa119c4f71f41
merged

diff -r 41d81b4a0a21 -r 9f5b287279c8 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Sun Apr 12 11:00:56 2015 +0100
+++ b/src/HOL/Library/Countable.thy	Sun Apr 12 12:07:52 2015 +0200
@@ -202,9 +202,9 @@
 
 ML {*
 fun countable_datatype_tac ctxt st =
-  HEADGOAL (old_countable_datatype_tac ctxt) st
-  handle exn =>
-    if Exn.is_interrupt exn then reraise exn else BNF_LFP_Countable.countable_datatype_tac ctxt st;
+  (case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of
+    SOME res => res
+  | NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st);
 
 (* compatibility *)
 fun countable_tac ctxt =
diff -r 41d81b4a0a21 -r 9f5b287279c8 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Apr 12 11:00:56 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Sun Apr 12 12:07:52 2015 +0200
@@ -92,7 +92,8 @@
                   Exn.interruptible_capture (fn () =>
                     read_file_node file_node master_dir pos src_path) ()
               | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
-                  Exn.Res (blob_file src_path lines digest file_node)
+                  (Position.report pos Markup.language_path;
+                    Exn.Res (blob_file src_path lines digest file_node))
               | make_file _ (Exn.Exn e) = Exn.Exn e;
             val src_paths = Keyword.command_files keywords cmd path;
             val files =
diff -r 41d81b4a0a21 -r 9f5b287279c8 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Apr 12 11:00:56 2015 +0100
+++ b/src/Pure/PIDE/document.ML	Sun Apr 12 12:07:52 2015 +0200
@@ -388,10 +388,8 @@
                     map_filter Exn.get_exn blobs_digests
                     |> List.app (Output.error_message o Runtime.exn_message)
                   else (*auxiliary files*)
-                    let val pos = Token.pos_of (nth tokens blobs_index) in
-                      Position.reports
-                        ((pos, Markup.language_path) :: maps (blob_reports pos) blobs_digests)
-                    end;
+                    let val pos = Token.pos_of (nth tokens blobs_index)
+                    in Position.reports (maps (blob_reports pos) blobs_digests) end;
               in tokens end) ());
       val commands' =
         Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands
diff -r 41d81b4a0a21 -r 9f5b287279c8 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sun Apr 12 11:00:56 2015 +0100
+++ b/src/Pure/System/isabelle_system.ML	Sun Apr 12 12:07:52 2015 +0200
@@ -59,9 +59,8 @@
 (* directory operations *)
 
 fun mkdirs path =
-  if #rc (Bash.process ("mkdir -p " ^ File.shell_path path)) <> 0 then
-    error ("Failed to create directory: " ^ Path.print path)
-  else ();
+  if File.is_dir path orelse #rc (Bash.process ("mkdir -p " ^ File.shell_path path)) = 0 then ()
+  else error ("Failed to create directory: " ^ Path.print path);
 
 fun mkdir path =
   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
diff -r 41d81b4a0a21 -r 9f5b287279c8 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Apr 12 11:00:56 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Apr 12 12:07:52 2015 +0200
@@ -257,8 +257,8 @@
   /* mkdirs */
 
   def mkdirs(path: Path): Unit =
-    if (bash("mkdir -p " + shell_path(path)).rc != 0)
-      error("Failed to create directory: " + quote(platform_path(path)))
+    if (path.is_dir || bash("mkdir -p " + shell_path(path)).rc == 0) ()
+    else error("Failed to create directory: " + quote(platform_path(path)))