--- 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";