# HG changeset patch
# User wenzelm
# Date 953071074 -3600
# Node ID 59d66fe9bbb9cb78ecd7bddadbe6aaafa396f0ba
# Parent  614f18139d47cd682965be98eb5c3b319b034edd
silence undo command;

diff -r 614f18139d47 -r 59d66fe9bbb9 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Tue Mar 14 11:33:30 2000 +0100
+++ b/src/Pure/Interface/proof_general.ML	Tue Mar 14 22:57:54 2000 +0100
@@ -206,6 +206,10 @@
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
+val silent_undoP =	(* FIXME same name for compatibility with PG/Isabelle99 *)
+  OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
+    (Scan.succeed IsarCmd.undo);
+
 val context_thy_onlyP =
   OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
     (P.name >> IsarThy.init_context update_thy_only);
@@ -231,7 +235,7 @@
     (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name)));
 
 fun init_outer_syntax () = OuterSyntax.add_parsers
- [restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
+ [silent_undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
   inform_file_processedP, inform_file_retractedP];
 
 end;
@@ -240,13 +244,13 @@
 (* init *)
 
 fun init isar =
- (setup_xsymbols_output ();
+ (if isar then init_outer_syntax () else ();
+  setup_xsymbols_output ();
   setup_messages ();
   setup_state ();
   setup_thy_loader ();
   print_mode := [proof_generalN];
   set quick_and_dirty;
-  if isar then init_outer_syntax () else ();
   ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
   if isar then Isar.sync_main () else isa_restart ());