# HG changeset patch # User wenzelm # Date 1215713008 -7200 # Node ID bddf129af8ba7844ba6cd062b77502ea93a9684f # Parent df14c9cbd21d28b38ff01c8e024ae6aca9e2759c added Isar.init_point, Isar.kill; diff -r df14c9cbd21d -r bddf129af8ba src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Jul 10 20:02:55 2008 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Jul 10 20:03:28 2008 +0200 @@ -740,15 +740,23 @@ (* global Isar state commands *) val _ = - OuterSyntax.improper_command "Isar.linear_undo" "undo tty commands" K.control + OuterSyntax.improper_command "Isar.init_point" "init command point-of-interest" K.control + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init_point)); + +val _ = + OuterSyntax.improper_command "Isar.linear_undo" "undo commands" K.control (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n))); val _ = - OuterSyntax.improper_command "Isar.undo" "undo tty commands (skipping closed proofs)" K.control + OuterSyntax.improper_command "Isar.undo" "undo commands (skipping closed proofs)" K.control (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n))); +val _ = + OuterSyntax.improper_command "Isar.kill" "kill partial proof or theory development" K.control + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill)); + (** diagnostic commands (for interactive mode only) **)