# HG changeset patch # User wenzelm # Date 1301172329 -3600 # Node ID c17508a61f49061a63091dc620c00e4433c8f74c # Parent eb84d28961a99ce84066c40a97a55a2755720a41 present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization; diff -r eb84d28961a9 -r c17508a61f49 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sat Mar 26 21:28:04 2011 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Sat Mar 26 21:45:29 2011 +0100 @@ -31,7 +31,7 @@ type isar val isar: TextIO.instream -> bool -> isar val prepare_command: Position.T -> string -> Toplevel.transition - val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> (unit -> unit) * theory + val load_thy: string -> (Path.T option -> theory) -> Position.T -> string -> theory * unit future end; structure Outer_Syntax: OUTER_SYNTAX = @@ -288,11 +288,16 @@ val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms); val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); - fun after_load () = - Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks - |> Buffer.content - |> Present.theory_output name; - in (after_load, thy) end; + val present = + singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE, + deps = map Future.task_of results, pri = 0}) + (fn () => + Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup + (maps Future.join results) toks + |> Buffer.content + |> Present.theory_output name); + + in (thy, present) end; end; diff -r eb84d28961a9 -r c17508a61f49 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Mar 26 21:28:04 2011 +0100 +++ b/src/Pure/Isar/toplevel.ML Sat Mar 26 21:45:29 2011 +0100 @@ -89,7 +89,8 @@ val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> (state * (exn * string) option) option val command: transition -> state -> state - val excursion: (transition * transition list) list -> (transition * state) list lazy * theory + val excursion: + (transition * transition list) list -> (transition * state) list future list * theory end; structure Toplevel: TOPLEVEL = @@ -655,7 +656,7 @@ Proof.is_relevant (proof_of st') then let val (states, st'') = fold_map command_result proof_trs st' - in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end + in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end else let val (body_trs, end_tr) = split_last proof_trs; @@ -679,8 +680,8 @@ (case States.get (presentation_context_of st'') of NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr)) | SOME states => states); - val result = Lazy.lazy - (fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]); + val result = states + |> Future.map (fn sts => (tr, st') :: (body_trs ~~ sts) @ [(end_tr, st'')]); in (result, st'') end end; @@ -691,6 +692,6 @@ val immediate = not (Goal.future_enabled ()); val (results, end_state) = fold_map (proof_result immediate) input toplevel; val thy = end_theory end_pos end_state; - in (Lazy.lazy (fn () => maps Lazy.force results), thy) end; + in (results, thy) end; end; diff -r eb84d28961a9 -r c17508a61f49 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Mar 26 21:28:04 2011 +0100 +++ b/src/Pure/Thy/thy_info.ML Sat Mar 26 21:45:29 2011 +0100 @@ -155,7 +155,7 @@ (* scheduling loader tasks *) datatype task = - Task of string list * (theory list -> (theory * (unit -> unit))) | + Task of string list * (theory list -> (theory * unit future * (unit -> unit))) | Finished of theory; fun task_finished (Task _) = false @@ -168,8 +168,9 @@ (case Graph.get_node task_graph name of Task (parents, body) => let - val (thy, after_load) = body (map (the o Symtab.lookup tab) parents); - val _ = after_load (); + val (thy, present, commit) = body (map (the o Symtab.lookup tab) parents); + val _ = Future.join present; + val _ = commit (); in Symtab.update (name, thy) tab end | Finished thy => Symtab.update (name, thy) tab))) |> ignore; @@ -194,13 +195,14 @@ | bad => error (loader_msg ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") []))); in Symtab.update (name, future) tab end - | Finished thy => Symtab.update (name, Future.value (thy, I)) tab)); + | Finished thy => Symtab.update (name, Future.value (thy, Future.value (), I)) tab)); val _ = tasks |> maps (fn name => let - val (thy, after_load) = Future.join (the (Symtab.lookup futures name)); + val (thy, present, commit) = Future.join (the (Symtab.lookup futures name)); val _ = Global_Theory.join_proofs thy; - val _ = after_load (); + val _ = Future.join present; + val _ = commit (); in [] end handle exn => [Exn.Exn exn]) |> rev |> Exn.release_all; in () end) (); @@ -237,17 +239,15 @@ Thy_Load.begin_theory dir name imports parent_thys uses |> Present.begin_theory update_time dir uses; - val (after_load, theory) = Outer_Syntax.load_thy name init pos text; + val (theory, present) = Outer_Syntax.load_thy name init pos text; val parents = map Context.theory_name parent_thys; - fun after_load' () = - (after_load (); + fun commit () = NAMED_CRITICAL "Thy_Info" (fn () => (map get_theory parents; change_thys (new_entry name parents (SOME deps, SOME theory)); - perform Update name))); - - in (theory, after_load') end; + perform Update name)); + in (theory, present, commit) end; fun check_deps dir name = (case lookup_deps name of @@ -255,7 +255,7 @@ | NONE => let val {master, text, imports, ...} = Thy_Load.check_thy dir name in (false, SOME (make_deps master imports, text), imports) end - | SOME (SOME {master, imports}) => + | SOME (SOME {master, ...}) => let val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name; val deps' = SOME (make_deps master' imports', text');