--- a/src/Pure/Isar/isar_syn.ML Fri Dec 07 22:19:45 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Dec 07 22:19:49 2007 +0100
@@ -746,6 +746,17 @@
(Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.kill));
+(* nested command *)
+
+val _ =
+ OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
+ (P.position P.string :|-- (fn (str, pos) =>
+ (case OuterSyntax.parse pos str of
+ [transition] => Scan.succeed (K transition)
+ | _ => Scan.fail_with (K "exactly one nested Isabelle command expected"))
+ handle ERROR msg => Scan.fail_with (K ("malformed nested command\n" ^ msg))));
+
+
(** diagnostic commands (for interactive mode only) **)