# HG changeset patch
# User wenzelm
# Date 1363211188 -3600
# Node ID d2dfd743b58cddfdbbc1dde6aa313a9bb2591ab9
# Parent  587f493447d92cad180628721a534c106436c06b# Parent  e5f9a6d9ca82e81c22e4d89299fa2e5c9ec8c297
merged

diff -r 587f493447d9 -r d2dfd743b58c NEWS
--- a/NEWS	Wed Mar 13 17:17:33 2013 +0000
+++ b/NEWS	Wed Mar 13 22:46:28 2013 +0100
@@ -6,6 +6,13 @@
 
 *** General ***
 
+* Sessions may be organized via 'chapter' specifications in the ROOT
+file, which determines a two-level hierarchy of browser info.  The old
+tree-like organization via implicit sub-session relation, with its
+tendency towards erratic fluctuation of URLs, has been discontinued.
+The default chapter is "Unsorted".  Potential INCOMPATIBILITY for HTML
+presentation of theories.
+
 * Discontinued obsolete 'uses' within theory header.  Note that
 commands like 'ML_file' work without separate declaration of file
 dependencies.  Minor INCOMPATIBILITY.
diff -r 587f493447d9 -r d2dfd743b58c etc/options
--- a/etc/options	Wed Mar 13 17:17:33 2013 +0000
+++ b/etc/options	Wed Mar 13 22:46:28 2013 +0100
@@ -51,8 +51,10 @@
   -- "level of tracing information for multithreading"
 option parallel_proofs : int = 2
   -- "level of parallel proof checking: 0, 1, 2"
-option parallel_proofs_threshold : int = 100
-  -- "threshold for sub-proof parallelization"
+option parallel_subproofs_saturation : int = 100
+  -- "upper bound for forks of nested proofs (multiplied by worker threads)"
+option parallel_subproofs_threshold : real = 0.01
+  -- "lower bound of timing estimate for forked nested proofs (seconds)"
 option parallel_proofs_reuse_timing : bool = true
   -- "reuse timing information from old log file for parallel proof scheduling"
 
diff -r 587f493447d9 -r d2dfd743b58c lib/html/library_index_content.template
--- a/lib/html/library_index_content.template	Wed Mar 13 17:17:33 2013 +0000
+++ b/lib/html/library_index_content.template	Wed Mar 13 22:46:28 2013 +0100
@@ -8,10 +8,6 @@
         that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
         </li>
       </ul>
-      <ul>
-        <li>HOL with explicit <a href="HOL-Proofs/index.html">proof terms</a>.
-        </li>
-      </ul>
     </li>
   </ul>
 
diff -r 587f493447d9 -r d2dfd743b58c src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Doc/System/Presentation.thy	Wed Mar 13 22:46:28 2013 +0100
@@ -57,9 +57,11 @@
   theory browsing information, including HTML documents that show the
   theory sources and the relationship with its ancestors and
   descendants.  Besides the HTML file that is generated for every
-  theory, Isabelle stores links to all theories in an index
-  file. These indexes are linked with other indexes to represent the
-  overall tree structure of the sessions.
+  theory, Isabelle stores links to all theories of a session in an
+  index file.  As a second hierarchy, groups of sessions are organized
+  as \emph{chapters}, with a separate index.  Note that the implicit
+  tree structure of the session build hierarchy is \emph{not} relevant
+  for the presentation.
 
   Isabelle also generates graph files that represent the theory
   dependencies within a session.  There is a graph browser Java applet
@@ -80,7 +82,7 @@
 \end{ttbox}
 
   The presentation output will appear in @{verbatim
-  "$ISABELLE_BROWSER_INFO/FOL"} as reported by the above verbose
+  "$ISABELLE_BROWSER_INFO/FOL/FOL"} as reported by the above verbose
   invocation of the build process.
 
   Many Isabelle sessions (such as @{verbatim "HOL-Library"} in @{file
@@ -99,11 +101,9 @@
   \bigskip The theory browsing information is stored in a
   sub-directory directory determined by the @{setting_ref
   ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
-  session identifier (according to the tree structure of sub-sessions
-  by default).  In order to present Isabelle applications on the web,
-  the corresponding subdirectory from @{setting ISABELLE_BROWSER_INFO}
-  can be put on a WWW server.
-*}
+  session chapter and identifier.  In order to present Isabelle
+  applications on the web, the corresponding subdirectory from
+  @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.  *}
 
 section {* Preparing session root directories \label{sec:tool-mkroot} *}
 
@@ -311,7 +311,7 @@
   inspect {\LaTeX} runs in further detail, e.g.\ like this:
 
 \begin{ttbox}
-  cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
+  cd ~/.isabelle/IsabelleXXXX/browser_info/Unsorted/Test/document
   isabelle latex -o pdf
 \end{ttbox}
 *}
diff -r 587f493447d9 -r d2dfd743b58c src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Doc/System/Sessions.thy	Wed Mar 13 22:46:28 2013 +0100
@@ -38,15 +38,20 @@
   \emph{outer syntax} of Isabelle/Isar, see also
   \cite{isabelle-isar-ref}.  This defines common forms like
   identifiers, names, quoted strings, verbatim text, nested comments
-  etc.  The grammar for a single @{syntax session_entry} is given as
-  syntax diagram below; each ROOT file may contain multiple session
-  specifications like this.
+  etc.  The grammar for @{syntax session_chapter} and @{syntax
+  session_entry} is given as syntax diagram below; each ROOT file may
+  contain multiple specifications like this.  Chapters help to
+  organize browser info (\secref{sec:info}), but have no formal
+  meaning.  The default chapter is ``@{text "Unsorted"}''.
 
   Isabelle/jEdit (\secref{sec:tool-jedit}) includes a simple editing
   mode @{verbatim "isabelle-root"} for session ROOT files, which is
   enabled by default for any file of that name.
 
   @{rail "
+    @{syntax_def session_chapter}: @'chapter' @{syntax name}
+    ;
+
     @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
     ;
     body: description? options? ( theories + ) files?
diff -r 587f493447d9 -r d2dfd743b58c src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/HOL/ROOT	Wed Mar 13 22:46:28 2013 +0100
@@ -1,7 +1,9 @@
 chapter HOL
 
 session HOL (main) = Pure +
-  description {* Classical Higher-order Logic *}
+  description {*
+    Classical Higher-order Logic.
+  *}
   options [document_graph]
   theories Complex_Main
   files
@@ -11,7 +13,9 @@
     "document/root.tex"
 
 session "HOL-Proofs" = Pure +
-  description {* HOL-Main with explicit proof terms *}
+  description {*
+    HOL-Main with explicit proof terms.
+  *}
   options [document = false, proofs = 2]
   theories Main
   files
@@ -19,7 +23,9 @@
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
 
 session "HOL-Library" (main) in Library = HOL +
-  description {* Classical Higher-order Logic -- batteries included *}
+  description {*
+    Classical Higher-order Logic -- batteries included.
+  *}
   theories
     Library
     (*conflicting type class instantiations*)
@@ -204,7 +210,12 @@
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   options [document = false, document_graph = false, browser_info = false]
-  theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char
+  theories
+    Generate
+    Generate_Binary_Nat
+    Generate_Target_Nat
+    Generate_Efficient_Datastructures
+    Generate_Pretty_Char
 
 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   description {*
@@ -264,7 +275,9 @@
   files "document/root.bib" "document/root.tex"
 
 session "HOL-Auth" in Auth = HOL +
-  description {* A new approach to verifying authentication protocols. *}
+  description {*
+    A new approach to verifying authentication protocols.
+  *}
   options [document_graph]
   theories
     Auth_Shared
@@ -346,7 +359,9 @@
   theories Hilbert_Classical
 
 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
-  description {* Examples for program extraction in Higher-Order Logic *}
+  description {*
+    Examples for program extraction in Higher-Order Logic.
+  *}
   options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
@@ -471,7 +486,9 @@
   files "document/root.tex"
 
 session "HOL-ex" in ex = HOL +
-  description {* Miscellaneous examples for Higher-Order Logic. *}
+  description {*
+    Miscellaneous examples for Higher-Order Logic.
+  *}
   options [timeout = 3600, condition = ISABELLE_POLYML]
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
@@ -669,12 +686,16 @@
   theories [quick_and_dirty] VC_Condition
 
 session "HOL-Cardinals-Base" in Cardinals = HOL +
-  description {* Ordinals and Cardinals, Base Theories *}
+  description {*
+    Ordinals and Cardinals, Base Theories.
+  *}
   options [document = false]
   theories Cardinal_Arithmetic
 
 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
-  description {* Ordinals and Cardinals, Full Theories *}
+  description {*
+    Ordinals and Cardinals, Full Theories.
+  *}
   options [document = false]
   theories Cardinals
   files
@@ -683,17 +704,23 @@
     "document/root.bib"
 
 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" +
-  description {* Bounded Natural Functors for Datatypes *}
+  description {*
+    Bounded Natural Functors for Datatypes.
+  *}
   options [document = false]
   theories BNF_LFP
 
 session "HOL-BNF" in BNF = "HOL-Cardinals" +
-  description {* Bounded Natural Functors for (Co)datatypes *}
+  description {*
+    Bounded Natural Functors for (Co)datatypes.
+  *}
   options [document = false]
   theories BNF
 
 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" +
-  description {* Examples for Bounded Natural Functors *}
+  description {*
+    Examples for Bounded Natural Functors.
+  *}
   options [document = false]
   theories
     Lambda_Term
@@ -720,7 +747,9 @@
   files "document/root.tex"
 
 session "HOL-NSA" in NSA = HOL +
-  description {* Nonstandard analysis. *}
+  description {*
+    Nonstandard analysis.
+  *}
   options [document_graph]
   theories Hypercomplex
   files "document/root.tex"
@@ -958,7 +987,9 @@
   files "document/root.tex"
 
 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
-  description {* Misc HOLCF examples *}
+  description {*
+    Miscellaneous examples for HOLCF.
+  *}
   options [document = false]
   theories
     Dnat
@@ -1046,7 +1077,9 @@
     TrivEx2
 
 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
-  description {* Some rather large datatype examples (from John Harrison). *}
+  description {*
+    Some rather large datatype examples (from John Harrison).
+  *}
   options [document = false]
   theories [condition = ISABELLE_FULL_TEST, timing]
     Brackin
@@ -1055,7 +1088,9 @@
     Verilog
 
 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
-  description {* Some benchmark on large record. *}
+  description {*
+    Some benchmark on large record.
+  *}
   options [document = false]
   theories [condition = ISABELLE_FULL_TEST, timing]
     Record_Benchmark
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Isar/toplevel.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -91,8 +91,8 @@
   val status: transition -> Markup.T -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val approximative_id: transition -> {file: string, offset: int, name: string} option
-  val get_timing: transition -> Time.time
-  val put_timing: Time.time -> transition -> transition
+  val get_timing: transition -> Time.time option
+  val put_timing: Time.time option -> transition -> transition
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command_errors: bool -> transition -> state -> Runtime.error list * state option
   val command_exception: bool -> transition -> state -> state
@@ -346,7 +346,7 @@
   int_only: bool,            (*interactive-only*)
   print: bool,               (*print result state*)
   no_timing: bool,           (*suppress timing*)
-  timing: Time.time,         (*prescient timing information*)
+  timing: Time.time option,  (*prescient timing information*)
   trans: trans list};        (*primitive transitions (union)*)
 
 fun make_transition (name, pos, int_only, print, no_timing, timing, trans) =
@@ -356,7 +356,7 @@
 fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) =
   make_transition (f (name, pos, int_only, print, no_timing, timing, trans));
 
-val empty = make_transition ("", Position.none, false, false, false, Time.zeroTime, []);
+val empty = make_transition ("", Position.none, false, false, false, NONE, []);
 
 
 (* diagnostics *)
@@ -638,14 +638,12 @@
 local
 
 fun timing_message tr (t: Timing.timing) =
-  if Timing.is_relevant_time (#elapsed t) then
-    (case approximative_id tr of
-      SOME id =>
-        (Output.protocol_message
-          (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
-        handle Fail _ => ())
-    | NONE => ())
-  else ();
+  (case approximative_id tr of
+    SOME id =>
+      (Output.protocol_message
+        (Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) ""
+      handle Fail _ => ())
+  | NONE => ());
 
 fun app int (tr as Transition {trans, print, no_timing, ...}) =
   setmp_thread_position tr (fn state =>
@@ -727,29 +725,38 @@
 val get_result = Result.get o Proof.context_of;
 val put_result = Proof.map_context o Result.put;
 
-fun proof_future_enabled st =
+fun timing_estimate include_head elem =
+  let
+    val trs = Thy_Syntax.flat_element elem |> not include_head ? tl;
+    val timings = map get_timing trs;
+  in
+    if forall is_some timings then
+      SOME (fold (curry Time.+ o the) timings Time.zeroTime)
+    else NONE
+  end;
+
+fun priority NONE = ~1
+  | priority (SOME estimate) =
+      Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
+
+fun proof_future_enabled estimate st =
   (case try proof_of st of
     NONE => false
   | SOME state =>
       not (Proof.is_relevant state) andalso
        (if can (Proof.assert_bottom true) state
         then Goal.future_enabled ()
-        else Goal.future_enabled_nested 2));
-
-fun priority elem =
-  let
-    val estimate = Thy_Syntax.fold_element (curry Time.+ o get_timing) elem Time.zeroTime;
-  in
-    if estimate = Time.zeroTime then ~1
-    else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
-  end;
+        else
+          (case estimate of
+            NONE => Goal.future_enabled_nested 2
+          | SOME t => Goal.future_enabled_timing t)));
 
 fun atom_result tr st =
   let
     val st' =
       if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
         setmp_thread_position tr (fn () =>
-          (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
+          (Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr)))
             (fn () => command tr st); st)) ()
       else command tr st;
   in (Result (tr, st'), st') end;
@@ -757,12 +764,13 @@
 in
 
 fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
-  | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
+  | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
       let
         val (head_result, st') = atom_result head_tr st;
         val (body_elems, end_tr) = element_rest;
+        val estimate = timing_estimate false elem;
       in
-        if not (proof_future_enabled st')
+        if not (proof_future_enabled estimate st')
         then
           let
             val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
@@ -776,7 +784,7 @@
               (fn state =>
                 setmp_thread_position head_tr (fn () =>
                   Goal.fork_name "Toplevel.future_proof"
-                    (priority (Thy_Syntax.Element (empty, SOME element_rest)))
+                    (priority estimate)
                     (fn () =>
                       let
                         val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/System/isabelle_process.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -243,7 +243,8 @@
         if Multithreading.max_threads_value () < 2
         then Multithreading.max_threads := 2 else ();
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
-        Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
+        Goal.parallel_subproofs_saturation := Options.int options "parallel_subproofs_saturation";
+        Goal.parallel_subproofs_threshold := Options.real options "parallel_subproofs_threshold";
         tracing_messages := Options.int options "editor_tracing_messages"
       end);
 
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/System/session.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -94,7 +94,7 @@
 
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name doc_dump rpath level timing verbose max_threads trace_threads
-    parallel_proofs parallel_proofs_threshold =
+    parallel_proofs parallel_subproofs_saturation =
   ((fn () =>
     let
       val _ =
@@ -116,7 +116,7 @@
     |> Unsynchronized.setmp Proofterm.proofs level
     |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
-    |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
+    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation
     |> Unsynchronized.setmp Multithreading.trace trace_threads
     |> Unsynchronized.setmp Multithreading.max_threads
       (if Multithreading.available then max_threads
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/present.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -36,7 +36,6 @@
 val html_path = html_ext o Path.basic;
 val index_path = Path.basic "index.html";
 val readme_html_path = Path.basic "README.html";
-val readme_path = Path.basic "README";
 val documentN = "document";
 val document_path = Path.basic documentN;
 val doc_indexN = "session";
@@ -44,7 +43,7 @@
 val graph_pdf_path = Path.basic "session_graph.pdf";
 val graph_eps_path = Path.basic "session_graph.eps";
 
-fun show_path path = Path.implode (Path.append (File.pwd ()) path);
+fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
 
 
 
@@ -241,10 +240,7 @@
            else (); [])
         else doc_variants;
 
-      val readme =
-        if File.exists readme_html_path then SOME readme_html_path
-        else if File.exists readme_path then SOME readme_path
-        else NONE;
+      val readme = if File.exists readme_html_path then SOME readme_html_path else NONE;
 
       val docs =
         (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/present.scala	Wed Mar 13 22:46:28 2013 +0100
@@ -19,8 +19,12 @@
 
   private def read_sessions(dir: Path): List[(String, String)] =
   {
-    import XML.Decode._
-    list(pair(string, string))(YXML.parse_body(File.read(dir + sessions_path)))
+    val path = dir + sessions_path
+    if (path.is_file) {
+      import XML.Decode._
+      list(pair(string, string))(YXML.parse_body(File.read(path)))
+    }
+    else Nil
   }
 
   private def write_sessions(dir: Path, sessions: List[(String, String)])
@@ -36,7 +40,7 @@
 
     val sessions0 =
       try { read_sessions(dir) }
-      catch { case ERROR(_) => Nil case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
+      catch { case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
 
     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
 
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/thy_info.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -17,7 +17,7 @@
   val loaded_files: string -> Path.T list
   val remove_thy: string -> unit
   val kill_thy: string -> unit
-  val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} ->
+  val use_theories: {last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
     (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
@@ -174,7 +174,7 @@
 fun result_commit (Result {commit, ...}) = commit;
 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
 
-fun join_proofs (Result {theory, id, present, ...}) =
+fun join_proofs (Result {theory, id, ...}) =
   let
     val result1 = Exn.capture Thm.join_theory_proofs theory;
     val results2 = Future.join_results (Goal.peek_futures id);
@@ -351,7 +351,7 @@
 fun use_theories {last_timing, master_dir} imports =
   schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty));
 
-val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current};
+val use_thys = use_theories {last_timing = K NONE, master_dir = Path.current};
 val use_thy = use_thys o single;
 
 
@@ -361,7 +361,7 @@
   let
     val {name = (name, _), imports, ...} = header;
     val _ = kill_thy name;
-    val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports;
+    val _ = use_theories {last_timing = K NONE, master_dir = master_dir} imports;
     val _ = Thy_Header.define_keywords header;
     val parents = map (get_theory o base_name o fst) imports;
   in Thy_Load.begin_theory master_dir header parents end;
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/thy_load.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -22,7 +22,7 @@
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
-  val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header ->
+  val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header ->
     Position.T -> string -> theory list -> theory * (unit -> unit) * int
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -17,7 +17,6 @@
   val parse_spans: Token.T list -> span list
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val atom: 'a -> 'a element
-  val fold_element: ('a -> 'b -> 'b) -> 'a element -> 'b -> 'b
   val map_element: ('a -> 'b) -> 'a element -> 'b element
   val flat_element: 'a element -> 'a list
   val last_element: 'a element -> 'a
@@ -144,9 +143,6 @@
 fun element (a, b) = Element (a, SOME b);
 fun atom a = Element (a, NONE);
 
-fun fold_element f (Element (a, NONE)) = f a
-  | fold_element f (Element (a, SOME (elems, b))) = f a #> (fold o fold_element) f elems #> f b;
-
 fun map_element f (Element (a, NONE)) = Element (f a, NONE)
   | map_element f (Element (a, SOME (elems, b))) =
       Element (f a, SOME ((map o map_element) f elems, f b));
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Tools/build.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -50,8 +50,10 @@
     |> Unsynchronized.setmp print_mode
         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
-    |> Unsynchronized.setmp Goal.parallel_proofs_threshold
-        (Options.int options "parallel_proofs_threshold")
+    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
+        (Options.int options "parallel_subproofs_saturation")
+    |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
+        (Options.real options "parallel_subproofs_threshold")
     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     |> Unsynchronized.setmp Future.ML_statistics true
@@ -99,10 +101,10 @@
       (case Symtab.lookup timings file of
         SOME offsets =>
           (case Inttab.lookup offsets offset of
-            SOME (name', time) => if name = name' then time else Time.zeroTime
-          | NONE => Time.zeroTime)
-      | NONE => Time.zeroTime)
-  | NONE => Time.zeroTime);
+            SOME (name', time) => if name = name' then SOME time else NONE
+          | NONE => NONE)
+      | NONE => NONE)
+  | NONE => NONE);
 
 in
 
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/Tools/build.scala	Wed Mar 13 22:46:28 2013 +0100
@@ -474,18 +474,6 @@
     name: String, val info: Session_Info, output: Path, do_output: Boolean,
     verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
   {
-    // global browser info dir
-    if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
-    {
-      Isabelle_System.mkdirs(browser_info)
-      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
-        browser_info + Path.explode("isabelle.gif"))
-      File.write(browser_info + Path.explode("index.html"),
-        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
-        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
-        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
-    }
-
     def output_path: Option[Path] = if (do_output) Some(output) else None
 
     private val parent = info.parent.getOrElse("")
@@ -867,12 +855,36 @@
       }
       else loop(queue, Map.empty, Map.empty)
 
-    val session_entries =
-      (for { (name, res) <- results.iterator; info = full_tree(name) }
-        yield (info.chapter, (name, info.description))).toList.groupBy(_._1).map(
-          { case (chapter, es) => (chapter, es.map(_._2)) })
-    for ((chapter, entries) <- session_entries)
-      Present.update_chapter_index(browser_info, chapter, entries)
+
+    /* global browser info */
+
+    if (!no_build) {
+      val browser_chapters =
+        (for {
+          (name, result) <- results.iterator
+          if result.rc == 0
+          info = full_tree(name)
+          if info.options.bool("browser_info")
+        } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
+            map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
+
+      for ((chapter, entries) <- browser_chapters)
+        Present.update_chapter_index(browser_info, chapter, entries)
+
+      if (!browser_chapters.isEmpty && !(browser_info + Path.explode("index.html")).is_file)
+      {
+        Isabelle_System.mkdirs(browser_info)
+        File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+          browser_info + Path.explode("isabelle.gif"))
+        File.write(browser_info + Path.explode("index.html"),
+          File.read(Path.explode("~~/lib/html/library_index_header.template")) +
+          File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+          File.read(Path.explode("~~/lib/html/library_index_footer.template")))
+      }
+    }
+
+
+    /* return code */
 
     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
     if (rc != 0 && (verbose || !no_build)) {
diff -r 587f493447d9 -r d2dfd743b58c src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Pure/goal.ML	Wed Mar 13 22:46:28 2013 +0100
@@ -7,7 +7,8 @@
 signature BASIC_GOAL =
 sig
   val parallel_proofs: int Unsynchronized.ref
-  val parallel_proofs_threshold: int Unsynchronized.ref
+  val parallel_subproofs_saturation: int Unsynchronized.ref
+  val parallel_subproofs_threshold: real Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -32,6 +33,7 @@
   val future_enabled_level: int -> bool
   val future_enabled: unit -> bool
   val future_enabled_nested: int -> bool
+  val future_enabled_timing: Time.time -> bool
   val future_result: Proof.context -> thm future -> term -> thm
   val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -191,7 +193,8 @@
 (* scheduling parameters *)
 
 val parallel_proofs = Unsynchronized.ref 1;
-val parallel_proofs_threshold = Unsynchronized.ref 100;
+val parallel_subproofs_saturation = Unsynchronized.ref 100;
+val parallel_subproofs_threshold = Unsynchronized.ref 0.01;
 
 fun future_enabled_level n =
   Multithreading.enabled () andalso ! parallel_proofs >= n andalso
@@ -201,7 +204,10 @@
 
 fun future_enabled_nested n =
   future_enabled_level n andalso
-  forked_count () < ! parallel_proofs_threshold * Multithreading.max_threads_value ();
+  forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value ();
+
+fun future_enabled_timing t =
+  future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold;
 
 
 (* future_result *)
diff -r 587f493447d9 -r d2dfd743b58c src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 13 17:17:33 2013 +0000
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Wed Mar 13 22:46:28 2013 +0100
@@ -41,10 +41,10 @@
 {
   // FIXME avoid hard-wired stuff
   private val relevant_options =
-    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
-      "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
-      "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
-      "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay",
+    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit",
+      "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale",
+      "jedit_tooltip_margin", "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
+      "parallel_subproofs_saturation", "editor_load_delay", "editor_input_delay",
       "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
       "editor_update_delay", "editor_chart_delay")