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