src/Pure/PIDE/command.ML
changeset 59331 4139db32821e
parent 59328 b83d6c3c439a
child 59348 8a6788917b32
equal deleted inserted replaced
59330:cb3a4caf206d 59331:4139db32821e
   352 
   352 
   353 val _ =
   353 val _ =
   354   print_function "print_state"
   354   print_function "print_state"
   355     (fn {keywords, command_name, ...} =>
   355     (fn {keywords, command_name, ...} =>
   356       if Keyword.is_printed keywords command_name then
   356       if Keyword.is_printed keywords command_name then
   357         SOME {delay = NONE, pri = 1, persistent = false, strict = true,
   357         SOME {delay = NONE, pri = 1, persistent = false, strict = false,
   358           print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
   358           print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
   359       else NONE);
   359       else NONE);
   360 
   360 
   361 
   361 
   362 (* combined execution *)
   362 (* combined execution *)