# HG changeset patch # User wenzelm # Date 1373057904 -7200 # Node ID 3a35ce87a55c4fe255e4334944d93007d29cba5c # Parent b7badd371e4d9f2b798478a6dbe96ae816c65df3 tuned signature; tuned comments; diff -r b7badd371e4d -r 3a35ce87a55c src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Jul 05 22:09:16 2013 +0200 +++ b/src/Pure/Isar/toplevel.ML Fri Jul 05 22:58:24 2013 +0200 @@ -81,7 +81,7 @@ val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition val skip_proof: (int -> int) -> transition -> transition val skip_proof_to_theory: (int -> bool) -> transition -> transition - val put_id: int -> transition -> transition + val exec_id: Document_ID.exec -> transition -> transition val unknown_theory: transition -> transition val unknown_proof: transition -> transition val unknown_context: transition -> transition @@ -585,8 +585,8 @@ (* runtime position *) -fun put_id id (tr as Transition {pos, ...}) = - position (Position.put_id (Markup.print_int id) pos) tr; +fun exec_id id (tr as Transition {pos, ...}) = + position (Position.put_id (Document_ID.print id) pos) tr; fun setmp_thread_position (Transition {pos, ...}) f x = Position.setmp_thread_data pos f x; diff -r b7badd371e4d -r 3a35ce87a55c src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Jul 05 22:09:16 2013 +0200 +++ b/src/Pure/PIDE/command.ML Fri Jul 05 22:58:24 2013 +0200 @@ -8,19 +8,18 @@ sig type eval_process type eval = {exec_id: Document_ID.exec, eval_process: eval_process} + val eval_result_state: eval -> Toplevel.state type print_process type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process} type exec = eval * print list + val no_exec: exec + val exec_ids: exec -> Document_ID.exec list val read: (unit -> theory) -> Token.T list -> Toplevel.transition - val no_eval: eval - val eval_result_state: eval -> Toplevel.state val eval: (unit -> theory) -> Token.T list -> eval -> eval val print: string -> eval -> print list type print_fn = Toplevel.transition -> Toplevel.state -> unit val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit - val no_exec: exec - val exec_ids: exec -> Document_ID.exec list - val exec_run: exec -> unit + val execute: exec -> unit val stable_eval: eval -> bool val stable_print: print -> bool end; @@ -70,16 +69,29 @@ -(** main phases **) +(** main phases of execution **) + +(* basic type definitions *) 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}; + type eval_process = eval_state memo; type eval = {exec_id: Document_ID.exec, eval_process: eval_process}; +fun eval_result ({eval_process, ...}: eval) = memo_result eval_process; +val eval_result_state = #state o eval_result; + type print_process = unit memo; type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}; +type exec = eval * print list; +val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []); + +fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints; + (* read *) @@ -113,14 +125,6 @@ (* eval *) -val no_eval_state: eval_state = - {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel}; - -val no_eval: eval = {exec_id = Document_ID.none, eval_process = memo_value no_eval_state}; - -fun eval_result ({eval_process, ...}: eval) = memo_result eval_process; -val eval_result_state = #state o eval_result; - local fun run int tr st = @@ -179,7 +183,7 @@ let val tr = Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) - (fn () => read init span |> Toplevel.put_id exec_id) (); + (fn () => read init span |> Toplevel.exec_id exec_id) (); in eval_state span tr (eval_result eval0) end; in {exec_id = exec_id, eval_process = memo process} end; @@ -214,7 +218,7 @@ fun process () = let val {failed, command, state = st', ...} = eval_result eval; - val tr = Toplevel.put_id exec_id command; + val tr = Toplevel.exec_id exec_id command; in if failed then () else print_error tr (fn () => print_fn tr st') () end; in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end | Exn.Exn exn => @@ -223,7 +227,7 @@ fun process () = let val {command, ...} = eval_result eval; - val tr = Toplevel.put_id exec_id command; + val tr = Toplevel.exec_id exec_id command; in output_error tr exn end; in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end)); @@ -246,24 +250,13 @@ in if do_print then Toplevel.print_state false st' else () end)); - -(** managed evaluation **) - -(* execution *) +(* overall execution process *) -type exec = eval * print list; -val no_exec: exec = (no_eval, []); - -fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints; - -fun exec_run (({eval_process, ...}, prints): exec) = +fun execute (({eval_process, ...}, prints): exec) = (memo_eval eval_process; prints |> List.app (fn {name, pri, print_process, ...} => memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process)); - -(* stable situations after cancellation *) - fun stable_goals exec_id = not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))); diff -r b7badd371e4d -r 3a35ce87a55c src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Jul 05 22:09:16 2013 +0200 +++ b/src/Pure/PIDE/command.scala Fri Jul 05 22:58:24 2013 +0200 @@ -2,12 +2,11 @@ Author: Fabian Immler, TU Munich Author: Makarius -Prover commands with semantic state. +Prover commands with accumulated results from execution. */ package isabelle -import java.lang.System import scala.collection.mutable import scala.collection.immutable.SortedMap @@ -84,7 +83,9 @@ state.add_status(markup) .add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!? - case _ => System.err.println("Ignored status message: " + msg); state + case _ => + java.lang.System.err.println("Ignored status message: " + msg) + state }) case XML.Elem(Markup(Markup.REPORT, _), msgs) => @@ -104,7 +105,7 @@ val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) state.add_markup(info) case _ => - // FIXME System.err.println("Ignored report message: " + msg) + // FIXME java.lang.System.err.println("Ignored report message: " + msg) state }) case XML.Elem(Markup(name, atts), body) => @@ -122,7 +123,9 @@ else st0 st1 - case _ => System.err.println("Ignored message without serial number: " + message); this + case _ => + java.lang.System.err.println("Ignored message without serial number: " + message) + this } } diff -r b7badd371e4d -r 3a35ce87a55c src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Jul 05 22:09:16 2013 +0200 +++ b/src/Pure/PIDE/document.ML Fri Jul 05 22:58:24 2013 +0200 @@ -2,7 +2,7 @@ Author: Makarius Document as collection of named nodes, each consisting of an editable -list of commands, with asynchronous read/eval/print processes. +list of commands, associated with asynchronous execution process. *) signature DOCUMENT = @@ -201,11 +201,20 @@ (** main state -- document structure and execution process **) +type execution = + {version_id: Document_ID.version, + group: Future.group, + running: bool Unsynchronized.ref}; + +val no_execution = + {version_id = Document_ID.none, + group = Future.new_group NONE, + running = Unsynchronized.ref false}; + abstype state = State of - {versions: version Inttab.table, (*version_id -> document content*) - commands: (string * Token.T list lazy) Inttab.table, (*command_id -> named span*) - execution: - Document_ID.version * Future.group * bool Unsynchronized.ref} (*current execution process*) + {versions: version Inttab.table, (*version id -> document content*) + commands: (string * Token.T list lazy) Inttab.table, (*command id -> named span*) + execution: execution} (*current execution process*) with fun make_state (versions, commands, execution) = @@ -215,81 +224,85 @@ make_state (f (versions, commands, execution)); val init_state = - make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, - (Document_ID.none, Future.new_group NONE, Unsynchronized.ref false)); + make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution); fun execution_of (State {execution, ...}) = execution; (* document versions *) -fun define_version (id: Document_ID.version) version = +fun define_version version_id version = map_state (fn (versions, commands, _) => let - val versions' = Inttab.update_new (id, version) versions + val versions' = Inttab.update_new (version_id, version) versions handle Inttab.DUP dup => err_dup "document version" dup; - val execution' = (id, Future.new_group NONE, Unsynchronized.ref true); + val execution' = + {version_id = version_id, + group = Future.new_group NONE, + running = Unsynchronized.ref true}; in (versions', commands, execution') end); -fun the_version (State {versions, ...}) (id: Document_ID.version) = - (case Inttab.lookup versions id of - NONE => err_undef "document version" id +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 (id: Document_ID.version) versions = Inttab.delete id versions - handle Inttab.UNDEF _ => err_undef "document version" id; +fun delete_version version_id versions = + Inttab.delete version_id versions + handle Inttab.UNDEF _ => err_undef "document version" version_id; (* commands *) -fun define_command (id: Document_ID.command) name text = +fun define_command command_id name text = map_state (fn (versions, commands, execution) => let - val id_string = Document_ID.print id; - val span = Lazy.lazy (fn () => - Position.setmp_thread_data (Position.id_only id_string) - (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text) - ()); + val id = Document_ID.print command_id; + val span = + Lazy.lazy (fn () => + Position.setmp_thread_data (Position.id_only id) + (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ()); val _ = - Position.setmp_thread_data (Position.id_only id_string) + Position.setmp_thread_data (Position.id_only id) (fn () => Output.status (Markup.markup_only Markup.accepted)) (); val commands' = - Inttab.update_new (id, (name, span)) commands + Inttab.update_new (command_id, (name, span)) commands handle Inttab.DUP dup => err_dup "command" dup; in (versions, commands', execution) end); -fun the_command (State {commands, ...}) (id: Document_ID.command) = - (case Inttab.lookup commands id of - NONE => err_undef "command" id +fun the_command (State {commands, ...}) command_id = + (case Inttab.lookup commands command_id of + NONE => err_undef "command" command_id | SOME command => command); end; -fun remove_versions ids state = state |> map_state (fn (versions, _, execution) => +fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) => let - val _ = member (op =) ids (#1 execution) andalso - error ("Attempt to remove execution version " ^ Document_ID.print (#1 execution)); + 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 ids versions; + 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 ((_, id), _) => - SOME o Inttab.insert (K true) (id, the_command state id)))); + iterate_entries (fn ((_, command_id), _) => + SOME o Inttab.insert (K true) (command_id, the_command state command_id)))); in (versions', commands', execution) end); (** document execution **) -val discontinue_execution = execution_of #> (fn (_, _, running) => running := false); -val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group); -val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group); +val discontinue_execution = execution_of #> (fn {running, ...} => running := false); +val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group); +val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group); fun start_execution state = let - val (version_id, group, running) = execution_of state; + val {version_id, group, running} = execution_of state; val _ = (singleton o Future.forks) {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true} @@ -306,7 +319,7 @@ (fn () => iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of - SOME exec => if ! running then SOME (Command.exec_run exec) else NONE + SOME exec => if ! running then SOME (Command.execute exec) else NONE | NONE => NONE)) node ())))); in () end; @@ -347,9 +360,9 @@ SOME thy => thy | NONE => Toplevel.end_theory (Position.file_only import) - (Command.eval_result_state - (the_default Command.no_eval - (get_result (snd (the (AList.lookup (op =) deps 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 Thy_Load.begin_theory master_dir header parents end; @@ -423,9 +436,9 @@ in -fun update (old_id: Document_ID.version) (new_id: Document_ID.version) edits state = +fun update old_version_id new_version_id edits state = let - val old_version = the_version state old_id; + val old_version = the_version state old_version_id; val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); val nodes = nodes_of new_version; @@ -510,7 +523,7 @@ val updated_nodes = map_filter #3 updated; val state' = state - |> define_version new_id (fold put_node updated_nodes new_version); + |> define_version new_version_id (fold put_node updated_nodes new_version); in (command_execs, state') end; end; diff -r b7badd371e4d -r 3a35ce87a55c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Jul 05 22:09:16 2013 +0200 +++ b/src/Pure/ROOT.ML Fri Jul 05 22:58:24 2013 +0200 @@ -256,6 +256,7 @@ (*toplevel transactions*) use "Isar/proof_node.ML"; +use "PIDE/document_id.ML"; use "Isar/toplevel.ML"; (*theory documents*) @@ -265,7 +266,6 @@ use "Isar/outer_syntax.ML"; use "General/graph_display.ML"; use "Thy/present.ML"; -use "PIDE/document_id.ML"; use "PIDE/command.ML"; use "Thy/thy_load.ML"; use "Thy/thy_info.ML";