# HG changeset patch # User wenzelm # Date 1274987693 -7200 # Node ID d515609c88f794d06ba1b1ee52f968f87a7c311f # Parent 0c0ef115c7aaf37cffdc8b5a4ad0b70f0f94cb49 substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up; tuned; diff -r 0c0ef115c7aa -r d515609c88f7 src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Thu May 27 20:15:36 2010 +0200 +++ b/src/Pure/Isar/isar_document.ML Thu May 27 21:14:53 2010 +0200 @@ -111,12 +111,10 @@ (* states *) -val empty_state = Future.value (SOME Toplevel.toplevel); +val empty_state = Lazy.value (SOME Toplevel.toplevel); local - -val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]); - + val global_states = Unsynchronized.ref (Symtab.make [(no_id, empty_state)]); in fun define_state (id: state_id) = @@ -139,9 +137,7 @@ (* commands *) local - -val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]); - + val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]); in fun define_command id tr = @@ -160,9 +156,7 @@ (* documents *) local - -val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table); - + val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table); in fun define_document (id: document_id) document = @@ -178,6 +172,18 @@ end; +(* execution *) + +local + val execution = Unsynchronized.ref (Future.value ()); +in + +fun execute e = + NAMED_CRITICAL "Isar" (fn () => (Future.cancel (! execution); execution := Future.fork e)); + +end; + + (** main operations **) @@ -198,9 +204,9 @@ val end_state = the_state (the (#state (#3 (the (first_entry (fn (_, {next, ...}) => is_none next) document))))); - val _ = - Future.fork_deps [end_state] (fn () => - (case Future.join end_state of + val _ = (* FIXME regular execution (??) *) + Future.fork (fn () => + (case Lazy.force end_state of SOME st => (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st; ThyInfo.touch_child_thys name; @@ -227,11 +233,11 @@ let val state = the_state state_id; val state' = - Future.fork_deps [state] (fn () => - (case Future.join state of + Lazy.lazy (fn () => + (case Lazy.force state of NONE => NONE | SOME st => Toplevel.run_command name tr st)); - in put_state state_id' state' end; + in put_state state_id' state'; state' end; in (state_id', ((id, state_id'), make_state') :: updates) end; fun report_updates updates = @@ -248,19 +254,11 @@ val new_document as Document {entries = new_entries, ...} = old_document |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits; - fun cancel_old id = fold_entries id - (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ()) - old_document (); - val (updates, new_document') = (case first_entry (is_changed old_entries) new_document of - NONE => - (case first_entry (is_changed new_entries) old_document of - NONE => ([], new_document) - | SOME (_, id, _) => (cancel_old id; ([], new_document))) + NONE => ([], new_document) | SOME (prev, id, _) => let - val _ = cancel_old id; val prev_state_id = the (#state (the_entry new_entries (the prev))); val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []); val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates); @@ -268,7 +266,8 @@ val _ = define_document new_id new_document'; val _ = report_updates (map #1 updates); - val _ = List.app (fn (_, run) => run ()) updates; + val execs = map (fn (_, make) => make ()) updates; + val _ = execute (fn () => List.app (ignore o Lazy.force) execs); in () end); end;