added nested_command (with explicit position argument via properties);
authorwenzelm
Wed Jan 02 23:00:52 2008 +0100 (2008-01-02 ago)
changeset 257936c2adbf41c7c
parent 25792 c7125b591885
child 25794 11bec58fc289
added nested_command (with explicit position argument via properties);
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Jan 02 23:00:51 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Jan 02 23:00:52 2008 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4    val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
     1.5    val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
     1.6    val use_commit: Toplevel.transition -> Toplevel.transition
     1.7 +  val nested_command: Markup.property list -> string * Position.T -> Toplevel.transition
     1.8    val cd: Path.T -> Toplevel.transition -> Toplevel.transition
     1.9    val pwd: Toplevel.transition -> Toplevel.transition
    1.10    val use_thy: string -> Toplevel.transition -> Toplevel.transition
    1.11 @@ -388,6 +389,16 @@
    1.12  val use_commit = Toplevel.imperative Secure.commit;
    1.13  
    1.14  
    1.15 +(* nested commands *)
    1.16 +
    1.17 +fun nested_command props (str, pos) =
    1.18 +  let val (pos', props') = Position.of_properties (props @ Position.properties_of pos) in
    1.19 +    (case OuterSyntax.parse pos' str of
    1.20 +      [transition] => Toplevel.properties props' transition
    1.21 +    | _ => error "exactly one command expected")
    1.22 +  end;
    1.23 +
    1.24 +
    1.25  (* current working directory *)
    1.26  
    1.27  fun cd path = Toplevel.imperative (fn () => (File.cd path));