# HG changeset patch
# User wenzelm
# Date 1331985983 -3600
# Node ID 88b0a8052c753c149e94a2d09589de1f5ddbab18
# Parent  9f492f5b0cec864e9542912c38506144223c5276
added Syntax.read_typs;
tuned parallelism for syntax operations;

diff -r 9f492f5b0cec -r 88b0a8052c75 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 17 12:52:40 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 17 13:06:23 2012 +0100
@@ -119,7 +119,8 @@
 
     val Asss =
       (map o map) snd raw_specss
-      |> (burrow o burrow) (Par_List.map_name "Specification.parse_prop" (parse_prop params_ctxt));
+      |> (burrow o burrow)
+        (grouped 10 (Par_List.map_name "Specification.parse_prop") (parse_prop params_ctxt));
     val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
       |> fold Name.declare xs;
     val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
diff -r 9f492f5b0cec -r 88b0a8052c75 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Mar 17 12:52:40 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Mar 17 13:06:23 2012 +0100
@@ -43,6 +43,7 @@
   val read_typ: Proof.context -> string -> typ
   val read_term: Proof.context -> string -> term
   val read_prop: Proof.context -> string -> term
+  val read_typs: Proof.context -> string list -> typ list
   val read_terms: Proof.context -> string list -> term list
   val read_props: Proof.context -> string list -> term list
   val read_sort_global: theory -> string -> sort
@@ -265,11 +266,17 @@
 (* read = parse + check *)
 
 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
-fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
+
+fun read_typs ctxt =
+  grouped 10 (Par_List.map_name "Syntax.read_typs") (parse_typ ctxt) #> check_typs ctxt;
 
-fun read_terms ctxt = Par_List.map_name "Syntax.read_terms" (parse_term ctxt) #> check_terms ctxt;
-fun read_props ctxt = Par_List.map_name "Syntax.read_props" (parse_prop ctxt) #> check_props ctxt;
+fun read_terms ctxt =
+  grouped 10 (Par_List.map_name "Syntax.read_terms") (parse_term ctxt) #> check_terms ctxt;
 
+fun read_props ctxt =
+  grouped 10 (Par_List.map_name "Syntax.read_props") (parse_prop ctxt) #> check_props ctxt;
+
+val read_typ = singleton o read_typs;
 val read_term = singleton o read_terms;
 val read_prop = singleton o read_props;
 
diff -r 9f492f5b0cec -r 88b0a8052c75 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Mar 17 12:52:40 2012 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Mar 17 13:06:23 2012 +0100
@@ -360,7 +360,7 @@
 
           val results' =
             if parsed_len > 1 then
-              (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
+              (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
                 check results
             else results;
           val reports' = fst (hd results');