# HG changeset patch
# User wenzelm
# Date 1199311254 -3600
# Node ID 11bec58fc289666e2737f283b08f8cb69fb36552
# Parent  6c2adbf41c7c5108c0490d1f042c4c297d7a7ae4
Isabelle.command: IsarCmd.nested_command (with properties);

diff -r 6c2adbf41c7c -r 11bec58fc289 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jan 02 23:00:52 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 02 23:00:54 2008 +0100
@@ -750,11 +750,9 @@
 
 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 command expected"))
-      handle ERROR msg => Scan.fail_with (K msg)));
+    ((Scan.optional P.properties [] -- P.position P.string) :|-- (fn (props, arg) =>
+      Scan.succeed (K (IsarCmd.nested_command props arg))
+        handle ERROR msg => Scan.fail_with (K msg)));