mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
--- 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 () =>
--- 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 _ =