wenzelm@38150: (* Title: Pure/PIDE/document.ML wenzelm@38150: Author: Makarius wenzelm@38150: wenzelm@38150: Document as collection of named nodes, each consisting of an editable wenzelm@44478: list of commands, with asynchronous read/eval/print processes. wenzelm@38150: *) wenzelm@38150: wenzelm@38150: signature DOCUMENT = wenzelm@38150: sig wenzelm@38363: type id = int wenzelm@38373: type version_id = id wenzelm@38363: type command_id = id wenzelm@38373: type exec_id = id wenzelm@38363: val no_id: id wenzelm@38419: val new_id: unit -> id wenzelm@38363: val parse_id: string -> id wenzelm@38363: val print_id: id -> string wenzelm@48707: type node_header = string * Thy_Header.header * string list wenzelm@44157: datatype node_edit = wenzelm@48755: Clear | (* FIXME unused !? *) wenzelm@44157: Edits of (command_id option * command_id option) list | wenzelm@48707: Deps of node_header | wenzelm@44385: Perspective of command_id list wenzelm@44156: type edit = string * node_edit wenzelm@38418: type state wenzelm@38418: val init_state: state wenzelm@44644: val define_command: command_id -> string -> string -> state -> state wenzelm@47420: val remove_versions: version_id list -> state -> state wenzelm@47343: val discontinue_execution: state -> unit wenzelm@47404: val cancel_execution: state -> unit wenzelm@47420: val start_execution: state -> unit wenzelm@47628: val timing: bool Unsynchronized.ref wenzelm@44481: val update: version_id -> version_id -> edit list -> state -> wenzelm@47388: (command_id * exec_id option) list * state wenzelm@43713: val state: unit -> state wenzelm@43713: val change_state: (state -> state) -> unit wenzelm@38150: end; wenzelm@38150: wenzelm@38150: structure Document: DOCUMENT = wenzelm@38150: struct wenzelm@38150: wenzelm@38150: (* unique identifiers *) wenzelm@38150: wenzelm@38363: type id = int; wenzelm@38373: type version_id = id; wenzelm@38363: type command_id = id; wenzelm@38373: type exec_id = id; wenzelm@38355: wenzelm@38355: val no_id = 0; wenzelm@40449: val new_id = Synchronized.counter (); wenzelm@38418: wenzelm@38414: val parse_id = Markup.parse_int; wenzelm@38414: val print_id = Markup.print_int; wenzelm@38150: wenzelm@38418: fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id); wenzelm@38418: fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id); wenzelm@38150: wenzelm@38418: wenzelm@38418: wenzelm@38418: (** document structure **) wenzelm@38418: wenzelm@48707: type node_header = string * Thy_Header.header * string list; wenzelm@47407: type perspective = (command_id -> bool) * command_id option; wenzelm@38448: structure Entries = Linear_Set(type key = command_id val ord = int_ord); wenzelm@38448: wenzelm@48772: type exec = ((Toplevel.state * bool) * unit lazy) Command.memo; (*eval/print process*) wenzelm@48772: val no_exec = Command.memo_value ((Toplevel.toplevel, false), Lazy.value ()); wenzelm@44674: wenzelm@43668: abstype node = Node of wenzelm@48707: {header: node_header, (*master directory, theory header, errors*) wenzelm@47407: perspective: perspective, (*visible commands, last*) wenzelm@49064: entries: (exec_id * exec) option Entries.T * bool, (*command entries with excecutions, stable*) wenzelm@47407: result: exec option} (*result of last execution*) wenzelm@43668: and version = Version of node Graph.T (*development graph wrt. static imports*) wenzelm@38418: with wenzelm@38418: wenzelm@47406: fun make_node (header, perspective, entries, result) = wenzelm@47406: Node {header = header, perspective = perspective, entries = entries, result = result}; wenzelm@43668: wenzelm@47406: fun map_node f (Node {header, perspective, entries, result}) = wenzelm@47406: make_node (f (header, perspective, entries, result)); wenzelm@38418: wenzelm@44476: fun make_perspective command_ids : perspective = wenzelm@44476: (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids); wenzelm@44441: wenzelm@48927: val no_header = ("", Thy_Header.make ("", Position.none) [] [] [], ["Bad theory header"]); wenzelm@44441: val no_perspective = make_perspective []; wenzelm@44386: wenzelm@49064: val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE); wenzelm@49064: val clear_node = wenzelm@49064: map_node (fn (header, _, _, _) => (header, no_perspective, (Entries.empty, true), NONE)); wenzelm@44386: wenzelm@44386: wenzelm@44386: (* basic components *) wenzelm@44386: wenzelm@48927: fun set_header header = wenzelm@48927: map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result)); wenzelm@48927: wenzelm@48707: fun get_header (Node {header = (master, header, errors), ...}) = wenzelm@48707: if null errors then (master, header) wenzelm@48707: else error (cat_lines errors); wenzelm@48707: wenzelm@48927: fun read_header node span = wenzelm@48927: let wenzelm@48927: val (dir, {name = (name, _), imports, keywords, uses}) = get_header node; wenzelm@48927: val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span; wenzelm@48927: in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords uses) end; wenzelm@44180: wenzelm@44385: fun get_perspective (Node {perspective, ...}) = perspective; wenzelm@44441: fun set_perspective ids = wenzelm@47406: map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result)); wenzelm@44385: wenzelm@47345: val visible_command = #1 o get_perspective; wenzelm@47345: val visible_last = #2 o get_perspective; wenzelm@47345: val visible_node = is_some o visible_last wenzelm@47345: wenzelm@44444: fun map_entries f = wenzelm@49064: map_node (fn (header, perspective, (entries, stable), result) => wenzelm@49064: (header, perspective, (f entries, stable), result)); wenzelm@49064: fun get_entries (Node {entries = (entries, _), ...}) = entries; wenzelm@49064: wenzelm@49064: fun entries_stable stable = wenzelm@49064: map_node (fn (header, perspective, (entries, _), result) => wenzelm@49064: (header, perspective, (entries, stable), result)); wenzelm@49064: fun stable_entries (Node {entries = (_, stable), ...}) = stable; wenzelm@44645: wenzelm@44645: fun iterate_entries f = Entries.iterate NONE f o get_entries; wenzelm@49064: fun iterate_entries_after start f (Node {entries = (entries, _), ...}) = wenzelm@44645: (case Entries.get_after entries start of wenzelm@44645: NONE => I wenzelm@44645: | SOME id => Entries.iterate (SOME id) f entries); wenzelm@43668: wenzelm@47339: fun get_result (Node {result, ...}) = result; wenzelm@44385: fun set_result result = wenzelm@47406: map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); wenzelm@44180: wenzelm@44185: fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; wenzelm@44202: fun default_node name = Graph.default_node (name, empty_node); wenzelm@44202: fun update_node name f = default_node name #> Graph.map_node name f; wenzelm@38418: wenzelm@38418: wenzelm@38448: (* node edits and associated executions *) wenzelm@38150: wenzelm@44157: datatype node_edit = wenzelm@44185: Clear | wenzelm@44157: Edits of (command_id option * command_id option) list | wenzelm@48707: Deps of node_header | wenzelm@44385: Perspective of command_id list; wenzelm@44157: wenzelm@44156: type edit = string * node_edit; wenzelm@38448: wenzelm@49064: val after_entry = Entries.get_after o get_entries; wenzelm@44479: wenzelm@49064: fun lookup_entry node id = wenzelm@49064: (case Entries.lookup (get_entries node) id of wenzelm@44480: NONE => NONE wenzelm@44480: | SOME (exec, _) => exec); wenzelm@44480: wenzelm@49064: fun the_entry node id = wenzelm@49064: (case Entries.lookup (get_entries node) id of wenzelm@38448: NONE => err_undef "command entry" id wenzelm@44476: | SOME (exec, _) => exec); wenzelm@38150: wenzelm@47420: fun the_default_entry node (SOME id) = (id, the_default (no_id, no_exec) (the_entry node id)) wenzelm@47341: | the_default_entry _ NONE = (no_id, (no_id, no_exec)); wenzelm@44476: wenzelm@44482: fun update_entry id exec = wenzelm@44482: map_entries (Entries.update (id, exec)); wenzelm@44482: wenzelm@44482: fun reset_entry id node = wenzelm@44482: if is_some (lookup_entry node id) then update_entry id NONE node else node; wenzelm@38418: wenzelm@38448: fun reset_after id entries = wenzelm@38448: (case Entries.get_after entries id of wenzelm@38448: NONE => entries wenzelm@38448: | SOME next => Entries.update (next, NONE) entries); wenzelm@38448: wenzelm@43668: val edit_node = map_entries o fold wenzelm@43668: (fn (id, SOME id2) => Entries.insert_after id (id2, NONE) wenzelm@43668: | (id, NONE) => Entries.delete_after id #> reset_after id); wenzelm@38418: wenzelm@38418: wenzelm@38418: (* version operations *) wenzelm@38418: wenzelm@44185: val empty_version = Version Graph.empty; wenzelm@44185: wenzelm@38418: fun nodes_of (Version nodes) = nodes; wenzelm@44185: val node_of = get_node o nodes_of; wenzelm@38418: wenzelm@44185: fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); wenzelm@44180: wenzelm@44157: fun edit_nodes (name, node_edit) (Version nodes) = wenzelm@44157: Version wenzelm@44436: (case node_edit of wenzelm@47406: Clear => update_node name clear_node nodes wenzelm@47406: | Edits edits => update_node name (edit_node edits) nodes wenzelm@48707: | Deps (master, header, errors) => wenzelm@44436: let wenzelm@48927: val imports = map fst (#imports header); wenzelm@48707: val errors1 = wenzelm@48707: (Thy_Header.define_keywords header; errors) wenzelm@48707: handle ERROR msg => errors @ [msg]; wenzelm@44436: val nodes1 = nodes wenzelm@44436: |> default_node name wenzelm@48927: |> fold default_node imports; wenzelm@44436: val nodes2 = nodes1 wenzelm@44436: |> Graph.Keys.fold wenzelm@44436: (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); wenzelm@48707: val (nodes3, errors2) = wenzelm@48927: (Graph.add_deps_acyclic (name, imports) nodes2, errors1) wenzelm@48707: handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs); wenzelm@48707: in Graph.map_node name (set_header (master, header, errors2)) nodes3 end wenzelm@47406: | Perspective perspective => update_node name (set_perspective perspective) nodes); wenzelm@44444: wenzelm@44222: fun put_node (name, node) (Version nodes) = wenzelm@44222: Version (update_node name (K node) nodes); wenzelm@38418: wenzelm@38150: end; wenzelm@38150: wenzelm@38418: wenzelm@38418: wenzelm@47389: (** main state -- document structure and execution process **) wenzelm@38418: wenzelm@38418: abstype state = State of wenzelm@40398: {versions: version Inttab.table, (*version_id -> document content*) wenzelm@47335: commands: (string * Token.T list lazy) Inttab.table, (*command_id -> named span*) wenzelm@47343: execution: version_id * Future.group * bool Unsynchronized.ref} (*current execution process*) wenzelm@38418: with wenzelm@38418: wenzelm@44674: fun make_state (versions, commands, execution) = wenzelm@44674: State {versions = versions, commands = commands, execution = execution}; wenzelm@38418: wenzelm@44674: fun map_state f (State {versions, commands, execution}) = wenzelm@44674: make_state (f (versions, commands, execution)); wenzelm@38418: wenzelm@38418: val init_state = wenzelm@47343: make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, wenzelm@47343: (no_id, Future.new_group NONE, Unsynchronized.ref false)); wenzelm@38418: wenzelm@47420: fun execution_of (State {execution, ...}) = execution; wenzelm@47420: wenzelm@38418: wenzelm@38418: (* document versions *) wenzelm@38418: wenzelm@38418: fun define_version (id: version_id) version = wenzelm@47420: map_state (fn (versions, commands, _) => wenzelm@47420: let wenzelm@47420: val versions' = Inttab.update_new (id, version) versions wenzelm@47420: handle Inttab.DUP dup => err_dup "document version" dup; wenzelm@47420: val execution' = (id, Future.new_group NONE, Unsynchronized.ref true); wenzelm@47420: in (versions', commands, execution') end); wenzelm@38418: wenzelm@38418: fun the_version (State {versions, ...}) (id: version_id) = wenzelm@38418: (case Inttab.lookup versions id of wenzelm@38418: NONE => err_undef "document version" id wenzelm@38418: | SOME version => version); wenzelm@38418: wenzelm@44673: fun delete_version (id: version_id) versions = Inttab.delete id versions wenzelm@44673: handle Inttab.UNDEF _ => err_undef "document version" id; wenzelm@44673: wenzelm@38418: wenzelm@38418: (* commands *) wenzelm@38418: wenzelm@44644: fun define_command (id: command_id) name text = wenzelm@44674: map_state (fn (versions, commands, execution) => wenzelm@38418: let wenzelm@47395: val id_string = print_id id; wenzelm@47395: val span = Lazy.lazy (fn () => wenzelm@47395: Position.setmp_thread_data (Position.id_only id_string) wenzelm@47395: (fn () => wenzelm@47395: Thy_Syntax.parse_tokens wenzelm@47395: (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ()); wenzelm@47395: val _ = wenzelm@47395: Position.setmp_thread_data (Position.id_only id_string) wenzelm@47395: (fn () => Output.status (Markup.markup_only Isabelle_Markup.accepted)) (); wenzelm@38418: val commands' = wenzelm@46945: Inttab.update_new (id, (name, span)) commands wenzelm@38418: handle Inttab.DUP dup => err_dup "command" dup; wenzelm@44674: in (versions, commands', execution) end); wenzelm@38418: wenzelm@38418: fun the_command (State {commands, ...}) (id: command_id) = wenzelm@44660: (case Inttab.lookup commands id of wenzelm@38418: NONE => err_undef "command" id wenzelm@44644: | SOME command => command); wenzelm@38418: wenzelm@47420: end; wenzelm@38418: wenzelm@47420: fun remove_versions ids state = state |> map_state (fn (versions, _, execution) => wenzelm@47420: let wenzelm@47420: val _ = member (op =) ids (#1 execution) andalso wenzelm@47420: error ("Attempt to remove execution version " ^ print_id (#1 execution)); wenzelm@47343: wenzelm@47420: val versions' = fold delete_version ids versions; wenzelm@47420: val commands' = wenzelm@47420: (versions', Inttab.empty) |-> wenzelm@47420: Inttab.fold (fn (_, version) => nodes_of version |> wenzelm@47420: Graph.fold (fn (_, (node, _)) => node |> wenzelm@47420: iterate_entries (fn ((_, id), _) => wenzelm@47420: SOME o Inttab.insert (K true) (id, the_command state id)))); wenzelm@47420: in (versions', commands', execution) end); wenzelm@38418: wenzelm@38418: wenzelm@49064: (* consolidated states *) wenzelm@49064: wenzelm@49064: fun stable_command (exec_id, exec) = wenzelm@49064: not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso wenzelm@49064: (case Exn.capture Command.memo_result exec of wenzelm@49064: Exn.Exn exn => not (Exn.is_interrupt exn) wenzelm@49064: | Exn.Res _ => true); wenzelm@49064: wenzelm@49064: fun finished_theory node = wenzelm@49064: (case Exn.capture (Command.memo_result o the) (get_result node) of wenzelm@49064: Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st wenzelm@49064: | _ => false); wenzelm@49064: wenzelm@49064: wenzelm@38888: wenzelm@47420: (** document execution **) wenzelm@47389: wenzelm@47420: val discontinue_execution = execution_of #> (fn (_, _, running) => running := false); wenzelm@47420: val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group); wenzelm@49906: val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group); wenzelm@47345: wenzelm@47420: fun start_execution state = wenzelm@47420: let wenzelm@47420: fun run node command_id exec = wenzelm@47420: let wenzelm@47420: val (_, print) = Command.memo_eval exec; wenzelm@47420: val _ = wenzelm@47420: if visible_command node command_id wenzelm@47420: then ignore (Lazy.future Future.default_params print) wenzelm@47420: else (); wenzelm@47420: in () end; wenzelm@47345: wenzelm@47420: val (version_id, group, running) = execution_of state; wenzelm@47633: wenzelm@47420: val _ = wenzelm@47633: (singleton o Future.forks) wenzelm@47633: {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true} wenzelm@47633: (fn () => wenzelm@47633: (OS.Process.sleep (seconds 0.02); wenzelm@47633: nodes_of (the_version state version_id) |> Graph.schedule wenzelm@47633: (fn deps => fn (name, node) => wenzelm@47633: if not (visible_node node) andalso finished_theory node then wenzelm@47633: Future.value () wenzelm@47633: else wenzelm@47633: (singleton o Future.forks) wenzelm@47633: {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), wenzelm@47633: deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false} wenzelm@47633: (fn () => wenzelm@47633: iterate_entries (fn ((_, id), opt_exec) => fn () => wenzelm@47633: (case opt_exec of wenzelm@47633: SOME (_, exec) => if ! running then SOME (run node id exec) else NONE wenzelm@47633: | NONE => NONE)) node ())))); wenzelm@47420: in () end; wenzelm@47345: wenzelm@47345: wenzelm@47420: wenzelm@47420: (** document update **) wenzelm@38418: wenzelm@47628: val timing = Unsynchronized.ref false; wenzelm@47628: fun timeit msg e = cond_timeit (! timing) msg e; wenzelm@47628: wenzelm@38418: local wenzelm@38418: wenzelm@47335: fun make_required nodes = wenzelm@47335: let wenzelm@47335: val all_visible = wenzelm@47345: Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] wenzelm@47345: |> Graph.all_preds nodes wenzelm@47345: |> map (rpair ()) |> Symtab.make; wenzelm@47345: wenzelm@47335: val required = wenzelm@47345: Symtab.fold (fn (a, ()) => wenzelm@47345: exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ? wenzelm@47345: Symtab.update (a, ())) all_visible Symtab.empty; wenzelm@47335: in Symtab.defined required end; wenzelm@47335: wenzelm@48927: fun init_theory deps node span = wenzelm@47335: let wenzelm@49173: (* FIXME provide files via Isabelle/Scala, not master_dir *) wenzelm@48927: val (dir, header) = read_header node span; wenzelm@47335: val master_dir = wenzelm@48735: (case try Url.explode dir of wenzelm@48735: SOME (Url.File path) => path wenzelm@47335: | _ => Path.current); wenzelm@48927: val imports = #imports header; wenzelm@47335: val parents = wenzelm@48927: imports |> map (fn (import, _) => wenzelm@47407: (case Thy_Info.lookup_theory import of wenzelm@47335: SOME thy => thy wenzelm@47335: | NONE => wenzelm@47339: Toplevel.end_theory (Position.file_only import) wenzelm@48772: (fst (fst wenzelm@47407: (Command.memo_result wenzelm@47407: (the_default no_exec wenzelm@48927: (get_result (snd (the (AList.lookup (op =) deps import)))))))))); wenzelm@48927: val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); wenzelm@47335: in Thy_Load.begin_theory master_dir header parents end; wenzelm@47335: wenzelm@47407: fun check_theory full name node = wenzelm@47407: is_some (Thy_Info.lookup_theory name) orelse wenzelm@48707: can get_header node andalso (not full orelse is_some (get_result node)); wenzelm@47335: wenzelm@44645: fun last_common state last_visible node0 node = wenzelm@44482: let wenzelm@44645: fun update_flags prev (visible, initial) = wenzelm@44645: let wenzelm@44645: val visible' = visible andalso prev <> last_visible; wenzelm@44645: val initial' = initial andalso wenzelm@44645: (case prev of wenzelm@44645: NONE => true wenzelm@44645: | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id)))); wenzelm@44645: in (visible', initial') end; wenzelm@47630: fun get_common ((prev, id), opt_exec) (same, (_, flags)) = wenzelm@47630: if same then wenzelm@47630: let wenzelm@47630: val flags' = update_flags prev flags; wenzelm@47630: val same' = wenzelm@47630: (case opt_exec of wenzelm@47630: NONE => false wenzelm@47630: | SOME (exec_id, exec) => wenzelm@47630: (case lookup_entry node0 id of wenzelm@47630: NONE => false wenzelm@49064: | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command (exec_id, exec))); wenzelm@47630: in SOME (same', (prev, flags')) end wenzelm@47630: else NONE; wenzelm@47630: val (same, (common, flags)) = wenzelm@47630: iterate_entries get_common node (true, (NONE, (true, true))); wenzelm@44645: in wenzelm@47630: if same then wenzelm@44645: let val last = Entries.get_after (get_entries node) common wenzelm@44645: in (last, update_flags last flags) end wenzelm@47630: else (common, flags) wenzelm@44645: end; wenzelm@44645: wenzelm@48927: fun illegal_init _ = error "Illegal theory header after end of theory"; wenzelm@44482: wenzelm@47407: fun new_exec state proper_init command_id' (execs, command_exec, init) = wenzelm@47407: if not proper_init andalso is_none init then NONE wenzelm@44645: else wenzelm@44645: let wenzelm@46945: val (name, span) = the_command state command_id' ||> Lazy.force; wenzelm@44645: val (modify_init, init') = wenzelm@44645: if Keyword.is_theory_begin name then wenzelm@48927: (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE) wenzelm@44645: else (I, init); wenzelm@44660: val exec_id' = new_id (); wenzelm@46876: val exec_id'_string = print_id exec_id'; wenzelm@48918: val cmd = wenzelm@46876: Position.setmp_thread_data (Position.id_only exec_id'_string) wenzelm@46876: (fn () => wenzelm@48918: let wenzelm@48918: val tr = wenzelm@48918: #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span) wenzelm@48918: |> modify_init wenzelm@48918: |> Toplevel.put_id exec_id'_string; wenzelm@48918: val cmts = Outer_Syntax.span_cmts span; wenzelm@48918: in (tr, cmts) end); wenzelm@47406: val exec' = wenzelm@47406: Command.memo (fn () => wenzelm@48918: Command.run_command (cmd ()) (fst (Command.memo_result (snd (snd command_exec))))); wenzelm@44674: val command_exec' = (command_id', (exec_id', exec')); wenzelm@44674: in SOME (command_exec' :: execs, command_exec', init') end; wenzelm@44482: wenzelm@38418: in wenzelm@38418: wenzelm@44481: fun update (old_id: version_id) (new_id: version_id) edits state = wenzelm@38418: let wenzelm@38418: val old_version = the_version state old_id; wenzelm@44180: val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) wenzelm@47628: val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); wenzelm@38418: wenzelm@44544: val nodes = nodes_of new_version; wenzelm@44544: val is_required = make_required nodes; wenzelm@44544: wenzelm@47628: val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state); wenzelm@47628: val updated = timeit "Document.update" (fn () => wenzelm@44544: nodes |> Graph.schedule wenzelm@44199: (fn deps => fn (name, node) => wenzelm@47406: (singleton o Future.forks) wenzelm@47406: {name = "Document.update", group = NONE, wenzelm@47406: deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} wenzelm@47406: (fn () => wenzelm@47406: let wenzelm@47406: val imports = map (apsnd Future.join) deps; wenzelm@47406: val updated_imports = exists (is_some o #3 o #1 o #2) imports; wenzelm@47406: val required = is_required name; wenzelm@47406: in wenzelm@47406: if updated_imports orelse AList.defined (op =) edits name orelse wenzelm@49064: not (stable_entries node) orelse not (finished_theory node) wenzelm@47406: then wenzelm@44482: let wenzelm@47406: val node0 = node_of old_version name; wenzelm@48927: val init = init_theory imports node; wenzelm@47407: val proper_init = wenzelm@47407: check_theory false name node andalso wenzelm@47407: forall (fn (name, (_, node)) => check_theory true name node) imports; wenzelm@47406: wenzelm@47345: val last_visible = visible_last node; wenzelm@47406: val (common, (visible, initial)) = wenzelm@47406: if updated_imports then (NONE, (true, true)) wenzelm@47406: else last_common state last_visible node0 node; wenzelm@44674: val common_command_exec = the_default_entry node common; wenzelm@44479: wenzelm@47405: val (new_execs, (command_id', (_, exec')), _) = wenzelm@44674: ([], common_command_exec, if initial then SOME init else NONE) |> wenzelm@44544: (visible orelse required) ? wenzelm@44645: iterate_entries_after common wenzelm@44482: (fn ((prev, id), _) => fn res => wenzelm@44544: if not required andalso prev = last_visible then NONE wenzelm@47407: else new_exec state proper_init id res) node; wenzelm@44479: wenzelm@44482: val no_execs = wenzelm@44645: iterate_entries_after common wenzelm@44482: (fn ((_, id0), exec0) => fn res => wenzelm@44482: if is_none exec0 then NONE wenzelm@47405: else if exists (fn (_, (id, _)) => id0 = id) new_execs then SOME res wenzelm@44482: else SOME (id0 :: res)) node0 []; wenzelm@44480: wenzelm@47405: val last_exec = if command_id' = no_id then NONE else SOME command_id'; wenzelm@44482: val result = wenzelm@47407: if is_some (after_entry node last_exec) then NONE wenzelm@47407: else SOME exec'; wenzelm@44480: wenzelm@44482: val node' = node wenzelm@44482: |> fold reset_entry no_execs wenzelm@47405: |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs wenzelm@49064: |> entries_stable (null new_execs) wenzelm@47406: |> set_result result; wenzelm@47406: val updated_node = wenzelm@47406: if null no_execs andalso null new_execs then NONE wenzelm@47406: else SOME (name, node'); wenzelm@47406: in ((no_execs, new_execs, updated_node), node') end wenzelm@47406: else (([], [], NONE), node) wenzelm@47406: end)) wenzelm@47628: |> Future.joins |> map #1); wenzelm@44476: wenzelm@44479: val command_execs = wenzelm@44479: map (rpair NONE) (maps #1 updated) @ wenzelm@44674: map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated); wenzelm@47406: val updated_nodes = map_filter #3 updated; wenzelm@38418: wenzelm@44197: val state' = state wenzelm@44476: |> define_version new_id (fold put_node updated_nodes new_version); wenzelm@47388: in (command_execs, state') end; wenzelm@38418: wenzelm@38418: end; wenzelm@38418: wenzelm@38418: wenzelm@43713: wenzelm@43713: (** global state **) wenzelm@43713: wenzelm@43713: val global_state = Synchronized.var "Document" init_state; wenzelm@43713: wenzelm@43713: fun state () = Synchronized.value global_state; wenzelm@43713: val change_state = Synchronized.change global_state; wenzelm@43713: wenzelm@38418: end; wenzelm@38418: