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@46938: type node_header = (string * Thy_Header.header) Exn.result wenzelm@44157: datatype node_edit = wenzelm@44185: Clear | wenzelm@44157: Edits of (command_id option * command_id option) list | wenzelm@44384: Header 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@44301: val cancel_execution: state -> Future.task list wenzelm@44436: val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state wenzelm@44481: val update: version_id -> version_id -> edit list -> state -> wenzelm@44479: ((command_id * exec_id option) list * (string * command_id option) list) * state wenzelm@38418: val execute: version_id -> state -> state wenzelm@44673: val remove_versions: version_id list -> state -> 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@46938: type node_header = (string * Thy_Header.header) Exn.result; wenzelm@44476: type perspective = (command_id -> bool) * command_id option; (*visible commands, last*) wenzelm@38448: structure Entries = Linear_Set(type key = command_id val ord = int_ord); wenzelm@38448: wenzelm@44674: type exec = exec_id * (Toplevel.state * unit lazy) lazy; (*eval/print process*) wenzelm@44674: val no_print = Lazy.value (); wenzelm@44674: val no_exec = (no_id, Lazy.value (Toplevel.toplevel, no_print)); wenzelm@44674: wenzelm@43668: abstype node = Node of wenzelm@44444: {touched: bool, wenzelm@44444: header: node_header, wenzelm@44386: perspective: perspective, wenzelm@44674: entries: exec option Entries.T, (*command entries with excecutions*) wenzelm@44476: last_exec: command_id option, (*last command with exec state assignment*) wenzelm@44197: result: Toplevel.state lazy} wenzelm@43668: and version = Version of node Graph.T (*development graph wrt. static imports*) wenzelm@38418: with wenzelm@38418: wenzelm@44476: fun make_node (touched, header, perspective, entries, last_exec, result) = wenzelm@44444: Node {touched = touched, header = header, perspective = perspective, wenzelm@44476: entries = entries, last_exec = last_exec, result = result}; wenzelm@43668: wenzelm@44476: fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) = wenzelm@44476: make_node (f (touched, header, perspective, entries, last_exec, 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@44476: val no_header = Exn.Exn (ERROR "Bad theory header"); wenzelm@44441: val no_perspective = make_perspective []; wenzelm@44386: val no_result = Lazy.value Toplevel.toplevel; wenzelm@44386: wenzelm@44476: val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result); wenzelm@44476: val clear_node = map_node (fn (_, header, _, _, _, _) => wenzelm@44476: (false, header, no_perspective, Entries.empty, NONE, no_result)); wenzelm@44386: wenzelm@44386: wenzelm@44386: (* basic components *) wenzelm@44386: wenzelm@44446: fun is_touched (Node {touched, ...}) = touched; wenzelm@44444: fun set_touched touched = wenzelm@44476: map_node (fn (_, header, perspective, entries, last_exec, result) => wenzelm@44476: (touched, header, perspective, entries, last_exec, result)); wenzelm@44444: wenzelm@44180: fun get_header (Node {header, ...}) = header; wenzelm@44385: fun set_header header = wenzelm@44476: map_node (fn (touched, _, perspective, entries, last_exec, result) => wenzelm@44476: (touched, header, perspective, entries, last_exec, result)); wenzelm@44180: wenzelm@44385: fun get_perspective (Node {perspective, ...}) = perspective; wenzelm@44441: fun set_perspective ids = wenzelm@44476: map_node (fn (touched, header, _, entries, last_exec, result) => wenzelm@44476: (touched, header, make_perspective ids, entries, last_exec, result)); wenzelm@44385: wenzelm@44444: fun map_entries f = wenzelm@44476: map_node (fn (touched, header, perspective, entries, last_exec, result) => wenzelm@44476: (touched, header, perspective, f entries, last_exec, result)); wenzelm@44643: fun get_entries (Node {entries, ...}) = entries; wenzelm@44645: wenzelm@44645: fun iterate_entries f = Entries.iterate NONE f o get_entries; wenzelm@44645: fun iterate_entries_after start f (Node {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@44476: fun get_last_exec (Node {last_exec, ...}) = last_exec; wenzelm@44476: fun set_last_exec last_exec = wenzelm@44476: map_node (fn (touched, header, perspective, entries, _, result) => wenzelm@44476: (touched, header, perspective, entries, last_exec, result)); wenzelm@44476: wenzelm@44386: fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result); wenzelm@44385: fun set_result result = wenzelm@44476: map_node (fn (touched, header, perspective, entries, last_exec, _) => wenzelm@44476: (touched, header, perspective, entries, last_exec, 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@44384: Header of node_header | wenzelm@44385: Perspective of command_id list; wenzelm@44157: wenzelm@44156: type edit = string * node_edit; wenzelm@38448: wenzelm@44482: fun after_entry (Node {entries, ...}) = Entries.get_after entries; wenzelm@44479: wenzelm@44480: fun lookup_entry (Node {entries, ...}) id = wenzelm@44480: (case Entries.lookup entries id of wenzelm@44480: NONE => NONE wenzelm@44480: | SOME (exec, _) => exec); wenzelm@44480: wenzelm@43668: fun the_entry (Node {entries, ...}) id = wenzelm@38448: (case Entries.lookup entries id of wenzelm@38448: NONE => err_undef "command entry" id wenzelm@44476: | SOME (exec, _) => exec); wenzelm@38150: wenzelm@44674: fun the_default_entry node (SOME id) = (id, (the_default no_exec (the_entry node id))) wenzelm@44674: | the_default_entry _ NONE = (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@44444: local wenzelm@44444: wenzelm@44185: fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); wenzelm@44180: wenzelm@44444: fun touch_node name nodes = wenzelm@44444: fold (fn desc => wenzelm@44643: update_node desc wenzelm@44643: (set_touched true #> wenzelm@44643: desc <> name ? (map_entries (reset_after NONE) #> set_result no_result))) wenzelm@44202: (Graph.all_succs nodes [name]) nodes; wenzelm@44202: wenzelm@44444: in wenzelm@44444: wenzelm@44157: fun edit_nodes (name, node_edit) (Version nodes) = wenzelm@44157: Version wenzelm@44436: (case node_edit of wenzelm@44436: Clear => wenzelm@44436: nodes wenzelm@44436: |> update_node name clear_node wenzelm@44444: |> touch_node name wenzelm@44436: | Edits edits => wenzelm@44436: nodes wenzelm@44436: |> update_node name (edit_node edits) wenzelm@44444: |> touch_node name wenzelm@44436: | Header header => wenzelm@44436: let wenzelm@46938: val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []); wenzelm@46945: val header' = wenzelm@46958: ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header) wenzelm@46945: handle exn as ERROR _ => Exn.Exn exn; wenzelm@44436: val nodes1 = nodes wenzelm@44436: |> default_node name wenzelm@46739: |> 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@46945: val (header'', nodes3) = wenzelm@46945: (header', Graph.add_deps_acyclic (name, imports) nodes2) wenzelm@44436: handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); wenzelm@46945: in Graph.map_node name (set_header header'') nodes3 end wenzelm@44444: |> touch_node name wenzelm@44436: | Perspective perspective => wenzelm@44544: update_node name (set_perspective perspective) nodes); wenzelm@38418: wenzelm@44444: end; 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@38418: (** global 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@44673: execution: version_id * Future.group} (*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@44675: make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE)); wenzelm@38418: wenzelm@38418: wenzelm@38418: (* document versions *) wenzelm@38418: wenzelm@38418: fun define_version (id: version_id) version = wenzelm@44674: map_state (fn (versions, commands, execution) => wenzelm@38418: let val versions' = Inttab.update_new (id, version) versions wenzelm@38418: handle Inttab.DUP dup => err_dup "document version" dup wenzelm@44674: 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@46910: fun parse_command id text = wenzelm@46876: Position.setmp_thread_data (Position.id_only id) wenzelm@46910: (fn () => wenzelm@46910: let wenzelm@46910: val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text; wenzelm@46910: val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed); wenzelm@46910: in toks end) (); wenzelm@46876: wenzelm@44644: fun define_command (id: command_id) name text = wenzelm@44674: map_state (fn (versions, commands, execution) => wenzelm@38418: let wenzelm@46945: val span = Lazy.lazy (fn () => parse_command (print_id id) text); 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@38418: wenzelm@41634: (* document execution *) wenzelm@41634: wenzelm@44673: fun cancel_execution (State {execution, ...}) = Future.cancel_group (#2 execution); wenzelm@41634: wenzelm@38418: end; wenzelm@38418: wenzelm@38418: wenzelm@38888: (* toplevel transactions *) wenzelm@38888: wenzelm@38888: local wenzelm@38888: wenzelm@47335: fun run int tr st = wenzelm@47335: (case Toplevel.transition int tr st of wenzelm@47335: SOME (st', NONE) => ([], SOME st') wenzelm@47335: | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) wenzelm@47335: | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); wenzelm@47335: wenzelm@44440: fun timing tr t = wenzelm@45674: if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else (); wenzelm@40391: wenzelm@38888: fun proof_status tr st = wenzelm@38888: (case try Toplevel.proof_of st of wenzelm@38888: SOME prf => Toplevel.status tr (Proof.status_markup prf) wenzelm@38888: | NONE => ()); wenzelm@38888: wenzelm@44386: fun print_state tr st = wenzelm@44386: (Lazy.lazy o Toplevel.setmp_thread_position tr) wenzelm@44386: (fn () => Toplevel.print_state false st); wenzelm@38888: wenzelm@38888: in wenzelm@38888: wenzelm@44199: fun run_command tr st = wenzelm@44185: let wenzelm@44199: val is_init = Toplevel.is_init tr; wenzelm@44185: val is_proof = Keyword.is_proof (Toplevel.name_of tr); wenzelm@44185: wenzelm@44614: val _ = Multithreading.interrupted (); wenzelm@45666: val _ = Toplevel.status tr Isabelle_Markup.forked; wenzelm@44185: val start = Timing.start (); wenzelm@44645: val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; wenzelm@44185: val _ = timing tr (Timing.result start); wenzelm@45666: val _ = Toplevel.status tr Isabelle_Markup.joined; wenzelm@44185: val _ = List.app (Toplevel.error_msg tr) errs; wenzelm@44185: in wenzelm@44185: (case result of wenzelm@44614: NONE => wenzelm@44804: let wenzelm@44804: val _ = if null errs then Exn.interrupt () else (); wenzelm@45666: val _ = Toplevel.status tr Isabelle_Markup.failed; wenzelm@44804: in (st, no_print) end wenzelm@44185: | SOME st' => wenzelm@44804: let wenzelm@45666: val _ = Toplevel.status tr Isabelle_Markup.finished; wenzelm@44804: val _ = proof_status tr st'; wenzelm@44804: val do_print = wenzelm@44804: not is_init andalso wenzelm@44804: (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); wenzelm@44804: in (st', if do_print then print_state tr st' else no_print) end) wenzelm@44185: end; wenzelm@38888: wenzelm@38888: end; wenzelm@38888: wenzelm@38888: wenzelm@38888: wenzelm@44481: (** update **) wenzelm@38418: wenzelm@44436: (* perspective *) wenzelm@44436: wenzelm@44436: fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state = wenzelm@44436: let wenzelm@44436: val old_version = the_version state old_id; wenzelm@44436: val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *) wenzelm@44436: val new_version = edit_nodes (name, Perspective perspective) old_version; wenzelm@44436: in define_version new_id new_version state end; wenzelm@44436: wenzelm@44436: wenzelm@44481: (* edits *) wenzelm@38418: wenzelm@38418: local wenzelm@38418: wenzelm@47335: fun make_required nodes = wenzelm@47335: let wenzelm@47335: val all_visible = wenzelm@47335: Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes [] wenzelm@47335: |> Graph.all_preds nodes; wenzelm@47335: val required = wenzelm@47335: fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ())) wenzelm@47335: all_visible Symtab.empty; wenzelm@47335: in Symtab.defined required end; wenzelm@47335: wenzelm@47335: fun init_theory deps node = wenzelm@47335: let wenzelm@47335: (* FIXME provide files via Scala layer, not master_dir *) wenzelm@47335: val (dir, header) = Exn.release (get_header node); wenzelm@47335: val master_dir = wenzelm@47335: (case Url.explode dir of wenzelm@47335: Url.File path => path wenzelm@47335: | _ => Path.current); wenzelm@47335: val parents = wenzelm@47335: #imports header |> map (fn import => wenzelm@47335: (case Thy_Info.lookup_theory import of (* FIXME more robust!? *) wenzelm@47335: SOME thy => thy wenzelm@47335: | NONE => wenzelm@47335: get_theory (Position.file_only import) wenzelm@47335: (snd (Future.join (the (AList.lookup (op =) deps import)))))); wenzelm@47335: in Thy_Load.begin_theory master_dir header parents end; wenzelm@47335: wenzelm@47335: fun check_theory nodes name = wenzelm@47335: is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *) wenzelm@47335: is_some (Exn.get_res (get_header (get_node nodes name))); 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@44645: fun get_common ((prev, id), exec) (found, (_, flags)) = wenzelm@44482: if found then NONE wenzelm@44482: else wenzelm@44674: let val found' = wenzelm@44674: is_none exec orelse op <> (pairself (Option.map #1) (exec, lookup_entry node0 id)); wenzelm@44645: in SOME (found', (prev, update_flags prev flags)) end; wenzelm@44645: val (found, (common, flags)) = wenzelm@44645: iterate_entries get_common node (false, (NONE, (true, true))); wenzelm@44645: in wenzelm@44645: if found then (common, flags) wenzelm@44645: else wenzelm@44645: let val last = Entries.get_after (get_entries node) common wenzelm@44645: in (last, update_flags last flags) end wenzelm@44645: end; wenzelm@44645: wenzelm@44645: fun illegal_init () = error "Illegal theory header after end of theory"; wenzelm@44482: wenzelm@44674: fun new_exec state bad_init command_id' (execs, command_exec, init) = wenzelm@44645: if bad_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@44645: (Toplevel.modify_init (the_default illegal_init init), NONE) wenzelm@44645: else (I, init); wenzelm@44660: val exec_id' = new_id (); wenzelm@46876: val exec_id'_string = print_id exec_id'; wenzelm@46876: val tr = wenzelm@46876: Position.setmp_thread_data (Position.id_only exec_id'_string) wenzelm@46876: (fn () => wenzelm@46876: #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span) wenzelm@46876: |> modify_init wenzelm@46876: |> Toplevel.put_id exec_id'_string); wenzelm@46876: val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command (tr ()) st); 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@44222: val new_version = 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@44476: val updated = wenzelm@44544: nodes |> Graph.schedule wenzelm@44199: (fn deps => fn (name, node) => wenzelm@44544: if not (is_touched node orelse is_required name) wenzelm@44544: then Future.value (([], [], []), node) wenzelm@44444: else wenzelm@44479: let wenzelm@44479: val node0 = node_of old_version name; wenzelm@44979: fun init () = init_theory deps node; wenzelm@44645: val bad_init = wenzelm@44645: not (check_theory nodes name andalso forall (check_theory nodes o #1) deps); wenzelm@44479: in wenzelm@44482: (singleton o Future.forks) wenzelm@44482: {name = "Document.update", group = NONE, wenzelm@44482: deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} wenzelm@44482: (fn () => wenzelm@44482: let wenzelm@44544: val required = is_required name; wenzelm@44482: val last_visible = #2 (get_perspective node); wenzelm@44645: val (common, (visible, initial)) = last_common state last_visible node0 node; wenzelm@44674: val common_command_exec = the_default_entry node common; wenzelm@44479: wenzelm@44674: val (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@44645: else new_exec state bad_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@44482: else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res wenzelm@44482: else SOME (id0 :: res)) node0 []; wenzelm@44480: wenzelm@44674: val last_exec = if command_id = no_id then NONE else SOME command_id; wenzelm@44482: val result = wenzelm@44482: if is_some (after_entry node last_exec) then no_result wenzelm@44674: else Lazy.map #1 exec; wenzelm@44480: wenzelm@44482: val node' = node wenzelm@44482: |> fold reset_entry no_execs wenzelm@44674: |> fold (fn (id, exec) => update_entry id (SOME exec)) execs wenzelm@44482: |> set_last_exec last_exec wenzelm@44482: |> set_result result wenzelm@44482: |> set_touched false; wenzelm@44482: in ((no_execs, execs, [(name, node')]), node') end) wenzelm@44479: end) wenzelm@44479: |> 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@44479: val updated_nodes = maps #3 updated; wenzelm@44476: val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes; wenzelm@38418: wenzelm@44197: val state' = state wenzelm@44476: |> define_version new_id (fold put_node updated_nodes new_version); wenzelm@44479: in ((command_execs, last_execs), state') end; wenzelm@38418: wenzelm@38418: end; wenzelm@38418: wenzelm@38418: wenzelm@38418: (* execute *) wenzelm@38418: wenzelm@38418: fun execute version_id state = wenzelm@44674: state |> map_state (fn (versions, commands, _) => wenzelm@38418: let wenzelm@38418: val version = the_version state version_id; wenzelm@38418: wenzelm@44674: fun force_exec _ _ NONE = () wenzelm@44674: | force_exec node command_id (SOME (_, exec)) = wenzelm@44386: let wenzelm@44386: val (_, print) = Lazy.force exec; wenzelm@44386: val _ = wenzelm@44439: if #1 (get_perspective node) command_id wenzelm@44386: then ignore (Lazy.future Future.default_params print) wenzelm@44386: else (); wenzelm@44386: in () end; wenzelm@38418: wenzelm@44673: val group = Future.new_group NONE; wenzelm@44299: val _ = wenzelm@44201: nodes_of version |> Graph.schedule wenzelm@44201: (fn deps => fn (name, node) => wenzelm@44302: (singleton o Future.forks) wenzelm@44673: {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), wenzelm@44614: deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} wenzelm@44674: (iterate_entries (fn ((_, id), exec) => fn () => wenzelm@44674: SOME (force_exec node id exec)) node)); wenzelm@40520: wenzelm@44674: in (versions, commands, (version_id, group)) end); wenzelm@44673: wenzelm@44673: wenzelm@44673: (* remove versions *) wenzelm@44673: wenzelm@44674: fun remove_versions ids state = state |> map_state (fn (versions, _, execution) => wenzelm@44673: let wenzelm@44673: val _ = member (op =) ids (#1 execution) andalso wenzelm@44673: error ("Attempt to remove execution version " ^ print_id (#1 execution)); wenzelm@44673: wenzelm@44673: val versions' = fold delete_version ids versions; wenzelm@44674: val commands' = wenzelm@44675: (versions', Inttab.empty) |-> wenzelm@44673: Inttab.fold (fn (_, version) => nodes_of version |> wenzelm@44673: Graph.fold (fn (_, (node, _)) => node |> wenzelm@44674: iterate_entries (fn ((_, id), _) => wenzelm@44674: SOME o Inttab.insert (K true) (id, the_command state id)))); wenzelm@44674: in (versions', commands', execution) end); wenzelm@38418: wenzelm@43713: 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: