more print function parameters;
authorwenzelm
Wed Jul 03 22:30:33 2013 +0200 (2013-07-03)
changeset 525150dcadc90550b
parent 52514 8dd8ab81f1d7
child 52516 b5b3c888df9f
more print function parameters;
check command_visible statically in assignment, instead of dynamically in execution;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     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