discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
authorwenzelm
Sun Aug 21 14:16:44 2011 +0200 (2011-08-21)
changeset 4435302f286491568
parent 44352 176e0fb6906b
child 44354 88bf93c2ae7c
child 44359 00af710d857e
child 44363 53f4f8287606
discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Sun Aug 21 13:42:55 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Aug 21 14:16:44 2011 +0200
     1.3 @@ -175,9 +175,7 @@
     1.4      val spans = Source.exhaust (Thy_Syntax.span_source toks);
     1.5      val elements =
     1.6        Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
     1.7 -      |> Par_List.map_name "Outer_Syntax.prepare_element"
     1.8 -        (Outer_Syntax.prepare_element outer_syntax init)
     1.9 -      |> flat;
    1.10 +      |> maps (Outer_Syntax.prepare_element outer_syntax init);
    1.11  
    1.12      val _ = Present.theory_source name
    1.13        (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);