src/Pure/PIDE/command.ML
changeset 57839 d5b0fa6f1f7a
parent 56944 578dc6b4be89
child 57844 ae3eac418c5f
equal deleted inserted replaced
57838:c21f2c52f54b 57839:d5b0fa6f1f7a
   380 
   380 
   381 val _ =
   381 val _ =
   382   print_function "Execution.print"
   382   print_function "Execution.print"
   383     (fn {args, exec_id, ...} =>
   383     (fn {args, exec_id, ...} =>
   384       if null args then
   384       if null args then
   385         SOME {delay = NONE, pri = 1, persistent = false, strict = true,
   385         SOME {delay = NONE, pri = 1, persistent = false, strict = false,
   386           print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
   386           print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
   387       else NONE);
   387       else NONE);
   388 
   388 
   389 val _ =
   389 val _ =
   390   print_function "print_state"
   390   print_function "print_state"