# HG changeset patch
# User wenzelm
# Date 1193324277 -7200
# Node ID b568f8c5d5ca72098f989b86254e710181bc0bd6
# Parent  e1146aa1e3e3fdf05d3f9ef76c6aad106581534c
made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);

diff -r e1146aa1e3e3 -r b568f8c5d5ca src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Oct 25 13:52:05 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 25 16:57:57 2007 +0200
@@ -731,7 +731,7 @@
 
 val _ =
   OuterSyntax.improper_command "undo" "undo last command" K.control
-    (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo));
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
 
 val _ =
   OuterSyntax.improper_command "kill" "kill current history node" K.control
diff -r e1146aa1e3e3 -r b568f8c5d5ca src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Oct 25 13:52:05 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Oct 25 16:57:57 2007 +0200
@@ -231,7 +231,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-fun undoP () = (*undo without output*)
+fun undoP () = (*undo without output -- historical*)
   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));