parallel Syntax.parse, which is rather slow;
authorwenzelm
Mon Jun 27 15:01:08 2011 +0200 (2011-06-27)
changeset 4355894a08fb3ae4a
parent 43557 844b4a178dff
child 43559 c1966f322105
parallel Syntax.parse, which is rather slow;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Jun 27 14:38:58 2011 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Jun 27 15:01:08 2011 +0200
     1.3 @@ -369,8 +369,8 @@
     1.4  fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
     1.5  fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
     1.6  
     1.7 -fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt;
     1.8 -fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt;
     1.9 +fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt;
    1.10 +fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt;
    1.11  
    1.12  val read_term = singleton o read_terms;
    1.13  val read_prop = singleton o read_props;