# HG changeset patch
# User wenzelm
# Date 1279809801 -7200
# Node ID f18c4bc8b02869584fe677d60a4adeee805a5bbb
# Parent  4195727a1f6c3038c934fbac150c000d911ca6ae
load_thy: parallel parsing of units, which consist of statement/proof each;

diff -r 4195727a1f6c -r f18c4bc8b028 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Jul 22 14:59:27 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jul 22 16:43:21 2010 +0200
@@ -279,7 +279,7 @@
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
     val _ = List.app Thy_Syntax.report_span spans;
     val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
-      |> maps (prepare_unit commands);
+      |> Par_List.map (prepare_unit commands) |> flat;
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);