1.1 --- a/src/Pure/Isar/toplevel.ML Fri Jul 05 22:09:16 2013 +0200
1.2 +++ b/src/Pure/Isar/toplevel.ML Fri Jul 05 22:58:24 2013 +0200
1.3 @@ -81,7 +81,7 @@
1.4 val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
1.5 val skip_proof: (int -> int) -> transition -> transition
1.6 val skip_proof_to_theory: (int -> bool) -> transition -> transition
1.7 - val put_id: int -> transition -> transition
1.8 + val exec_id: Document_ID.exec -> transition -> transition
1.9 val unknown_theory: transition -> transition
1.10 val unknown_proof: transition -> transition
1.11 val unknown_context: transition -> transition
1.12 @@ -585,8 +585,8 @@
1.13
1.14 (* runtime position *)
1.15
1.16 -fun put_id id (tr as Transition {pos, ...}) =
1.17 - position (Position.put_id (Markup.print_int id) pos) tr;
1.18 +fun exec_id id (tr as Transition {pos, ...}) =
1.19 + position (Position.put_id (Document_ID.print id) pos) tr;
1.20
1.21 fun setmp_thread_position (Transition {pos, ...}) f x =
1.22 Position.setmp_thread_data pos f x;
2.1 --- a/src/Pure/PIDE/command.ML Fri Jul 05 22:09:16 2013 +0200
2.2 +++ b/src/Pure/PIDE/command.ML Fri Jul 05 22:58:24 2013 +0200
2.3 @@ -8,19 +8,18 @@
2.4 sig
2.5 type eval_process
2.6 type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
2.7 + val eval_result_state: eval -> Toplevel.state
2.8 type print_process
2.9 type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
2.10 type exec = eval * print list
2.11 + val no_exec: exec
2.12 + val exec_ids: exec -> Document_ID.exec list
2.13 val read: (unit -> theory) -> Token.T list -> Toplevel.transition
2.14 - val no_eval: eval
2.15 - val eval_result_state: eval -> Toplevel.state
2.16 val eval: (unit -> theory) -> Token.T list -> eval -> eval
2.17 val print: string -> eval -> print list
2.18 type print_fn = Toplevel.transition -> Toplevel.state -> unit
2.19 val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
2.20 - val no_exec: exec
2.21 - val exec_ids: exec -> Document_ID.exec list
2.22 - val exec_run: exec -> unit
2.23 + val execute: exec -> unit
2.24 val stable_eval: eval -> bool
2.25 val stable_print: print -> bool
2.26 end;
2.27 @@ -70,16 +69,29 @@
2.28
2.29
2.30
2.31 -(** main phases **)
2.32 +(** main phases of execution **)
2.33 +
2.34 +(* basic type definitions *)
2.35
2.36 type eval_state =
2.37 {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
2.38 +val init_eval_state =
2.39 + {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
2.40 +
2.41 type eval_process = eval_state memo;
2.42 type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
2.43
2.44 +fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
2.45 +val eval_result_state = #state o eval_result;
2.46 +
2.47 type print_process = unit memo;
2.48 type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
2.49
2.50 +type exec = eval * print list;
2.51 +val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
2.52 +
2.53 +fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
2.54 +
2.55
2.56 (* read *)
2.57
2.58 @@ -113,14 +125,6 @@
2.59
2.60 (* eval *)
2.61
2.62 -val no_eval_state: eval_state =
2.63 - {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
2.64 -
2.65 -val no_eval: eval = {exec_id = Document_ID.none, eval_process = memo_value no_eval_state};
2.66 -
2.67 -fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
2.68 -val eval_result_state = #state o eval_result;
2.69 -
2.70 local
2.71
2.72 fun run int tr st =
2.73 @@ -179,7 +183,7 @@
2.74 let
2.75 val tr =
2.76 Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
2.77 - (fn () => read init span |> Toplevel.put_id exec_id) ();
2.78 + (fn () => read init span |> Toplevel.exec_id exec_id) ();
2.79 in eval_state span tr (eval_result eval0) end;
2.80 in {exec_id = exec_id, eval_process = memo process} end;
2.81
2.82 @@ -214,7 +218,7 @@
2.83 fun process () =
2.84 let
2.85 val {failed, command, state = st', ...} = eval_result eval;
2.86 - val tr = Toplevel.put_id exec_id command;
2.87 + val tr = Toplevel.exec_id exec_id command;
2.88 in if failed then () else print_error tr (fn () => print_fn tr st') () end;
2.89 in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
2.90 | Exn.Exn exn =>
2.91 @@ -223,7 +227,7 @@
2.92 fun process () =
2.93 let
2.94 val {command, ...} = eval_result eval;
2.95 - val tr = Toplevel.put_id exec_id command;
2.96 + val tr = Toplevel.exec_id exec_id command;
2.97 in output_error tr exn end;
2.98 in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
2.99
2.100 @@ -246,24 +250,13 @@
2.101 in if do_print then Toplevel.print_state false st' else () end));
2.102
2.103
2.104 +(* overall execution process *)
2.105
2.106 -(** managed evaluation **)
2.107 -
2.108 -(* execution *)
2.109 -
2.110 -type exec = eval * print list;
2.111 -val no_exec: exec = (no_eval, []);
2.112 -
2.113 -fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
2.114 -
2.115 -fun exec_run (({eval_process, ...}, prints): exec) =
2.116 +fun execute (({eval_process, ...}, prints): exec) =
2.117 (memo_eval eval_process;
2.118 prints |> List.app (fn {name, pri, print_process, ...} =>
2.119 memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
2.120
2.121 -
2.122 -(* stable situations after cancellation *)
2.123 -
2.124 fun stable_goals exec_id =
2.125 not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
2.126
3.1 --- a/src/Pure/PIDE/command.scala Fri Jul 05 22:09:16 2013 +0200
3.2 +++ b/src/Pure/PIDE/command.scala Fri Jul 05 22:58:24 2013 +0200
3.3 @@ -2,12 +2,11 @@
3.4 Author: Fabian Immler, TU Munich
3.5 Author: Makarius
3.6
3.7 -Prover commands with semantic state.
3.8 +Prover commands with accumulated results from execution.
3.9 */
3.10
3.11 package isabelle
3.12
3.13 -import java.lang.System
3.14
3.15 import scala.collection.mutable
3.16 import scala.collection.immutable.SortedMap
3.17 @@ -84,7 +83,9 @@
3.18 state.add_status(markup)
3.19 .add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
3.20
3.21 - case _ => System.err.println("Ignored status message: " + msg); state
3.22 + case _ =>
3.23 + java.lang.System.err.println("Ignored status message: " + msg)
3.24 + state
3.25 })
3.26
3.27 case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
3.28 @@ -104,7 +105,7 @@
3.29 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
3.30 state.add_markup(info)
3.31 case _ =>
3.32 - // FIXME System.err.println("Ignored report message: " + msg)
3.33 + // FIXME java.lang.System.err.println("Ignored report message: " + msg)
3.34 state
3.35 })
3.36 case XML.Elem(Markup(name, atts), body) =>
3.37 @@ -122,7 +123,9 @@
3.38 else st0
3.39
3.40 st1
3.41 - case _ => System.err.println("Ignored message without serial number: " + message); this
3.42 + case _ =>
3.43 + java.lang.System.err.println("Ignored message without serial number: " + message)
3.44 + this
3.45 }
3.46 }
3.47
4.1 --- a/src/Pure/PIDE/document.ML Fri Jul 05 22:09:16 2013 +0200
4.2 +++ b/src/Pure/PIDE/document.ML Fri Jul 05 22:58:24 2013 +0200
4.3 @@ -2,7 +2,7 @@
4.4 Author: Makarius
4.5
4.6 Document as collection of named nodes, each consisting of an editable
4.7 -list of commands, with asynchronous read/eval/print processes.
4.8 +list of commands, associated with asynchronous execution process.
4.9 *)
4.10
4.11 signature DOCUMENT =
4.12 @@ -201,11 +201,20 @@
4.13
4.14 (** main state -- document structure and execution process **)
4.15
4.16 +type execution =
4.17 + {version_id: Document_ID.version,
4.18 + group: Future.group,
4.19 + running: bool Unsynchronized.ref};
4.20 +
4.21 +val no_execution =
4.22 + {version_id = Document_ID.none,
4.23 + group = Future.new_group NONE,
4.24 + running = Unsynchronized.ref false};
4.25 +
4.26 abstype state = State of
4.27 - {versions: version Inttab.table, (*version_id -> document content*)
4.28 - commands: (string * Token.T list lazy) Inttab.table, (*command_id -> named span*)
4.29 - execution:
4.30 - Document_ID.version * Future.group * bool Unsynchronized.ref} (*current execution process*)
4.31 + {versions: version Inttab.table, (*version id -> document content*)
4.32 + commands: (string * Token.T list lazy) Inttab.table, (*command id -> named span*)
4.33 + execution: execution} (*current execution process*)
4.34 with
4.35
4.36 fun make_state (versions, commands, execution) =
4.37 @@ -215,81 +224,85 @@
4.38 make_state (f (versions, commands, execution));
4.39
4.40 val init_state =
4.41 - make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty,
4.42 - (Document_ID.none, Future.new_group NONE, Unsynchronized.ref false));
4.43 + make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
4.44
4.45 fun execution_of (State {execution, ...}) = execution;
4.46
4.47
4.48 (* document versions *)
4.49
4.50 -fun define_version (id: Document_ID.version) version =
4.51 +fun define_version version_id version =
4.52 map_state (fn (versions, commands, _) =>
4.53 let
4.54 - val versions' = Inttab.update_new (id, version) versions
4.55 + val versions' = Inttab.update_new (version_id, version) versions
4.56 handle Inttab.DUP dup => err_dup "document version" dup;
4.57 - val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
4.58 + val execution' =
4.59 + {version_id = version_id,
4.60 + group = Future.new_group NONE,
4.61 + running = Unsynchronized.ref true};
4.62 in (versions', commands, execution') end);
4.63
4.64 -fun the_version (State {versions, ...}) (id: Document_ID.version) =
4.65 - (case Inttab.lookup versions id of
4.66 - NONE => err_undef "document version" id
4.67 +fun the_version (State {versions, ...}) version_id =
4.68 + (case Inttab.lookup versions version_id of
4.69 + NONE => err_undef "document version" version_id
4.70 | SOME version => version);
4.71
4.72 -fun delete_version (id: Document_ID.version) versions = Inttab.delete id versions
4.73 - handle Inttab.UNDEF _ => err_undef "document version" id;
4.74 +fun delete_version version_id versions =
4.75 + Inttab.delete version_id versions
4.76 + handle Inttab.UNDEF _ => err_undef "document version" version_id;
4.77
4.78
4.79 (* commands *)
4.80
4.81 -fun define_command (id: Document_ID.command) name text =
4.82 +fun define_command command_id name text =
4.83 map_state (fn (versions, commands, execution) =>
4.84 let
4.85 - val id_string = Document_ID.print id;
4.86 - val span = Lazy.lazy (fn () =>
4.87 - Position.setmp_thread_data (Position.id_only id_string)
4.88 - (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
4.89 - ());
4.90 + val id = Document_ID.print command_id;
4.91 + val span =
4.92 + Lazy.lazy (fn () =>
4.93 + Position.setmp_thread_data (Position.id_only id)
4.94 + (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
4.95 val _ =
4.96 - Position.setmp_thread_data (Position.id_only id_string)
4.97 + Position.setmp_thread_data (Position.id_only id)
4.98 (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
4.99 val commands' =
4.100 - Inttab.update_new (id, (name, span)) commands
4.101 + Inttab.update_new (command_id, (name, span)) commands
4.102 handle Inttab.DUP dup => err_dup "command" dup;
4.103 in (versions, commands', execution) end);
4.104
4.105 -fun the_command (State {commands, ...}) (id: Document_ID.command) =
4.106 - (case Inttab.lookup commands id of
4.107 - NONE => err_undef "command" id
4.108 +fun the_command (State {commands, ...}) command_id =
4.109 + (case Inttab.lookup commands command_id of
4.110 + NONE => err_undef "command" command_id
4.111 | SOME command => command);
4.112
4.113 end;
4.114
4.115 -fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
4.116 +fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
4.117 let
4.118 - val _ = member (op =) ids (#1 execution) andalso
4.119 - error ("Attempt to remove execution version " ^ Document_ID.print (#1 execution));
4.120 + val _ =
4.121 + member (op =) version_ids (#version_id execution) andalso
4.122 + error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution));
4.123
4.124 - val versions' = fold delete_version ids versions;
4.125 + val versions' = fold delete_version version_ids versions;
4.126 val commands' =
4.127 (versions', Inttab.empty) |->
4.128 Inttab.fold (fn (_, version) => nodes_of version |>
4.129 String_Graph.fold (fn (_, (node, _)) => node |>
4.130 - iterate_entries (fn ((_, id), _) =>
4.131 - SOME o Inttab.insert (K true) (id, the_command state id))));
4.132 + iterate_entries (fn ((_, command_id), _) =>
4.133 + SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
4.134 in (versions', commands', execution) end);
4.135
4.136
4.137
4.138 (** document execution **)
4.139
4.140 -val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
4.141 -val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
4.142 -val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
4.143 +val discontinue_execution = execution_of #> (fn {running, ...} => running := false);
4.144 +val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
4.145 +val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
4.146
4.147 fun start_execution state =
4.148 let
4.149 - val (version_id, group, running) = execution_of state;
4.150 + val {version_id, group, running} = execution_of state;
4.151 val _ =
4.152 (singleton o Future.forks)
4.153 {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
4.154 @@ -306,7 +319,7 @@
4.155 (fn () =>
4.156 iterate_entries (fn (_, opt_exec) => fn () =>
4.157 (case opt_exec of
4.158 - SOME exec => if ! running then SOME (Command.exec_run exec) else NONE
4.159 + SOME exec => if ! running then SOME (Command.execute exec) else NONE
4.160 | NONE => NONE)) node ()))));
4.161 in () end;
4.162
4.163 @@ -347,9 +360,9 @@
4.164 SOME thy => thy
4.165 | NONE =>
4.166 Toplevel.end_theory (Position.file_only import)
4.167 - (Command.eval_result_state
4.168 - (the_default Command.no_eval
4.169 - (get_result (snd (the (AList.lookup (op =) deps import))))))));
4.170 + (case get_result (snd (the (AList.lookup (op =) deps import))) of
4.171 + NONE => Toplevel.toplevel
4.172 + | SOME eval => Command.eval_result_state eval)));
4.173 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
4.174 in Thy_Load.begin_theory master_dir header parents end;
4.175
4.176 @@ -423,9 +436,9 @@
4.177
4.178 in
4.179
4.180 -fun update (old_id: Document_ID.version) (new_id: Document_ID.version) edits state =
4.181 +fun update old_version_id new_version_id edits state =
4.182 let
4.183 - val old_version = the_version state old_id;
4.184 + val old_version = the_version state old_version_id;
4.185 val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
4.186
4.187 val nodes = nodes_of new_version;
4.188 @@ -510,7 +523,7 @@
4.189 val updated_nodes = map_filter #3 updated;
4.190
4.191 val state' = state
4.192 - |> define_version new_id (fold put_node updated_nodes new_version);
4.193 + |> define_version new_version_id (fold put_node updated_nodes new_version);
4.194 in (command_execs, state') end;
4.195
4.196 end;
5.1 --- a/src/Pure/ROOT.ML Fri Jul 05 22:09:16 2013 +0200
5.2 +++ b/src/Pure/ROOT.ML Fri Jul 05 22:58:24 2013 +0200
5.3 @@ -256,6 +256,7 @@
5.4
5.5 (*toplevel transactions*)
5.6 use "Isar/proof_node.ML";
5.7 +use "PIDE/document_id.ML";
5.8 use "Isar/toplevel.ML";
5.9
5.10 (*theory documents*)
5.11 @@ -265,7 +266,6 @@
5.12 use "Isar/outer_syntax.ML";
5.13 use "General/graph_display.ML";
5.14 use "Thy/present.ML";
5.15 -use "PIDE/document_id.ML";
5.16 use "PIDE/command.ML";
5.17 use "Thy/thy_load.ML";
5.18 use "Thy/thy_info.ML";