merged

--- a/src/Pure/Isar/runtime.ML	Wed Oct 19 17:45:25 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Oct 19 19:45:19 2011 +0200
@@ -126,8 +126,11 @@
     if Exn.is_interrupt exn then reraise exn
     else
       let
-        val ctxt = Option.map Context.proof_of (Context.thread_data ());
-        val _ = output_exn (exn_context ctxt exn);
+        val opt_ctxt =
+          (case Context.thread_data () of
+            NONE => NONE
+          | SOME context => try Context.proof_of context);
+        val _ = output_exn (exn_context opt_ctxt exn);
       in raise TOPLEVEL_ERROR end;
 
 end;

--- a/src/Pure/ML/ml_thms.ML	Wed Oct 19 17:45:25 2011 +0200
+++ b/src/Pure/ML/ml_thms.ML	Wed Oct 19 19:45:19 2011 +0200
@@ -52,7 +52,7 @@
 
 val and_ = Args.$$$ "and";
 val by = Args.$$$ "by";
-val goal = Scan.unless (by || and_) Args.name;
+val goal = Scan.unless (by || and_) Args.name_source;
 
 val _ =
   Context.>> (Context.map_theory

--- a/src/Pure/System/isabelle_system.ML	Wed Oct 19 17:45:25 2011 +0200
+++ b/src/Pure/System/isabelle_system.ML	Wed Oct 19 19:45:19 2011 +0200
@@ -96,7 +96,9 @@
         (_, 0) => f path
       | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
 
-fun bash_output_fifo script f =  (* FIXME blocks on Cygwin 1.7.x *)
+(* FIXME blocks on Cygwin 1.7.x *)
+(* See also http://cygwin.com/ml/cygwin/2010-08/msg00459.html *)
+fun bash_output_fifo script f =
   with_tmp_fifo (fn fifo =>
     uninterruptible (fn restore_attributes => fn () =>
       (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of