# HG changeset patch
# User wenzelm
# Date 1319046319 -7200
# Node ID fe8d0706a8aa2612350c320b19d86b63d51e9c5c
# Parent  2825ce94fd4d1d345d554c9064266c65f6170c25# Parent  42316b81ef49b5f905fa8201ee08c3be11d3e954
merged

diff -r 2825ce94fd4d -r fe8d0706a8aa src/Pure/Isar/runtime.ML
--- 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;
diff -r 2825ce94fd4d -r fe8d0706a8aa src/Pure/ML/ml_thms.ML
--- 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
diff -r 2825ce94fd4d -r fe8d0706a8aa src/Pure/System/isabelle_system.ML
--- 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