# HG changeset patch # User wenzelm # Date 1231599634 -3600 # Node ID 018d5c88c7a8d3bbad4241e37a258bd5f17bec45 # Parent 0a1d32bc5ee5303db98a99babafeedf37d39fde8# Parent a6c641f08af7add3e4d1a98d410d1d4a3820fa2e merged diff -r 0a1d32bc5ee5 -r 018d5c88c7a8 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sat Jan 10 15:55:19 2009 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Sat Jan 10 16:00:34 2009 +0100 @@ -32,7 +32,7 @@ type isar val isar: bool -> isar val prepare_command: Position.T -> string -> Toplevel.transition - val load_thy: string -> Position.T -> string list -> bool -> unit + val load_thy: string -> Position.T -> string list -> bool -> unit -> unit end; structure OuterSyntax: OUTER_SYNTAX = @@ -288,16 +288,13 @@ (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans); val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); - val _ = cond_timeit time "" (fn () => - let - val (results, commit_exit) = Toplevel.excursion units; - val _ = - ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup results toks - |> Buffer.content - |> Present.theory_output name - val _ = commit_exit (); - in () end); + val results = cond_timeit time "" (fn () => Toplevel.excursion units); val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); - in () end; + + fun after_load () = + ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup (Lazy.force results) toks + |> Buffer.content + |> Present.theory_output name; + in after_load end; end; diff -r 0a1d32bc5ee5 -r 018d5c88c7a8 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Jan 10 15:55:19 2009 +0100 +++ b/src/Pure/Isar/toplevel.ML Sat Jan 10 16:00:34 2009 +0100 @@ -96,7 +96,7 @@ val transition: bool -> transition -> state -> (state * (exn * string) option) option val commit_exit: Position.T -> transition val command: transition -> state -> state - val excursion: (transition * transition list) list -> (transition * state) list * (unit -> unit) + val excursion: (transition * transition list) list -> (transition * state) list lazy end; structure Toplevel: TOPLEVEL = @@ -746,12 +746,12 @@ val end_pos = if null input then error "No input" else pos_of (fst (List.last input)); val immediate = not (Future.enabled ()); - val (future_results, end_state) = fold_map (proof_result immediate) input toplevel; + val (results, end_state) = fold_map (proof_result immediate) input toplevel; val _ = (case end_state of - State (NONE, SOME (Theory (Context.Theory _, _), _)) => () + State (NONE, SOME (Theory (Context.Theory _, _), _)) => + command (commit_exit end_pos) end_state | _ => error "Unfinished development at end of input"); - val results = maps Lazy.force future_results; - in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end; + in Lazy.lazy (fn () => maps Lazy.force results) end; end; diff -r 0a1d32bc5ee5 -r 018d5c88c7a8 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Jan 10 15:55:19 2009 +0100 +++ b/src/Pure/Thy/thy_info.ML Sat Jan 10 16:00:34 2009 +0100 @@ -243,14 +243,6 @@ val kill_thy = if_known_thy remove_thy; -fun consolidate_thy name = - (case lookup_theory name of - NONE => [] - | SOME thy => - (case PureThy.join_proofs thy of - [] => [] - | exns => (kill_thy name; exns))); - (* load_file *) @@ -320,33 +312,29 @@ val _ = CRITICAL (fn () => change_deps name (Option.map (fn {master, text, parents, files, ...} => make_deps upd_time master text parents files))); - val _ = OuterSyntax.load_thy name pos text (time orelse ! Output.timing); - in - CRITICAL (fn () => - (change_deps name - (Option.map (fn {update_time, master, parents, files, ...} => - make_deps update_time master [] parents files)); - perform Update name)) - end; + val after_load = OuterSyntax.load_thy name pos text (time orelse ! Output.timing); + val _ = + CRITICAL (fn () => + (change_deps name + (Option.map (fn {update_time, master, parents, files, ...} => + make_deps update_time master [] parents files)); + perform Update name)); + in after_load end; (* scheduling loader tasks *) -datatype task = Task of (unit -> unit) | Finished | Running; +datatype task = Task of (unit -> unit -> unit) | Finished | Running; fun task_finished Finished = true | task_finished _ = false; local -fun schedule_seq tasks = - Graph.topological_order tasks - |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ())); - fun schedule_futures task_graph = let val tasks = Graph.topological_order task_graph |> map_filter (fn name => (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE)); - fun future (name, body) tab = + fun fork (name, body) tab = let val deps = Graph.imm_preds task_graph name |> map_filter (fn parent => @@ -358,12 +346,23 @@ [] => body () | bad => error (loader_msg ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") []))); + in Symtab.update (name, x) tab end; - in (x, Symtab.update (name, x) tab) end; + val futures = fold fork tasks Symtab.empty; - val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty)); - val proof_results = map Exn.Exn (maps (consolidate_thy o #1) tasks); - in ignore (Exn.release_all (thy_results @ proof_results)) end; + val exns = tasks |> maps (fn (name, _) => + let + val after_load = Future.join (the (Symtab.lookup futures name)); + val _ = after_load (); + val proof_exns = PureThy.join_proofs (get_theory name); + val _ = null proof_exns orelse raise Exn.EXCEPTIONS proof_exns; + in [] end handle exn => (kill_thy name; [exn])); + + in ignore (Exn.release_all (map Exn.Exn exns)) end; + +fun schedule_seq tasks = + Graph.topological_order tasks + |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () () | _ => ())); in