# HG changeset patch
# User wenzelm
# Date 1289068614 -3600
# Node ID 4985aaade799f7be7cd653de9c90ce1707fcef30
# Parent  6dcb6cbf07190042c890ff8749b06d5e91429254
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;

diff -r 6dcb6cbf0719 -r 4985aaade799 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 06 18:10:35 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 06 19:36:54 2010 +0100
@@ -37,8 +37,6 @@
   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
   val diag_state: unit -> Toplevel.state
   val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
-  val cd: Path.T -> Toplevel.transition -> Toplevel.transition
-  val pwd: Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
@@ -289,12 +287,6 @@
 val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()");
 
 
-(* current working directory *)
-
-fun cd path = Toplevel.imperative (fn () => File.cd path);
-val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
-
-
 (* present draft files *)
 
 fun display_drafts files = Toplevel.imperative (fn () =>
diff -r 6dcb6cbf0719 -r 4985aaade799 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Nov 06 18:10:35 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 06 19:36:54 2010 +0100
@@ -915,12 +915,13 @@
 (** system commands (for interactive mode only) **)
 
 val _ =
-  Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
-    (Parse.path >> (Toplevel.no_timing oo Isar_Cmd.cd));
+  Outer_Syntax.improper_command "cd" "change current working directory" Keyword.control
+    (Parse.path >> (fn path => Toplevel.no_timing o Toplevel.imperative (fn () => File.cd path)));
 
 val _ =
   Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
+    (Scan.succeed (Toplevel.no_timing o
+      Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())))));
 
 val _ =
   Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
@@ -962,7 +963,7 @@
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
 
 val _ =
-  Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
+  Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.control
     (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
 
 val _ =