--- 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;
--- 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)));
--- 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
}
}
--- 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;
--- 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";