equal
deleted
inserted
replaced
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 *) |