# 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)