# HG changeset patch
# User wenzelm
# Date 1197062389 -3600
# Node ID 11ee8b183477db08a54aa1ceaf57f9949a0eab7c
# Parent  d739f48ef40cd3c1ec7d7b8663f2b2d924fb84f7
added nested 'Isabelle.command';

diff -r d739f48ef40c -r 11ee8b183477 src/Pure/Isar/isar_syn.ML
--- 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) **)