1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Aug 04 10:37:33 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 04 17:13:33 2008 +0200
     1.3 @@ -706,10 +706,14 @@
     1.4  
     1.5  (* nested commands *)
     1.6  
     1.7 +val props_text =
     1.8 +  Scan.optional P.properties [] -- P.position P.string >> (fn (props, (str, pos)) =>
     1.9 +    (Position.of_properties (Position.default_properties pos props), str));
    1.10 +
    1.11  val _ =
    1.12    OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
    1.13 -    ((Scan.optional P.properties [] -- P.position P.string) :|-- (fn (props, text) =>
    1.14 -      Scan.succeed (K (OuterSyntax.prepare_command props text))
    1.15 +    (props_text :|-- (fn (pos, str) =>
    1.16 +      Scan.succeed (K (OuterSyntax.prepare_command pos str))
    1.17          handle ERROR msg => Scan.fail_with (K msg)));
    1.18  
    1.19  
    1.20 @@ -717,9 +721,9 @@
    1.21  
    1.22  val _ =
    1.23    OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control
    1.24 -    (Scan.optional P.properties [] -- P.position P.string >> (fn (props, text) =>
    1.25 -      Toplevel.no_timing o Toplevel.imperative (fn () =>
    1.26 -        ignore (Isar.create_command (OuterSyntax.prepare_command props text)))));
    1.27 +    (props_text >> (fn (pos, str) =>
    1.28 +      Toplevel.no_timing o Toplevel.position pos o Toplevel.imperative (fn () =>
    1.29 +        ignore (Isar.create_command (OuterSyntax.prepare_command pos str)))));
    1.30  
    1.31  val _ =
    1.32    OuterSyntax.improper_command "Isar.insert" "insert command (Isar editor model)" K.control