diff --git a/src/Pure/Concurrent/lazy.ML b/src/Pure/Concurrent/lazy.ML --- a/src/Pure/Concurrent/lazy.ML +++ b/src/Pure/Concurrent/lazy.ML @@ -1,96 +1,115 @@ (* Title: Pure/Concurrent/lazy.ML Author: Makarius Lazy evaluation with memoing of results and regular exceptions. Parallel version based on (passive) futures, to avoid critical or multiple evaluation (unless interrupted). *) signature LAZY = sig type 'a lazy - val peek: 'a lazy -> 'a Exn.result option - val is_finished: 'a lazy -> bool val lazy: (unit -> 'a) -> 'a lazy val value: 'a -> 'a lazy + val peek: 'a lazy -> 'a Exn.result option + val is_running: 'a lazy -> bool + val is_finished: 'a lazy -> bool + val finished_result: 'a lazy -> 'a Exn.result option val force_result: 'a lazy -> 'a Exn.result val force: 'a lazy -> 'a val map: ('a -> 'b) -> 'a lazy -> 'b lazy val future: Future.params -> 'a lazy -> 'a future end; structure Lazy: LAZY = struct (* datatype *) datatype 'a expr = Expr of unit -> 'a | Result of 'a future; abstype 'a lazy = Lazy of 'a expr Synchronized.var with +fun lazy e = Lazy (Synchronized.var "lazy" (Expr e)); +fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a))); + fun peek (Lazy var) = (case Synchronized.peek var of Expr _ => NONE | Result res => Future.peek res); -fun is_finished (Lazy var) = + +(* status *) + +fun is_future pred (Lazy var) = (case Synchronized.value var of Expr _ => false + | Result res => pred res); + +fun is_running x = is_future (not o Future.is_finished) x; + +fun is_finished x = + is_future (fn res => + Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x; + +fun finished_result (Lazy var) = + (case Synchronized.value var of + Expr _ => NONE | Result res => - Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))); - -fun lazy e = Lazy (Synchronized.var "lazy" (Expr e)); -fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a))); + if Future.is_finished res then + let val result = Future.join_result res + in if Exn.is_interrupt_exn result then NONE else SOME result end + else NONE); (* force result *) fun force_result (Lazy var) = (case peek (Lazy var) of SOME res => res | NONE => uninterruptible (fn restore_attributes => fn () => let val (expr, x) = Synchronized.change_result var (fn Expr e => let val x = Future.promise I in ((SOME e, x), Result x) end | Result x => ((NONE, x), Result x)); in (case expr of SOME e => let val res0 = Exn.capture (restore_attributes e) (); val _ = Exn.capture (fn () => Future.fulfill_result x res0) (); val res = Future.join_result x; (*semantic race: some other threads might see the same interrupt, until there is a fresh start*) val _ = if Exn.is_interrupt_exn res then Synchronized.change var (fn _ => Expr e) else (); in res end | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ()) end) ()); end; fun force r = Exn.release (force_result r); fun map f x = lazy (fn () => f (force x)); (* future evaluation *) fun future params x = if is_finished x then Future.value_result (force_result x) else (singleton o Future.forks) params (fn () => force x); end; type 'a lazy = 'a Lazy.lazy; diff --git a/src/Pure/PIDE/command.ML b/src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML +++ b/src/Pure/PIDE/command.ML @@ -1,441 +1,409 @@ (* Title: Pure/PIDE/command.ML Author: Makarius Prover command execution: read -- eval -- print. *) signature COMMAND = sig type blob = (string * (SHA1.digest * string list) option) Exn.result val read_file: Path.T -> Position.T -> Path.T -> Token.file val read_thy: Toplevel.state -> theory val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> blob list -> Token.T list -> Toplevel.transition type eval val eval_eq: eval * eval -> bool val eval_running: eval -> bool val eval_finished: eval -> bool val eval_result_state: eval -> Toplevel.state val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> blob list -> Token.T list -> eval -> eval type print val print: bool -> (string * string list) list -> Keyword.keywords -> string -> eval -> print list -> print list option type print_fn = Toplevel.transition -> Toplevel.state -> unit type print_function = {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option val print_function: string -> print_function -> unit val no_print_function: string -> unit type exec = eval * print list val no_exec: exec val exec_ids: exec option -> Document_ID.exec list val exec: Document_ID.execution -> exec -> unit end; structure Command: COMMAND = struct -(** memo results **) - -datatype 'a expr = - Expr of Document_ID.exec * (unit -> 'a) | - Result of 'a Exn.result; - -abstype 'a memo = Memo of 'a expr Synchronized.var -with - -fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e))); -fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a))); - -fun memo_result (Memo v) = - (case Synchronized.value v of - Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id) - | Result res => Exn.release res); - -fun memo_finished (Memo v) = - (case Synchronized.value v of Expr _ => false | Result _ => true); - -fun memo_exec execution_id (Memo v) = - Synchronized.timed_access v (K (SOME Time.zeroTime)) - (fn expr => - (case expr of - Expr (exec_id, body) => - uninterruptible (fn restore_attributes => fn () => - let val group = Future.worker_subgroup () in - if Execution.running execution_id exec_id [group] then - let - val res = - (body - |> restore_attributes - |> Future.task_context "Command.memo_exec" group - |> Exn.interruptible_capture) (); - in SOME ((), Result res) end - else SOME ((), expr) - end) () - | Result _ => SOME ((), expr))) - |> (fn NONE => error "Conflicting command execution" | _ => ()); - -fun memo_fork params execution_id (Memo v) = - (case Synchronized.peek v of - Result _ => () - | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v)))); - -end; - - - (** main phases of execution **) (* read *) type blob = (string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*) fun read_file_node file_node master_dir pos src_path = let val _ = Position.report pos Markup.language_path; val _ = (case try Url.explode file_node of NONE => () | SOME (Url.File _) => () | _ => (Position.report pos (Markup.path file_node); error ("Prover cannot load remote file " ^ Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos))); val full_path = File.check_file (File.full_path master_dir src_path); val _ = Position.report pos (Markup.path (Path.implode full_path)); val text = File.read full_path; val lines = split_lines text; val digest = SHA1.digest text; in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end; val read_file = read_file_node ""; local fun blob_file src_path lines digest file_node = let val file_pos = Position.file file_node |> (case Position.get_id (Position.thread_data ()) of NONE => I | SOME exec_id => Position.put_id exec_id); in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end fun resolve_files keywords master_dir blobs toks = (case Outer_Syntax.parse_spans toks of [span] => span |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) => let fun make_file src_path (Exn.Res (file_node, NONE)) = Exn.interruptible_capture (fn () => read_file_node file_node master_dir pos src_path) () | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) = (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)]; Exn.Res (blob_file src_path lines digest file_node)) | make_file _ (Exn.Exn e) = Exn.Exn e; val src_paths = Keyword.command_files keywords cmd path; in if null blobs then map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) else if length src_paths = length blobs then map2 make_file src_paths blobs else error ("Misalignment of inlined files" ^ Position.here pos) end) |> Command_Span.content | _ => toks); val bootstrap_thy = ML_Context.the_global_context (); in fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy; fun read keywords thy master_dir init blobs span = let val command_reports = Outer_Syntax.command_reports thy; val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span)); val pos = (case find_first Token.is_command span of SOME tok => Token.pos_of tok | NONE => #1 proper_range); val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens keywords span; val _ = Position.reports_text (token_reports @ maps command_reports span); in if is_malformed then Toplevel.malformed pos "Malformed command syntax" else (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs span) of [tr] => Toplevel.modify_init init tr | [] => Toplevel.ignored (#1 (Token.range_of span)) | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected") handle ERROR msg => Toplevel.malformed (#1 proper_range) msg end; end; (* eval *) type eval_state = {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}; val init_eval_state = {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel}; -datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo}; +datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy}; fun eval_exec_id (Eval {exec_id, ...}) = exec_id; val eval_eq = op = o apply2 eval_exec_id; val eval_running = Execution.is_running_exec o eval_exec_id; -fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process; +fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process; -fun eval_result (Eval {eval_process, ...}) = memo_result eval_process; +fun eval_result (Eval {exec_id, eval_process}) = + (case Lazy.finished_result eval_process of + SOME result => Exn.release result + | NONE => error ("Unfinished execution result: " ^ Document_ID.print exec_id)); + val eval_result_state = #state o eval_result; local fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () => let val name = Toplevel.name_of tr; val res = if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0 else if Keyword.is_proof keywords name then Toplevel.reset_proof st0 else NONE; in (case res of NONE => st0 | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st)) end) (); fun run keywords int tr st = if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} (fn () => Toplevel.command_exception int tr st); ([], SOME st)) else Toplevel.command_errors int tr st; fun check_cmts span tr st' = Toplevel.setmp_thread_position tr (fn () => Outer_Syntax.side_comments span |> maps (fn cmt => (Thy_Output.check_text (Token.source_position_of cmt) st'; []) handle exn => if Exn.is_interrupt exn then reraise exn else Runtime.exn_messages_ids exn)) (); fun report tr m = Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) (); fun status tr m = Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); fun proof_status tr st = (case try Toplevel.proof_of st of SOME prf => status tr (Proof.status_markup prf) | NONE => ()); fun eval_state keywords span tr ({malformed, state, ...}: eval_state) = if malformed then {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel} else let val _ = Multithreading.interrupted (); val malformed' = Toplevel.is_malformed tr; val st = reset_state keywords tr state; val _ = status tr Markup.running; val (errs1, result) = run keywords true tr st; val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); val errs = errs1 @ errs2; val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; in (case result of NONE => let val _ = status tr Markup.failed; val _ = status tr Markup.finished; val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else (); in {failed = true, malformed = malformed', command = tr, state = st} end | SOME st' => let val _ = proof_status tr st'; val _ = status tr Markup.finished; in {failed = false, malformed = malformed', command = tr, state = st'} end) end; in fun eval keywords master_dir init blobs span eval0 = let val exec_id = Document_ID.make (); fun process () = let val eval_state0 = eval_result eval0; val thy = read_thy (#state eval_state0); val tr = Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) (); in eval_state keywords span tr eval_state0 end; - in Eval {exec_id = exec_id, eval_process = memo exec_id process} end; + in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end; end; (* print *) datatype print = Print of {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool, - exec_id: Document_ID.exec, print_process: unit memo}; + exec_id: Document_ID.exec, print_process: unit lazy}; fun print_exec_id (Print {exec_id, ...}) = exec_id; val print_eq = op = o apply2 print_exec_id; type print_fn = Toplevel.transition -> Toplevel.state -> unit; type print_function = {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option; local val print_functions = Synchronized.var "Command.print_functions" ([]: (string * print_function) list); fun print_error tr opt_context e = (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e () handle exn => if Exn.is_interrupt exn then reraise exn else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn); -fun print_finished (Print {print_process, ...}) = memo_finished print_process; +fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process; fun print_persistent (Print {persistent, ...}) = persistent; val overlay_ord = prod_ord string_ord (list_ord string_ord); in fun print command_visible command_overlays keywords command_name eval old_prints = let val print_functions = Synchronized.value print_functions; fun make_print name args {delay, pri, persistent, strict, print_fn} = let val exec_id = Document_ID.make (); fun process () = let val {failed, command, state = st', ...} = eval_result eval; val tr = Toplevel.exec_id exec_id command; val opt_context = try Toplevel.generic_theory_of st'; in if failed andalso strict then () else print_error tr opt_context (fn () => print_fn tr st') end; in Print { name = name, args = args, delay = delay, pri = pri, persistent = persistent, - exec_id = exec_id, print_process = memo exec_id process} + exec_id = exec_id, print_process = Lazy.lazy process} end; fun bad_print name args exn = make_print name args {delay = NONE, pri = 0, persistent = false, strict = false, print_fn = fn _ => fn _ => reraise exn}; fun new_print name args get_pr = let val params = {keywords = keywords, command_name = command_name, args = args, exec_id = eval_exec_id eval}; in (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of Exn.Res NONE => NONE | Exn.Res (SOME pr) => SOME (make_print name args pr) | Exn.Exn exn => SOME (bad_print name args exn)) end; fun get_print (a, b) = (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of NONE => (case AList.lookup (op =) print_functions a of NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a))) | SOME get_pr => new_print a b get_pr) | some => some); val new_prints = if command_visible then fold (fn (a, _) => cons (a, [])) print_functions command_overlays |> sort_distinct overlay_ord |> map_filter get_print else filter (fn print => print_finished print andalso print_persistent print) old_prints; in if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints end; fun print_function name f = Synchronized.change print_functions (fn funs => (if not (AList.defined (op =) funs name) then () else warning ("Redefining command print function: " ^ quote name); AList.update (op =) (name, f) funs)); fun no_print_function name = Synchronized.change print_functions (filter_out (equal name o #1)); end; val _ = print_function "Execution.print" (fn {args, exec_id, ...} => if null args then SOME {delay = NONE, pri = 1, persistent = false, strict = false, print_fn = fn _ => fn _ => Execution.fork_prints exec_id} else NONE); val _ = print_function "print_state" (fn {keywords, command_name, ...} => if Keyword.is_printed keywords command_name then SOME {delay = NONE, pri = 1, persistent = false, strict = true, print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()} else NONE); (* combined execution *) type exec = eval * print list; val no_exec: exec = - (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []); + (Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []); fun exec_ids NONE = [] | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints; local -fun run_print execution_id (Print {name, delay, pri, print_process, ...}) = - if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print") +fun run_process execution_id exec_id process = + let val group = Future.worker_subgroup () in + if Execution.running execution_id exec_id [group] then + ignore (Future.task_context "Command.run_process" group Lazy.force_result process) + else () + end; + +fun run_eval execution_id (Eval {exec_id, eval_process}) = + if Lazy.is_finished eval_process then () + else run_process execution_id exec_id eval_process; + +fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) = + if Lazy.is_running print_process orelse Lazy.is_finished print_process then () + else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print") then let val group = Future.worker_subgroup (); fun fork () = - memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true} - execution_id print_process; + ignore ((singleton o Future.forks) + {name = name, group = SOME group, deps = [], pri = pri, interrupts = true} + (fn () => run_process execution_id exec_id print_process)); in (case delay of NONE => fork () | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork)) end - else memo_exec execution_id print_process; + else run_process execution_id exec_id print_process; in -fun exec execution_id (Eval {eval_process, ...}, prints) = - (memo_exec execution_id eval_process; List.app (run_print execution_id) prints); +fun exec execution_id (eval, prints) = + (run_eval execution_id eval; List.app (run_print execution_id) prints); end; end; diff --git a/src/Pure/PIDE/document.ML b/src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML +++ b/src/Pure/PIDE/document.ML @@ -1,688 +1,683 @@ (* Title: Pure/PIDE/document.ML Author: Makarius Document as collection of named nodes, each consisting of an editable list of commands, associated with asynchronous execution process. *) signature DOCUMENT = sig val timing: bool Unsynchronized.ref type node_header = string * Thy_Header.header * string list type overlay = Document_ID.command * (string * string list) datatype node_edit = Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | Perspective of bool * Document_ID.command list * overlay list type edit = string * node_edit type state val init_state: state val define_blob: string -> string -> state -> state type blob_digest = (string * string option) Exn.result val define_command: Document_ID.command -> string -> blob_digest list -> ((int * int) * string) list -> state -> state val remove_versions: Document_ID.version list -> state -> state val start_execution: state -> state val update: Document_ID.version -> Document_ID.version -> edit list -> state -> Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state val state: unit -> state val change_state: (state -> state) -> unit end; structure Document: DOCUMENT = struct val timing = Unsynchronized.ref false; fun timeit msg e = cond_timeit (! timing) msg e; - - - (** document structure **) fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id); fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id); type node_header = string * Thy_Header.header * string list; type perspective = {required: bool, (*required node*) visible: Inttab.set, (*visible commands*) visible_last: Document_ID.command option, (*last visible command*) overlays: (string * string list) list Inttab.table}; (*command id -> print functions with args*) structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord); abstype node = Node of {header: node_header, (*master directory, theory header, errors*) keywords: Keyword.keywords option, (*outer syntax keywords*) perspective: perspective, (*command perspective*) entries: Command.exec option Entries.T, (*command entries with excecutions*) result: Command.eval option} (*result of last execution*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) with fun make_node (header, keywords, perspective, entries, result) = Node {header = header, keywords = keywords, perspective = perspective, entries = entries, result = result}; fun map_node f (Node {header, keywords, perspective, entries, result}) = make_node (f (header, keywords, perspective, entries, result)); fun make_perspective (required, command_ids, overlays) : perspective = {required = required, visible = Inttab.make_set command_ids, visible_last = try List.last command_ids, overlays = Inttab.make_list overlays}; val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []); val no_perspective = make_perspective (false, [], []); val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE); fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) = not required andalso Inttab.is_empty visible andalso is_none visible_last andalso Inttab.is_empty overlays; fun is_empty_node (Node {header, keywords, perspective, entries, result}) = header = no_header andalso is_none keywords andalso is_no_perspective perspective andalso Entries.is_empty entries andalso is_none result; (* basic components *) fun master_directory (Node {header = (master, _, _), ...}) = (case try Url.explode master of SOME (Url.File path) => path | _ => Path.current); fun set_header header = map_node (fn (_, keywords, perspective, entries, result) => (header, keywords, perspective, entries, result)); fun get_header_raw (Node {header, ...}) = header; fun get_header (Node {header = (master, header, errors), ...}) = if null errors then (master, header) else error (cat_lines errors); fun set_keywords keywords = map_node (fn (header, _, perspective, entries, result) => (header, keywords, perspective, entries, result)); fun get_keywords (Node {keywords, ...}) = keywords; fun read_header node span = let val {name = (name, _), imports, keywords} = #2 (get_header node); val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span; in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end; fun get_perspective (Node {perspective, ...}) = perspective; fun set_perspective args = map_node (fn (header, keywords, _, entries, result) => (header, keywords, make_perspective args, entries, result)); val required_node = #required o get_perspective; val visible_command = Inttab.defined o #visible o get_perspective; val visible_last = #visible_last o get_perspective; val visible_node = is_some o visible_last val overlays = Inttab.lookup_list o #overlays o get_perspective; fun map_entries f = map_node (fn (header, keywords, perspective, entries, result) => (header, keywords, perspective, f entries, result)); fun get_entries (Node {entries, ...}) = entries; fun iterate_entries f = Entries.iterate NONE f o get_entries; fun iterate_entries_after start f (Node {entries, ...}) = (case Entries.get_after entries start of NONE => I | SOME id => Entries.iterate (SOME id) f entries); fun get_result (Node {result, ...}) = result; fun set_result result = map_node (fn (header, keywords, perspective, entries, _) => (header, keywords, perspective, entries, result)); fun changed_result node node' = (case (get_result node, get_result node') of (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval')) | (NONE, NONE) => false | _ => true); fun pending_result node = (case get_result node of SOME eval => not (Command.eval_finished eval) | NONE => false); fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; fun default_node name = String_Graph.default_node (name, empty_node); fun update_node name f = default_node name #> String_Graph.map_node name f; (* node edits and associated executions *) type overlay = Document_ID.command * (string * string list); datatype node_edit = Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | Perspective of bool * Document_ID.command list * overlay list; type edit = string * node_edit; val after_entry = Entries.get_after o get_entries; fun lookup_entry node id = (case Entries.lookup (get_entries node) id of NONE => NONE | SOME (exec, _) => exec); fun the_entry node id = (case Entries.lookup (get_entries node) id of NONE => err_undef "command entry" id | SOME (exec, _) => exec); fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id)) | the_default_entry _ NONE = (Document_ID.none, Command.no_exec); fun assign_entry (command_id, exec) node = if is_none (Entries.lookup (get_entries node) command_id) then node else map_entries (Entries.update (command_id, exec)) node; fun reset_after id entries = (case Entries.get_after entries id of NONE => entries | SOME next => Entries.update (next, NONE) entries); val edit_node = map_entries o fold (fn (id, SOME id2) => Entries.insert_after id (id2, NONE) | (id, NONE) => Entries.delete_after id #> reset_after id); (* version operations *) val empty_version = Version String_Graph.empty; fun nodes_of (Version nodes) = nodes; val node_of = get_node o nodes_of; fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); fun edit_nodes (name, node_edit) (Version nodes) = Version (case node_edit of Edits edits => update_node name (edit_node edits) nodes | Deps (master, header, errors) => let val imports = map fst (#imports header); val nodes1 = nodes |> default_node name |> fold default_node imports; val nodes2 = nodes1 |> String_Graph.Keys.fold (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name); val (nodes3, errors1) = (String_Graph.add_deps_acyclic (name, imports) nodes2, errors) handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs); in String_Graph.map_node name (set_header (master, header, errors1)) nodes3 end | Perspective perspective => update_node name (set_perspective perspective) nodes); fun update_keywords name nodes = nodes |> String_Graph.map_node name (fn node => if is_empty_node node then node else let val (master, header, errors) = get_header_raw node; val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header); val keywords = Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords); val (keywords', errors') = (Keyword.add_keywords (#keywords header) keywords, errors) handle ERROR msg => (keywords, if member (op =) errors msg then errors else errors @ [msg]); in node |> set_header (master, header, errors') |> set_keywords (SOME keywords') end); fun edit_keywords edits (Version nodes) = Version (fold update_keywords (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits)) nodes); fun put_node (name, node) (Version nodes) = let val nodes1 = update_node name (K node) nodes; val nodes2 = if String_Graph.is_maximal nodes1 name andalso is_empty_node node then String_Graph.del_node name nodes1 else nodes1; in Version nodes2 end; end; (** main state -- document structure and execution process **) type blob_digest = (string * string option) Exn.result; (*file node name, raw digest*) type execution = {version_id: Document_ID.version, (*static version id*) execution_id: Document_ID.execution, (*dynamic execution id*) - delay_request: unit future, (*pending event timer request*) - frontier: Future.task Symtab.table}; (*node name -> running execution task*) + delay_request: unit future}; (*pending event timer request*) val no_execution: execution = - {version_id = Document_ID.none, execution_id = Document_ID.none, - delay_request = Future.value (), frontier = Symtab.empty}; + {version_id = Document_ID.none, + execution_id = Document_ID.none, + delay_request = Future.value ()}; -fun new_execution version_id delay_request frontier : execution = - {version_id = version_id, execution_id = Execution.start (), - delay_request = delay_request, frontier = frontier}; +fun new_execution version_id delay_request : execution = + {version_id = version_id, + execution_id = Execution.start (), + delay_request = delay_request}; abstype state = State of {versions: version Inttab.table, (*version id -> document content*) blobs: (SHA1.digest * string list) Symtab.table, (*raw digest -> digest, lines*) commands: (string * blob_digest list * Token.T list lazy) Inttab.table, (*command id -> name, inlined files, command span*) execution: execution} (*current execution process*) with fun make_state (versions, blobs, commands, execution) = State {versions = versions, blobs = blobs, commands = commands, execution = execution}; fun map_state f (State {versions, blobs, commands, execution}) = make_state (f (versions, blobs, commands, execution)); val init_state = make_state (Inttab.make [(Document_ID.none, empty_version)], Symtab.empty, Inttab.empty, no_execution); (* document versions *) fun define_version version_id version = - map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) => + map_state (fn (versions, blobs, commands, {delay_request, ...}) => let val versions' = Inttab.update_new (version_id, version) versions handle Inttab.DUP dup => err_dup "document version" dup; - val execution' = new_execution version_id delay_request frontier; + val execution' = new_execution version_id delay_request; in (versions', blobs, commands, execution') end); fun the_version (State {versions, ...}) version_id = (case Inttab.lookup versions version_id of NONE => err_undef "document version" version_id | SOME version => version); fun delete_version version_id versions = Inttab.delete version_id versions handle Inttab.UNDEF _ => err_undef "document version" version_id; (* inlined files *) fun define_blob digest text = map_state (fn (versions, blobs, commands, execution) => let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs in (versions, blobs', commands, execution) end); fun the_blob (State {blobs, ...}) digest = (case Symtab.lookup blobs digest of NONE => error ("Undefined blob: " ^ digest) | SOME content => content); fun resolve_blob state (blob_digest: blob_digest) = blob_digest |> Exn.map_result (fn (file_node, raw_digest) => (file_node, Option.map (the_blob state) raw_digest)); (* commands *) fun define_command command_id name command_blobs toks = map_state (fn (versions, blobs, commands, execution) => let val id = Document_ID.print command_id; val span = Lazy.lazy (fn () => Position.setmp_thread_data (Position.id_only id) (fn () => #1 (fold_map Token.make toks (Position.id id))) ()); val _ = Position.setmp_thread_data (Position.id_only id) (fn () => Output.status (Markup.markup_only Markup.accepted)) (); val commands' = Inttab.update_new (command_id, (name, command_blobs, span)) commands handle Inttab.DUP dup => err_dup "command" dup; in (versions, blobs, commands', execution) end); fun the_command (State {commands, ...}) command_id = (case Inttab.lookup commands command_id of NONE => err_undef "command" command_id | SOME command => command); val the_command_name = #1 oo the_command; end; (* remove_versions *) fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) => let val _ = member (op =) version_ids (#version_id execution) andalso error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution)); val versions' = fold delete_version version_ids versions; val commands' = (versions', Inttab.empty) |-> Inttab.fold (fn (_, version) => nodes_of version |> String_Graph.fold (fn (_, (node, _)) => node |> iterate_entries (fn ((_, command_id), _) => SOME o Inttab.insert (K true) (command_id, the_command state command_id)))); val blobs' = (commands', Symtab.empty) |-> Inttab.fold (fn (_, (_, blobs, _)) => blobs |> fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I)); in (versions', blobs', commands', execution) end); (* document execution *) fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) => timeit "Document.start_execution" (fn () => let - val {version_id, execution_id, delay_request, frontier} = execution; + val {version_id, execution_id, delay_request} = execution; val delay = seconds (Options.default_real "editor_execution_delay"); val _ = Future.cancel delay_request; val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay)); - val new_tasks = + val _ = nodes_of (the_version state version_id) |> String_Graph.schedule (fn deps => fn (name, node) => if visible_node node orelse pending_result node then let - val more_deps = - Future.task_of delay_request' :: the_list (Symtab.lookup frontier name); fun body () = iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of SOME exec => if Execution.is_running execution_id then SOME (Command.exec execution_id exec) else NONE | NONE => NONE)) node () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn; val future = (singleton o Future.forks) - {name = "theory:" ^ name, group = SOME (Future.new_group NONE), - deps = more_deps @ map #2 (maps #2 deps), - pri = 0, interrupts = false} body; - in [(name, Future.task_of future)] end + {name = "theory:" ^ name, + group = SOME (Future.new_group NONE), + deps = Future.task_of delay_request' :: maps #2 deps, + pri = 0, interrupts = false} body; + in [Future.task_of future] end else []); - val frontier' = (fold o fold) Symtab.update new_tasks frontier; val execution' = - {version_id = version_id, execution_id = execution_id, - delay_request = delay_request', frontier = frontier'}; + {version_id = version_id, execution_id = execution_id, delay_request = delay_request'}; in (versions, blobs, commands, execution') end)); (** document update **) (* exec state assignment *) type assign_update = Command.exec option Inttab.table; (*command id -> exec*) val assign_update_empty: assign_update = Inttab.empty; fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; fun assign_update_new upd (tab: assign_update) = Inttab.update_new upd tab handle Inttab.DUP dup => err_dup "exec state assignment" dup; fun assign_update_result (tab: assign_update) = Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab []; (* update *) local fun make_required nodes = let fun all_preds P = String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes [] |> String_Graph.all_preds nodes |> Symtab.make_set; val all_visible = all_preds visible_node; val all_required = all_preds required_node; in Symtab.fold (fn (a, ()) => exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? Symtab.update (a, ())) all_visible all_required end; fun loaded_theory name = (case try (unsuffix ".thy") name of SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a] | NONE => NONE); fun init_theory deps node span = let val master_dir = master_directory node; val header = read_header node span; val imports = #imports header; val parents = imports |> map (fn (import, _) => (case loaded_theory import of SOME thy => thy | NONE => Toplevel.end_theory (Position.file_only import) (case get_result (snd (the (AList.lookup (op =) deps import))) of NONE => Toplevel.toplevel | SOME eval => Command.eval_result_state eval))); val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); in Resources.begin_theory master_dir header parents end; fun check_theory full name node = is_some (loaded_theory name) orelse can get_header node andalso (not full orelse is_some (get_result node)); fun last_common keywords state node_required node0 node = let fun update_flags prev (visible, initial) = let val visible' = visible andalso prev <> visible_last node; val initial' = initial andalso (case prev of NONE => true | SOME command_id => not (Keyword.is_theory_begin keywords (the_command_name state command_id))); in (visible', initial') end; fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) = if ok then let val flags' as (visible', _) = update_flags prev flags; val ok' = (case (lookup_entry node0 command_id, opt_exec) of (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval) andalso (visible' orelse node_required orelse Command.eval_running eval) | _ => false); val assign_update' = assign_update |> ok' ? (case opt_exec of SOME (eval, prints) => let val command_visible = visible_command node command_id; val command_overlays = overlays node command_id; val command_name = the_command_name state command_id; in (case Command.print command_visible command_overlays keywords command_name eval prints of SOME prints' => assign_update_new (command_id, SOME (eval, prints')) | NONE => I) end | NONE => I); in SOME (prev, ok', flags', assign_update') end else NONE; val (common, ok, flags, assign_update') = iterate_entries get_common node (NONE, true, (true, true), assign_update_empty); val (common', flags') = if ok then let val last = Entries.get_after (get_entries node) common in (last, update_flags last flags) end else (common, flags); in (assign_update', common', flags') end; fun illegal_init _ = error "Illegal theory header after end of theory"; fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) = if not proper_init andalso is_none init then NONE else let val (_, (eval, _)) = command_exec; val command_visible = visible_command node command_id'; val command_overlays = overlays node command_id'; val (command_name, blob_digests, span0) = the_command state command_id'; val blobs = map (resolve_blob state) blob_digests; val span = Lazy.force span0; val eval' = Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span) blobs span eval; val prints' = perhaps (Command.print command_visible command_overlays keywords command_name eval') []; val exec' = (eval', prints'); val assign_update' = assign_update_new (command_id', SOME exec') assign_update; val init' = if Keyword.is_theory_begin keywords command_name then NONE else init; in SOME (assign_update', (command_id', (eval', prints')), init') end; fun removed_execs node0 (command_id, exec_ids) = subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id)); in fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () => let val old_version = the_version state old_version_id; val new_version = timeit "Document.edit_nodes" (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits); val nodes = nodes_of new_version; val required = make_required nodes; val required0 = make_required (nodes_of old_version); val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty; val updated = timeit "Document.update" (fn () => nodes |> String_Graph.schedule (fn deps => fn (name, node) => (singleton o Future.forks) {name = "Document.update", group = NONE, deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} (fn () => timeit ("Document.update " ^ name) (fn () => Runtime.exn_trace_system (fn () => let val keywords = the_default (Session.get_keywords ()) (get_keywords node); val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; val node_required = Symtab.defined required name; in if Symtab.defined edited name orelse visible_node node orelse imports_result_changed orelse Symtab.defined required0 name <> node_required then let val node0 = node_of old_version name; val init = init_theory imports node; val proper_init = check_theory false name node andalso forall (fn (name, (_, node)) => check_theory true name node) imports; val (print_execs, common, (still_visible, initial)) = if imports_result_changed then (assign_update_empty, NONE, (true, true)) else last_common keywords state node_required node0 node; val common_command_exec = the_default_entry node common; val (updated_execs, (command_id', (eval', _)), _) = (print_execs, common_command_exec, if initial then SOME init else NONE) |> (still_visible orelse node_required) ? iterate_entries_after common (fn ((prev, id), _) => fn res => if not node_required andalso prev = visible_last node then NONE else new_exec keywords state node proper_init id res) node; val assigned_execs = (node0, updated_execs) |-> iterate_entries_after common (fn ((_, command_id0), exec0) => fn res => if is_none exec0 then NONE else if assign_update_defined updated_execs command_id0 then SOME res else SOME (assign_update_new (command_id0, NONE) res)); val last_exec = if command_id' = Document_ID.none then NONE else SOME command_id'; val result = if is_none last_exec orelse is_some (after_entry node last_exec) then NONE else SOME eval'; val assign_update = assign_update_result assigned_execs; val removed = maps (removed_execs node0) assign_update; val _ = List.app Execution.cancel removed; val node' = node |> assign_update_apply assigned_execs |> set_result result; val assigned_node = SOME (name, node'); val result_changed = changed_result node0 node'; in ((removed, assign_update, assigned_node, result_changed), node') end else (([], [], NONE, false), node) end)))) |> Future.joins |> map #1); val removed = maps #1 updated; val assign_update = maps #2 updated; val assigned_nodes = map_filter #3 updated; val state' = state |> define_version new_version_id (fold put_node assigned_nodes new_version); in (removed, assign_update, state') end); end; (** global state **) val global_state = Synchronized.var "Document.global_state" init_state; fun state () = Synchronized.value global_state; val change_state = Synchronized.change global_state; end;