src/Pure/Isar/isar_syn.ML
changeset 40395 4985aaade799
parent 39214 49fc6c842d6c
child 40399 a3acca2bddc9
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 06 18:10:35 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 06 19:36:54 2010 +0100
     1.3 @@ -915,12 +915,13 @@
     1.4  (** system commands (for interactive mode only) **)
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
     1.8 -    (Parse.path >> (Toplevel.no_timing oo Isar_Cmd.cd));
     1.9 +  Outer_Syntax.improper_command "cd" "change current working directory" Keyword.control
    1.10 +    (Parse.path >> (fn path => Toplevel.no_timing o Toplevel.imperative (fn () => File.cd path)));
    1.11  
    1.12  val _ =
    1.13    Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
    1.14 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
    1.15 +    (Scan.succeed (Toplevel.no_timing o
    1.16 +      Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())))));
    1.17  
    1.18  val _ =
    1.19    Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
    1.20 @@ -962,7 +963,7 @@
    1.21      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
    1.22  
    1.23  val _ =
    1.24 -  Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
    1.25 +  Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.control
    1.26      (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
    1.27  
    1.28  val _ =