src/Pure/PIDE/command.ML
changeset 52850 9fff9f78240a
parent 52785 ecc7d8de4f94
child 52853 4ab66773a41f
equal deleted inserted replaced
52849:199e9fa5a5c2 52850:9fff9f78240a
    12   val eval_running: eval -> bool
    12   val eval_running: eval -> bool
    13   val eval_finished: eval -> bool
    13   val eval_finished: eval -> bool
    14   val eval_result_state: eval -> Toplevel.state
    14   val eval_result_state: eval -> Toplevel.state
    15   val eval: (unit -> theory) -> Token.T list -> eval -> eval
    15   val eval: (unit -> theory) -> Token.T list -> eval -> eval
    16   type print
    16   type print
    17   val print: bool -> string -> eval -> print list -> print list option
    17   val print: bool -> (string * string list) list -> string ->
       
    18     eval -> print list -> print list option
    18   type print_fn = Toplevel.transition -> Toplevel.state -> unit
    19   type print_fn = Toplevel.transition -> Toplevel.state -> unit
    19   val print_function: string ->
    20   val print_function: string ->
    20     ({command_name: string} ->
    21     ({command_name: string, args: string list} ->
    21       {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
    22       {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
    22   val no_print_function: string -> unit
    23   val no_print_function: string -> unit
    23   type exec = eval * print list
    24   type exec = eval * print list
    24   val no_exec: exec
    25   val no_exec: exec
    25   val exec_ids: exec option -> Document_ID.exec list
    26   val exec_ids: exec option -> Document_ID.exec list
   193 
   194 
   194 
   195 
   195 (* print *)
   196 (* print *)
   196 
   197 
   197 datatype print = Print of
   198 datatype print = Print of
   198  {name: string, delay: Time.time option, pri: int, persistent: bool,
   199  {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
   199   exec_id: Document_ID.exec, print_process: unit memo};
   200   exec_id: Document_ID.exec, print_process: unit memo};
   200 
   201 
   201 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   202 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   202 
   203 
   203 type print_function =
   204 type print_function =
   204   {command_name: string} ->
   205   {command_name: string, args: string list} ->
   205     {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
   206     {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
   206 
   207 
   207 local
   208 local
   208 
   209 
   209 val print_functions =
   210 val print_functions =
   221 
   222 
   222 fun print_persistent (Print {persistent, ...}) = persistent;
   223 fun print_persistent (Print {persistent, ...}) = persistent;
   223 
   224 
   224 in
   225 in
   225 
   226 
   226 fun print command_visible command_name eval old_prints =
   227 fun print command_visible command_overlays command_name eval old_prints =
   227   let
   228   let
   228     fun new_print (name, get_pr) =
   229     val print_functions = Synchronized.value print_functions;
       
   230 
       
   231     fun new_print name args get_pr =
   229       let
   232       let
   230         fun make_print strict {delay, pri, persistent, print_fn} =
   233         fun make_print strict {delay, pri, persistent, print_fn} =
   231           let
   234           let
   232             val exec_id = Document_ID.make ();
   235             val exec_id = Document_ID.make ();
   233             fun process () =
   236             fun process () =
   238                 if failed andalso not strict then ()
   241                 if failed andalso not strict then ()
   239                 else print_error tr (fn () => print_fn tr st')
   242                 else print_error tr (fn () => print_fn tr st')
   240               end;
   243               end;
   241           in
   244           in
   242            Print {
   245            Print {
   243              name = name, delay = delay, pri = pri, persistent = persistent,
   246              name = name, args = args, delay = delay, pri = pri, persistent = persistent,
   244              exec_id = exec_id, print_process = memo exec_id process}
   247              exec_id = exec_id, print_process = memo exec_id process}
   245           end;
   248           end;
       
   249         val params = {command_name = command_name, args = args};
   246       in
   250       in
   247         (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
   251         (case Exn.capture (Runtime.controlled_execution get_pr) params of
   248           Exn.Res NONE => NONE
   252           Exn.Res NONE => NONE
   249         | Exn.Res (SOME pr) => SOME (make_print false pr)
   253         | Exn.Res (SOME pr) => SOME (make_print false pr)
   250         | Exn.Exn exn =>
   254         | Exn.Exn exn =>
   251             SOME (make_print true
   255             SOME (make_print true
   252               {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
   256               {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
   253       end;
   257       end;
   254 
   258 
       
   259     fun get_print (a, b) =
       
   260       (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
       
   261         NONE =>
       
   262           (case AList.lookup (op =) print_functions a of
       
   263             NONE => NONE
       
   264           | SOME get_pr => new_print a b get_pr)
       
   265       | some => some);
       
   266 
   255     val new_prints =
   267     val new_prints =
   256       if command_visible then
   268       if command_visible then
   257         rev (Synchronized.value print_functions) |> map_filter (fn pr =>
   269         distinct (op =) (fold (fn (a, _) => cons (a, [])) print_functions command_overlays)
   258           (case find_first (fn Print {name, ...} => name = fst pr) old_prints of
   270         |> map_filter get_print
   259             NONE => new_print pr
       
   260           | some => some))
       
   261       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   271       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   262   in
   272   in
   263     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   273     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   264   end;
   274   end;
   265 
   275 
   274 
   284 
   275 end;
   285 end;
   276 
   286 
   277 val _ =
   287 val _ =
   278   print_function "print_state"
   288   print_function "print_state"
   279     (fn {command_name} =>
   289     (fn {command_name, ...} =>
   280       SOME {delay = NONE, pri = 1, persistent = true,
   290       SOME {delay = NONE, pri = 1, persistent = true,
   281         print_fn = fn tr => fn st' =>
   291         print_fn = fn tr => fn st' =>
   282           let
   292           let
   283             val is_init = Keyword.is_theory_begin command_name;
   293             val is_init = Keyword.is_theory_begin command_name;
   284             val is_proof = Keyword.is_proof command_name;
   294             val is_proof = Keyword.is_proof command_name;