# HG changeset patch
# User wenzelm
# Date 1296934712 -3600
# Node ID 3422ae5aff3a351a7f7bbc0097400f84cb055413
# Parent  11ae688e4e3028f38d68d78624e1911d9a821d2e
more tracing information via Par_List.map_name;

diff -r 11ae688e4e30 -r 3422ae5aff3a src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Sat Feb 05 18:09:57 2011 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Sat Feb 05 20:38:32 2011 +0100
@@ -16,6 +16,7 @@
 
 signature PAR_LIST =
 sig
+  val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
   val map: ('a -> 'b) -> 'a list -> 'b list
   val get_some: ('a -> 'b option) -> 'a list -> 'b option
   val find_some: ('a -> bool) -> 'a list -> 'a option
@@ -40,7 +41,8 @@
         handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
     in results end;
 
-fun map f xs = Exn.release_first (managed_results "Par_List.map" f xs);
+fun map_name name f xs = Exn.release_first (managed_results name f xs);
+fun map f = map_name "Par_List.map" f;
 
 fun get_some f xs =
   let
diff -r 11ae688e4e30 -r 3422ae5aff3a src/Pure/Concurrent/par_list_sequential.ML
--- a/src/Pure/Concurrent/par_list_sequential.ML	Sat Feb 05 18:09:57 2011 +0100
+++ b/src/Pure/Concurrent/par_list_sequential.ML	Sat Feb 05 20:38:32 2011 +0100
@@ -7,6 +7,7 @@
 structure Par_List: PAR_LIST =
 struct
 
+fun map_name _ = map;
 val map = map;
 val get_some = get_first;
 val find_some = find_first;
diff -r 11ae688e4e30 -r 3422ae5aff3a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Feb 05 18:09:57 2011 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Feb 05 20:38:32 2011 +0100
@@ -279,7 +279,7 @@
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
     val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
     val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans))
-      |> Par_List.map (prepare_atom commands init) |> flat;
+      |> Par_List.map_name "Outer_Syntax.prepare_atom" (prepare_atom commands init) |> flat;
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
diff -r 11ae688e4e30 -r 3422ae5aff3a src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Feb 05 18:09:57 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Feb 05 20:38:32 2011 +0100
@@ -756,7 +756,7 @@
             \Retry with smaller syntax_ambiguity_level for more information."
           else "";
 
-        val errs = Par_List.map check ts;
+        val errs = Par_List.map_name "Syntax.disambig" check ts;
         val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
         val len = length results;
 
diff -r 11ae688e4e30 -r 3422ae5aff3a src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Feb 05 18:09:57 2011 +0100
+++ b/src/Pure/context.ML	Sat Feb 05 20:38:32 2011 +0100
@@ -141,7 +141,7 @@
 
 fun merge_data pp (data1, data2) =
   Datatab.keys (Datatab.merge (K true) (data1, data2))
-  |> Par_List.map (fn k =>
+  |> Par_List.map_name "Context.merge_data" (fn k =>
     (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
       (SOME x, NONE) => (k, invoke_extend k x)
     | (NONE, SOME y) => (k, invoke_extend k y)