# HG changeset patch
# User wenzelm
# Date 1217862813 -7200
# Node ID de34a576c7568e3ede42f5bf26d0f1029310495f
# Parent  3a85bc6bfd739e32d2b3fd3aeafe761175438d0e
Isar.command: explicitly set transaction position, as required for prepare_command errors;
adapted Isabelle.command;

diff -r 3a85bc6bfd73 -r de34a576c756 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 04 10:37:33 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 04 17:13:33 2008 +0200
@@ -706,10 +706,14 @@
 
 (* nested commands *)
 
+val props_text =
+  Scan.optional P.properties [] -- P.position P.string >> (fn (props, (str, pos)) =>
+    (Position.of_properties (Position.default_properties pos props), str));
+
 val _ =
   OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
-    ((Scan.optional P.properties [] -- P.position P.string) :|-- (fn (props, text) =>
-      Scan.succeed (K (OuterSyntax.prepare_command props text))
+    (props_text :|-- (fn (pos, str) =>
+      Scan.succeed (K (OuterSyntax.prepare_command pos str))
         handle ERROR msg => Scan.fail_with (K msg)));
 
 
@@ -717,9 +721,9 @@
 
 val _ =
   OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control
-    (Scan.optional P.properties [] -- P.position P.string >> (fn (props, text) =>
-      Toplevel.no_timing o Toplevel.imperative (fn () =>
-        ignore (Isar.create_command (OuterSyntax.prepare_command props text)))));
+    (props_text >> (fn (pos, str) =>
+      Toplevel.no_timing o Toplevel.position pos o Toplevel.imperative (fn () =>
+        ignore (Isar.create_command (OuterSyntax.prepare_command pos str)))));
 
 val _ =
   OuterSyntax.improper_command "Isar.insert" "insert command (Isar editor model)" K.control