more tracing information via Par_List.map_name;
authorwenzelm
Sat Feb 05 20:38:32 2011 +0100 (2011-02-05)
changeset 417113422ae5aff3a
parent 41710 11ae688e4e30
child 41712 82339c3fd74a
child 41719 91c2510e19c5
more tracing information via Par_List.map_name;
src/Pure/Concurrent/par_list.ML
src/Pure/Concurrent/par_list_sequential.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Syntax/syntax.ML
src/Pure/context.ML
     1.1 --- a/src/Pure/Concurrent/par_list.ML	Sat Feb 05 18:09:57 2011 +0100
     1.2 +++ b/src/Pure/Concurrent/par_list.ML	Sat Feb 05 20:38:32 2011 +0100
     1.3 @@ -16,6 +16,7 @@
     1.4  
     1.5  signature PAR_LIST =
     1.6  sig
     1.7 +  val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
     1.8    val map: ('a -> 'b) -> 'a list -> 'b list
     1.9    val get_some: ('a -> 'b option) -> 'a list -> 'b option
    1.10    val find_some: ('a -> bool) -> 'a list -> 'a option
    1.11 @@ -40,7 +41,8 @@
    1.12          handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
    1.13      in results end;
    1.14  
    1.15 -fun map f xs = Exn.release_first (managed_results "Par_List.map" f xs);
    1.16 +fun map_name name f xs = Exn.release_first (managed_results name f xs);
    1.17 +fun map f = map_name "Par_List.map" f;
    1.18  
    1.19  fun get_some f xs =
    1.20    let
     2.1 --- a/src/Pure/Concurrent/par_list_sequential.ML	Sat Feb 05 18:09:57 2011 +0100
     2.2 +++ b/src/Pure/Concurrent/par_list_sequential.ML	Sat Feb 05 20:38:32 2011 +0100
     2.3 @@ -7,6 +7,7 @@
     2.4  structure Par_List: PAR_LIST =
     2.5  struct
     2.6  
     2.7 +fun map_name _ = map;
     2.8  val map = map;
     2.9  val get_some = get_first;
    2.10  val find_some = find_first;
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Feb 05 18:09:57 2011 +0100
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Feb 05 20:38:32 2011 +0100
     3.3 @@ -279,7 +279,7 @@
     3.4      val spans = Source.exhaust (Thy_Syntax.span_source toks);
     3.5      val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
     3.6      val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans))
     3.7 -      |> Par_List.map (prepare_atom commands init) |> flat;
     3.8 +      |> Par_List.map_name "Outer_Syntax.prepare_atom" (prepare_atom commands init) |> flat;
     3.9  
    3.10      val _ = Present.theory_source name
    3.11        (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
     4.1 --- a/src/Pure/Syntax/syntax.ML	Sat Feb 05 18:09:57 2011 +0100
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Feb 05 20:38:32 2011 +0100
     4.3 @@ -756,7 +756,7 @@
     4.4              \Retry with smaller syntax_ambiguity_level for more information."
     4.5            else "";
     4.6  
     4.7 -        val errs = Par_List.map check ts;
     4.8 +        val errs = Par_List.map_name "Syntax.disambig" check ts;
     4.9          val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
    4.10          val len = length results;
    4.11  
     5.1 --- a/src/Pure/context.ML	Sat Feb 05 18:09:57 2011 +0100
     5.2 +++ b/src/Pure/context.ML	Sat Feb 05 20:38:32 2011 +0100
     5.3 @@ -141,7 +141,7 @@
     5.4  
     5.5  fun merge_data pp (data1, data2) =
     5.6    Datatab.keys (Datatab.merge (K true) (data1, data2))
     5.7 -  |> Par_List.map (fn k =>
     5.8 +  |> Par_List.map_name "Context.merge_data" (fn k =>
     5.9      (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
    5.10        (SOME x, NONE) => (k, invoke_extend k x)
    5.11      | (NONE, SOME y) => (k, invoke_extend k y)