# HG changeset patch # User wenzelm # Date 1372883433 -7200 # Node ID 0dcadc90550b42ec6a3a800dd01b4ae77ee33939 # Parent 8dd8ab81f1d7d9c6a1ad98d6f5bdeface7a8a67e more print function parameters; check command_visible statically in assignment, instead of dynamically in execution; diff -r 8dd8ab81f1d7 -r 0dcadc90550b src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Jul 03 21:55:15 2013 +0200 +++ b/src/Pure/PIDE/command.ML Wed Jul 03 22:30:33 2013 +0200 @@ -17,9 +17,12 @@ val read: span -> Toplevel.transition val eval: span -> Toplevel.transition -> Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool}) - val print: Toplevel.transition -> Toplevel.state -> (string * unit lazy) list - val print_function: string -> - ({tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option) -> unit + type print = {name: string, pri: int, pr: unit lazy} + val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list + type print_function = + {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} -> + (unit -> unit) option + val print_function: string -> int -> print_function -> unit end; structure Command: COMMAND = @@ -151,31 +154,35 @@ (* print *) +type print_function = + {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} -> + (unit -> unit) option; + +type print = {name: string, pri: int, pr: unit lazy}; + local -type print_function = - {tr: Toplevel.transition, state: Toplevel.state} -> (unit -> unit) option; - val print_functions = - Synchronized.var "Command.print_functions" ([]: (string * print_function) list); + Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list); in -fun print tr st' = - rev (Synchronized.value print_functions) |> map_filter (fn (name, f) => - (case f {tr = tr, state = st'} of - SOME pr => SOME (name, (Lazy.lazy o Toplevel.setmp_thread_position tr) pr) +fun print st tr st' = + rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) => + (case f {old_state = st, tr = tr, state = st'} of + SOME pr => + SOME {name = name, pri = pri, pr = (Lazy.lazy o Toplevel.setmp_thread_position tr) pr} | NONE => NONE)); -fun print_function name f = +fun print_function name pri 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)); + AList.update (op =) (name, (pri, f)) funs)); end; -val _ = print_function "print_state" (fn {tr, state} => +val _ = print_function "print_state" 0 (fn {tr, state, ...} => let val is_init = Toplevel.is_init tr; val is_proof = Keyword.is_proof (Toplevel.name_of tr); diff -r 8dd8ab81f1d7 -r 0dcadc90550b src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Jul 03 21:55:15 2013 +0200 +++ b/src/Pure/PIDE/document.ML Wed Jul 03 22:30:33 2013 +0200 @@ -63,8 +63,8 @@ type perspective = (command_id -> bool) * command_id option; structure Entries = Linear_Set(type key = command_id val ord = int_ord); -type print = string * unit lazy; -type exec = ((Toplevel.state * {malformed: bool}) * print list) Command.memo; (*eval/print process*) +type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo; + (*eval/print process*) val no_exec = Command.memo_value ((Toplevel.toplevel, {malformed = false}), []); abstype node = Node of @@ -324,16 +324,12 @@ fun start_execution state = let - fun run node command_id exec = - let - val (_, print) = Command.memo_eval exec; - val _ = - if visible_command node command_id then - print |> List.app (fn (a, pr) => - ignore - (Lazy.future {name = a, group = NONE, deps = [], pri = 0, interrupts = true} pr)) - else (); - in () end; + fun execute exec = + Command.memo_eval exec + |> (fn (_, print) => + print |> List.app (fn {name, pri, pr} => + Lazy.future {name = name, group = NONE, deps = [], pri = pri, interrupts = true} pr + |> ignore)); val (version_id, group, running) = execution_of state; @@ -351,9 +347,9 @@ {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false} (fn () => - iterate_entries (fn ((_, id), opt_exec) => fn () => + iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of - SOME (_, exec) => if ! running then SOME (run node id exec) else NONE + SOME (_, exec) => if ! running then SOME (execute exec) else NONE | NONE => NONE)) node ())))); in () end; @@ -437,7 +433,7 @@ else (common, flags) end; -fun new_exec state proper_init command_id' (execs, command_exec, init) = +fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) = if not proper_init andalso is_none init then NONE else let @@ -458,10 +454,10 @@ val exec' = Command.memo (fn () => let - val (st_malformed, _) = Command.memo_result (snd (snd command_exec)); + val ((st, malformed), _) = Command.memo_result (snd (snd command_exec)); val tr = read (); - val ({failed}, (st', malformed')) = Command.eval span tr st_malformed; - val print = if failed then [] else Command.print tr st'; + val ({failed}, (st', malformed')) = Command.eval span tr (st, malformed); + val print = if failed orelse not command_visible then [] else Command.print st tr st'; in ((st', malformed'), print) end); val command_exec' = (command_id', (exec_id', exec')); in SOME (command_exec' :: execs, command_exec', init') end; @@ -511,7 +507,7 @@ iterate_entries_after common (fn ((prev, id), _) => fn res => if not node_required andalso prev = last_visible then NONE - else new_exec state proper_init id res) node; + else new_exec state proper_init (visible_command node id) id res) node; val no_execs = iterate_entries_after common