1.1 --- a/src/Pure/PIDE/command.ML Wed Jul 03 21:55:15 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Wed Jul 03 22:30:33 2013 +0200
1.3 @@ -17,9 +17,12 @@
1.4 val read: span -> Toplevel.transition
1.5 val eval: span -> Toplevel.transition ->
1.6 Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
1.7 - val print: Toplevel.transition -> Toplevel.state -> (string * unit lazy) list
1.8 - val print_function: string ->
1.9 - ({tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option) -> unit
1.10 + type print = {name: string, pri: int, pr: unit lazy}
1.11 + val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
1.12 + type print_function =
1.13 + {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
1.14 + (unit -> unit) option
1.15 + val print_function: string -> int -> print_function -> unit
1.16 end;
1.17
1.18 structure Command: COMMAND =
1.19 @@ -151,31 +154,35 @@
1.20
1.21 (* print *)
1.22
1.23 +type print_function =
1.24 + {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
1.25 + (unit -> unit) option;
1.26 +
1.27 +type print = {name: string, pri: int, pr: unit lazy};
1.28 +
1.29 local
1.30
1.31 -type print_function =
1.32 - {tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option;
1.33 -
1.34 val print_functions =
1.35 - Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
1.36 + Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
1.37
1.38 in
1.39
1.40 -fun print tr st' =
1.41 - rev (Synchronized.value print_functions) |> map_filter (fn (name, f) =>
1.42 - (case f {tr = tr, state = st'} of
1.43 - SOME pr => SOME (name, (Lazy.lazy o Toplevel.setmp_thread_position tr) pr)
1.44 +fun print st tr st' =
1.45 + rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
1.46 + (case f {old_state = st, tr = tr, state = st'} of
1.47 + SOME pr =>
1.48 + SOME {name = name, pri = pri, pr = (Lazy.lazy o Toplevel.setmp_thread_position tr) pr}
1.49 | NONE => NONE));
1.50
1.51 -fun print_function name f =
1.52 +fun print_function name pri f =
1.53 Synchronized.change print_functions (fn funs =>
1.54 (if not (AList.defined (op =) funs name) then ()
1.55 else warning ("Redefining command print function: " ^ quote name);
1.56 - AList.update (op =) (name, f) funs));
1.57 + AList.update (op =) (name, (pri, f)) funs));
1.58
1.59 end;
1.60
1.61 -val _ = print_function "print_state" (fn {tr, state} =>
1.62 +val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
1.63 let
1.64 val is_init = Toplevel.is_init tr;
1.65 val is_proof = Keyword.is_proof (Toplevel.name_of tr);
2.1 --- a/src/Pure/PIDE/document.ML Wed Jul 03 21:55:15 2013 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Wed Jul 03 22:30:33 2013 +0200
2.3 @@ -63,8 +63,8 @@
2.4 type perspective = (command_id -> bool) * command_id option;
2.5 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
2.6
2.7 -type print = string * unit lazy;
2.8 -type exec = ((Toplevel.state * {malformed: bool}) * print list) Command.memo; (*eval/print process*)
2.9 +type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo;
2.10 + (*eval/print process*)
2.11 val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), []);
2.12
2.13 abstype node = Node of
2.14 @@ -324,16 +324,12 @@
2.15
2.16 fun start_execution state =
2.17 let
2.18 - fun run node command_id exec =
2.19 - let
2.20 - val (_, print) = Command.memo_eval exec;
2.21 - val _ =
2.22 - if visible_command node command_id then
2.23 - print |> List.app (fn (a, pr) =>
2.24 - ignore
2.25 - (Lazy.future {name = a, group = NONE, deps = [], pri = 0, interrupts = true} pr))
2.26 - else ();
2.27 - in () end;
2.28 + fun execute exec =
2.29 + Command.memo_eval exec
2.30 + |> (fn (_, print) =>
2.31 + print |> List.app (fn {name, pri, pr} =>
2.32 + Lazy.future {name = name, group = NONE, deps = [], pri = pri, interrupts = true} pr
2.33 + |> ignore));
2.34
2.35 val (version_id, group, running) = execution_of state;
2.36
2.37 @@ -351,9 +347,9 @@
2.38 {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
2.39 deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
2.40 (fn () =>
2.41 - iterate_entries (fn ((_, id), opt_exec) => fn () =>
2.42 + iterate_entries (fn (_, opt_exec) => fn () =>
2.43 (case opt_exec of
2.44 - SOME (_, exec) => if ! running then SOME (run node id exec) else NONE
2.45 + SOME (_, exec) => if ! running then SOME (execute exec) else NONE
2.46 | NONE => NONE)) node ()))));
2.47 in () end;
2.48
2.49 @@ -437,7 +433,7 @@
2.50 else (common, flags)
2.51 end;
2.52
2.53 -fun new_exec state proper_init command_id' (execs, command_exec, init) =
2.54 +fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
2.55 if not proper_init andalso is_none init then NONE
2.56 else
2.57 let
2.58 @@ -458,10 +454,10 @@
2.59 val exec' =
2.60 Command.memo (fn () =>
2.61 let
2.62 - val (st_malformed, _) = Command.memo_result (snd (snd command_exec));
2.63 + val ((st, malformed), _) = Command.memo_result (snd (snd command_exec));
2.64 val tr = read ();
2.65 - val ({failed}, (st', malformed')) = Command.eval span tr st_malformed;
2.66 - val print = if failed then [] else Command.print tr st';
2.67 + val ({failed}, (st', malformed')) = Command.eval span tr (st, malformed);
2.68 + val print = if failed orelse not command_visible then [] else Command.print st tr st';
2.69 in ((st', malformed'), print) end);
2.70 val command_exec' = (command_id', (exec_id', exec'));
2.71 in SOME (command_exec' :: execs, command_exec', init') end;
2.72 @@ -511,7 +507,7 @@
2.73 iterate_entries_after common
2.74 (fn ((prev, id), _) => fn res =>
2.75 if not node_required andalso prev = last_visible then NONE
2.76 - else new_exec state proper_init id res) node;
2.77 + else new_exec state proper_init (visible_command node id) id res) node;
2.78
2.79 val no_execs =
2.80 iterate_entries_after common