# HG changeset patch
# User wenzelm
# Date 1082984250 -7200
# Node ID 08b9c690f9cf1241dd423bfd5b00cba0bd4bf998
# Parent  3506a9af46fc85577a7af7eb677e66f51d26ab44
removed obsolete 'undo';

diff -r 3506a9af46fc -r 08b9c690f9cf src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Mon Apr 26 14:56:18 2004 +0200
+++ b/src/Pure/proof_general.ML	Mon Apr 26 14:57:30 2004 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/proof_general.ML
     ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     David Aspinall and Markus Wenzel
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk).
@@ -35,7 +35,6 @@
 val xsymbolsN = "xsymbols";
 val thm_depsN = "thm_deps";
 
-
 val pgml_version_supported = "1.0";
 val pgmlN = "PGML";
 fun pgml () = pgmlN mem_string ! print_mode;
@@ -107,7 +106,6 @@
 in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
 
 
-
 (* messages and notification *)
 
 local
@@ -313,15 +311,15 @@
       print_depth_option))];
 
 
-(* Sending PGIP commands to the interface *)
+(* sending PGIP commands to the interface *)
 
 fun issue_pgip pgips = notify (XML.element "pgip" [] pgips);
 
 fun usespgml () = 
   issue_pgip [XML.element "usespgml" [("version", pgml_version_supported)] []];
 
-(* NB: the default returned here is actually the current value, so
-   repeated uses of <askprefs> will not work correctly. *)
+(*NB: the default returned here is actually the current value, so
+  repeated uses of <askprefs> will not work correctly*)
 fun show_options () = issue_pgip (map 
   (fn (name, (descr, (ty, get, _))) => (XML.element "oldhaspref"
     [("type", ty), ("descr", descr), ("default", get ())] [name])) (!options));
@@ -336,9 +334,9 @@
 	issue_pgip [XML.element "prefval" [("name", name)] [get ()]]);
 
 
-(* Processing PGIP commands from the interface *)
+(* processing PGIP commands from the interface *)
 
-(* FIXME: matching on attributes is a bit too strict here *)
+(*FIXME: matching on attributes is a bit too strict here*)
 
 fun process_pgip_element pgip = (case pgip of
       XML.Elem ("askpgml", _, []) => usespgml ()
@@ -397,10 +395,6 @@
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
-val old_undoP = (*same name for compatibility with PG/Isabelle99*)
-  OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
-
 val undoP =
   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
@@ -433,7 +427,7 @@
       (fn name => Toplevel.imperative (fn () => inform_file_retracted name))));
 
 fun init_outer_syntax () = OuterSyntax.add_parsers
- [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
+ [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
   inform_file_processedP, inform_file_retractedP];
 
 end;
@@ -484,7 +478,7 @@
   \;; $" ^ "Id$\n\
   \;;\n" ^
   defconst "major" (map #1 commands) ^
-  defconst "minor" (filter Syntax.is_identifier keywords) ^
+  defconst "minor" (filter Syntax.is_ascii_identifier keywords) ^
   implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
   "\n(provide 'isar-keywords)\n";