mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
authorwenzelm
Sat Nov 06 19:36:54 2010 +0100 (2010-11-06 ago)
changeset 403954985aaade799
parent 40394 6dcb6cbf0719
child 40396 c4c6fa6819aa
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 06 18:10:35 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 06 19:36:54 2010 +0100
     1.3 @@ -37,8 +37,6 @@
     1.4    val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
     1.5    val diag_state: unit -> Toplevel.state
     1.6    val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
     1.7 -  val cd: Path.T -> Toplevel.transition -> Toplevel.transition
     1.8 -  val pwd: Toplevel.transition -> Toplevel.transition
     1.9    val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    1.10    val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    1.11    val print_context: Toplevel.transition -> Toplevel.transition
    1.12 @@ -289,12 +287,6 @@
    1.13  val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()");
    1.14  
    1.15  
    1.16 -(* current working directory *)
    1.17 -
    1.18 -fun cd path = Toplevel.imperative (fn () => File.cd path);
    1.19 -val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
    1.20 -
    1.21 -
    1.22  (* present draft files *)
    1.23  
    1.24  fun display_drafts files = Toplevel.imperative (fn () =>
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 06 18:10:35 2010 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 06 19:36:54 2010 +0100
     2.3 @@ -915,12 +915,13 @@
     2.4  (** system commands (for interactive mode only) **)
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
     2.8 -    (Parse.path >> (Toplevel.no_timing oo Isar_Cmd.cd));
     2.9 +  Outer_Syntax.improper_command "cd" "change current working directory" Keyword.control
    2.10 +    (Parse.path >> (fn path => Toplevel.no_timing o Toplevel.imperative (fn () => File.cd path)));
    2.11  
    2.12  val _ =
    2.13    Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
    2.14 -    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
    2.15 +    (Scan.succeed (Toplevel.no_timing o
    2.16 +      Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())))));
    2.17  
    2.18  val _ =
    2.19    Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
    2.20 @@ -962,7 +963,7 @@
    2.21      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
    2.22  
    2.23  val _ =
    2.24 -  Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
    2.25 +  Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.control
    2.26      (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
    2.27  
    2.28  val _ =