# HG changeset patch
# User wenzelm
# Date 1199311252 -3600
# Node ID 6c2adbf41c7c5108c0490d1f042c4c297d7a7ae4
# Parent  c7125b591885161bef14e7b8f2cc5749296a6b7c
added nested_command (with explicit position argument via properties);

diff -r c7125b591885 -r 6c2adbf41c7c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 02 23:00:51 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 02 23:00:52 2008 +0100
@@ -65,6 +65,7 @@
   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
   val use_commit: Toplevel.transition -> Toplevel.transition
+  val nested_command: Markup.property list -> string * Position.T -> Toplevel.transition
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val use_thy: string -> Toplevel.transition -> Toplevel.transition
@@ -388,6 +389,16 @@
 val use_commit = Toplevel.imperative Secure.commit;
 
 
+(* nested commands *)
+
+fun nested_command props (str, pos) =
+  let val (pos', props') = Position.of_properties (props @ Position.properties_of pos) in
+    (case OuterSyntax.parse pos' str of
+      [transition] => Toplevel.properties props' transition
+    | _ => error "exactly one command expected")
+  end;
+
+
 (* current working directory *)
 
 fun cd path = Toplevel.imperative (fn () => (File.cd path));