src/Pure/PIDE/command.ML
changeset 52953 2c927b7501c5
parent 52853 4ab66773a41f
child 52999 1f09c98a3232
equal deleted inserted replaced
52952:07423b37bc22 52953:2c927b7501c5
    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 * string list) list -> string ->
    17   val print: bool -> (string * string list) list -> string ->
    18     eval -> print list -> print list option
    18     eval -> print list -> print list option
    19   type print_fn = Toplevel.transition -> Toplevel.state -> unit
    19   type print_fn = Toplevel.transition -> Toplevel.state -> unit
    20   val print_function: string ->
    20   type print_function =
    21     ({command_name: string, args: string list} ->
    21     {command_name: string, args: string list} ->
    22       {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
    22       {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
       
    23   val print_function: string -> print_function -> unit
    23   val no_print_function: string -> unit
    24   val no_print_function: string -> unit
    24   type exec = eval * print list
    25   type exec = eval * print list
    25   val no_exec: exec
    26   val no_exec: exec
    26   val exec_ids: exec option -> Document_ID.exec list
    27   val exec_ids: exec option -> Document_ID.exec list
    27   val exec: Document_ID.execution -> exec -> unit
    28   val exec: Document_ID.execution -> exec -> unit
   201 
   202 
   202 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   203 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   203 
   204 
   204 type print_function =
   205 type print_function =
   205   {command_name: string, args: string list} ->
   206   {command_name: string, args: string list} ->
   206     {delay: Time.time option, pri: int, persistent: bool, print_fn: print_fn} option;
   207     {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
   207 
   208 
   208 local
   209 local
   209 
   210 
   210 val print_functions =
   211 val print_functions =
   211   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
   212   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
   230   let
   231   let
   231     val print_functions = Synchronized.value print_functions;
   232     val print_functions = Synchronized.value print_functions;
   232 
   233 
   233     fun new_print name args get_pr =
   234     fun new_print name args get_pr =
   234       let
   235       let
   235         fun make_print strict {delay, pri, persistent, print_fn} =
   236         fun make_print {delay, pri, persistent, strict, print_fn} =
   236           let
   237           let
   237             val exec_id = Document_ID.make ();
   238             val exec_id = Document_ID.make ();
   238             fun process () =
   239             fun process () =
   239               let
   240               let
   240                 val {failed, command, state = st', ...} = eval_result eval;
   241                 val {failed, command, state = st', ...} = eval_result eval;
   241                 val tr = Toplevel.exec_id exec_id command;
   242                 val tr = Toplevel.exec_id exec_id command;
   242               in
   243               in
   243                 if failed andalso not strict then ()
   244                 if failed andalso strict then ()
   244                 else print_error tr (fn () => print_fn tr st')
   245                 else print_error tr (fn () => print_fn tr st')
   245               end;
   246               end;
   246           in
   247           in
   247            Print {
   248             Print {
   248              name = name, args = args, delay = delay, pri = pri, persistent = persistent,
   249               name = name, args = args, delay = delay, pri = pri, persistent = persistent,
   249              exec_id = exec_id, print_process = memo exec_id process}
   250               exec_id = exec_id, print_process = memo exec_id process}
   250           end;
   251           end;
   251         val params = {command_name = command_name, args = args};
   252         val params = {command_name = command_name, args = args};
   252       in
   253       in
   253         (case Exn.capture (Runtime.controlled_execution get_pr) params of
   254         (case Exn.capture (Runtime.controlled_execution get_pr) params of
   254           Exn.Res NONE => NONE
   255           Exn.Res NONE => NONE
   255         | Exn.Res (SOME pr) => SOME (make_print false pr)
   256         | Exn.Res (SOME pr) => SOME (make_print pr)
   256         | Exn.Exn exn =>
   257         | Exn.Exn exn =>
   257             SOME (make_print true
   258             SOME (make_print {delay = NONE, pri = 0, persistent = false,
   258               {delay = NONE, pri = 0, persistent = false, print_fn = fn _ => fn _ => reraise exn}))
   259               strict = false, print_fn = fn _ => fn _ => reraise exn}))
   259       end;
   260       end;
   260 
   261 
   261     fun get_print (a, b) =
   262     fun get_print (a, b) =
   262       (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
   263       (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
   263         NONE =>
   264         NONE =>
   288 end;
   289 end;
   289 
   290 
   290 val _ =
   291 val _ =
   291   print_function "print_state"
   292   print_function "print_state"
   292     (fn {command_name, ...} =>
   293     (fn {command_name, ...} =>
   293       SOME {delay = NONE, pri = 1, persistent = true,
   294       SOME {delay = NONE, pri = 1, persistent = true, strict = true,
   294         print_fn = fn tr => fn st' =>
   295         print_fn = fn tr => fn st' =>
   295           let
   296           let
   296             val is_init = Keyword.is_theory_begin command_name;
   297             val is_init = Keyword.is_theory_begin command_name;
   297             val is_proof = Keyword.is_proof command_name;
   298             val is_proof = Keyword.is_proof command_name;
   298             val do_print =
   299             val do_print =