--- a/src/Pure/ProofGeneral/pgip.ML Sat May 11 18:45:38 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: Pure/ProofGeneral/pgip.ML
- Author: David Aspinall
-
-Prover-side PGIP abstraction.
-Not too closely tied to Isabelle, to help with reuse/porting.
-*)
-
-signature PGIP =
-sig
- include PGIPTYPES
- include PGIPMARKUP
- include PGIPINPUT
- include PGIPOUTPUT
-end
-
-structure Pgip : PGIP =
-struct
- open PgipTypes
- open PgipMarkup
- open PgipInput
- open PgipOutput
-end
--- a/src/Pure/ProofGeneral/pgip_tests.ML Sat May 11 18:45:38 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-(* Title: Pure/ProofGeneral/pgip_tests.ML
- Author: David Aspinall
-
-A test suite for the PGIP abstraction code (in progress).
-Run to provide some mild insurance against breakage in Isabelle here.
-*)
-
-(** pgip_types.ML **)
-
-local
-fun asseq_p toS a b =
- if a=b then ()
- else error("PGIP test: expected these two values to be equal:\n" ^
- (toS a) ^"\n and: \n" ^ (toS b))
-
-val asseqx = asseq_p XML.string_of
-val asseqs = asseq_p I
-val asseqb = asseq_p (fn b=>if b then "true" else "false")
-
-open PgipTypes;
-in
-
-val _ = asseqx (pgiptype_to_xml Pgipnull) (XML.parse "<pgipnull/>");
-val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse "<pgipbool/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse "<pgipint/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse "<pgipint min='5' max='7'/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse "<pgipint max='7'/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse "<pgipint min='-5'/>");
-val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse "<pgipstring/>");
-val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1")) (XML.parse "<pgipconst name='radio1'/>");
-val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
- (XML.parse "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
-
-val _ = asseqs (pgval_to_string (read_pgval Pgipbool "true")) "true";
-val _ = asseqs (pgval_to_string (read_pgval Pgipbool "false")) "false";
-val _ = asseqs (pgval_to_string (read_pgval (Pgipint(NONE,NONE)) "-37")) "-37";
-val _ = asseqs (pgval_to_string (read_pgval Pgipnat "45")) "45";
-val _ = asseqs (pgval_to_string (read_pgval Pgipstring "stringvalue")) "stringvalue";
-
-local
- val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat),
- Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
-in
-val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45";
-val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo";
-val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true";
-val _ = asseqs (pgval_to_string (read_pgval choices "")) "";
-val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37";
- error "pgip_tests: should fail") handle PGIP _ => ()
-end
-
-val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
- default=SOME "true", pgiptype=Pgipbool})
- (XML.parse "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
-end
-
-
-(** pgip_input.ML **)
-local
-
-fun e str = case XML.parse str of
- (XML.Elem args) => args
- | _ => error("Expected to get an XML Element")
-
-open PgipInput;
-open PgipTypes;
-open PgipIsabelle;
-
-fun asseqi a b =
- if input (e a) = b then ()
- else error("PGIP test: expected two inputs to be equal, for input:\n" ^ a)
-
-in
-
-val _ = asseqi "<askpgip/>" (SOME (Askpgip()));
-val _ = asseqi "<askpgml/>" (SOME (Askpgml()));
-val _ = asseqi "<askconfig/>" (SOME (Askconfig()));
-(* FIXME: new tests:
-val _ = asseqi "<pgmlsymbolson/>" (SOME (Pgmlsymbolson()));
-val _ = asseqi "<pgmlsymbolsoff/>" (SOME (Pgmlsymbolsoff()));
-val _ = asseqi "<startquiet/>" (SOME (Startquiet()));
-val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
-*)
-val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
- objtype=SOME ObjTheory,name=NONE}));
-val _ = asseqi "<otherelt/>" NONE;
-
-end
-
-(** pgip_markup.ML **)
-local
-open PgipMarkup
-in
-val _ = ()
-end
-
-
-(** pgip_output.ML **)
-local
-open PgipOutput
-in
-val _ = ()
-end
-
-
-(** pgip_parser.ML **)
-local
-open PgipMarkup
-open PgipParser
-open PgipIsabelle
-
-fun asseqp a b =
- if pgip_parser Position.none a = b then ()
- else error("PGIP test: expected two parses to be equal, for input:\n" ^ a)
-
-in
-val _ =
- asseqp "theory A imports Bthy Cthy Dthy begin"
- [Opentheory
- {text = "theory A imports Bthy Cthy Dthy begin",
- thyname = SOME "A",
- parentnames = ["Bthy", "Cthy", "Dthy"]},
- Openblock {metavarid=NONE,name=NONE,objtype=SOME ObjTheoryBody}];
-
-val _ =
- asseqp "end"
- [Closeblock {}, Closetheory {text = "end"}];
-
-end
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat May 11 18:45:38 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat May 11 20:10:24 2013 +0200
@@ -26,7 +26,10 @@
structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
struct
-open Pgip;
+open PgipTypes;
+open PgipMarkup;
+open PgipInput;
+open PgipOutput;
(** print mode **)
@@ -845,50 +848,50 @@
fun quitpgip _ = raise PGIP_QUIT
fun process_input inp = case inp
- of Pgip.Askpgip _ => askpgip inp
- | Pgip.Askpgml _ => askpgml inp
- | Pgip.Askprefs _ => askprefs inp
- | Pgip.Askconfig _ => askconfig inp
- | Pgip.Getpref _ => getpref inp
- | Pgip.Setpref _ => setpref inp
- | Pgip.Proverinit _ => proverinit inp
- | Pgip.Proverexit _ => proverexit inp
- | Pgip.Setproverflag _ => setproverflag inp
- | Pgip.Dostep _ => dostep inp
- | Pgip.Undostep _ => undostep inp
- | Pgip.Redostep _ => redostep inp
- | Pgip.Forget _ => error "<forget> not implemented by Isabelle"
- | Pgip.Restoregoal _ => error "<restoregoal> not implemented by Isabelle"
- | Pgip.Abortgoal _ => abortgoal inp
- | Pgip.Askids _ => askids inp
- | Pgip.Askrefs _ => askrefs inp
- | Pgip.Showid _ => showid inp
- | Pgip.Askguise _ => askguise inp
- | Pgip.Parsescript _ => parsescript inp
- | Pgip.Showproofstate _ => showproofstate inp
- | Pgip.Showctxt _ => showctxt inp
- | Pgip.Searchtheorems _ => searchtheorems inp
- | Pgip.Setlinewidth _ => setlinewidth inp
- | Pgip.Viewdoc _ => viewdoc inp
- | Pgip.Doitem _ => doitem inp
- | Pgip.Undoitem _ => undoitem inp
- | Pgip.Redoitem _ => redoitem inp
- | Pgip.Aborttheory _ => aborttheory inp
- | Pgip.Retracttheory _ => retracttheory inp
- | Pgip.Loadfile _ => loadfile inp
- | Pgip.Openfile _ => openfile inp
- | Pgip.Closefile _ => closefile inp
- | Pgip.Abortfile _ => abortfile inp
- | Pgip.Retractfile _ => retractfile inp
- | Pgip.Changecwd _ => changecwd inp
- | Pgip.Systemcmd _ => systemcmd inp
- | Pgip.Quitpgip _ => quitpgip inp
+ of PgipInput.Askpgip _ => askpgip inp
+ | PgipInput.Askpgml _ => askpgml inp
+ | PgipInput.Askprefs _ => askprefs inp
+ | PgipInput.Askconfig _ => askconfig inp
+ | PgipInput.Getpref _ => getpref inp
+ | PgipInput.Setpref _ => setpref inp
+ | PgipInput.Proverinit _ => proverinit inp
+ | PgipInput.Proverexit _ => proverexit inp
+ | PgipInput.Setproverflag _ => setproverflag inp
+ | PgipInput.Dostep _ => dostep inp
+ | PgipInput.Undostep _ => undostep inp
+ | PgipInput.Redostep _ => redostep inp
+ | PgipInput.Forget _ => error "<forget> not implemented by Isabelle"
+ | PgipInput.Restoregoal _ => error "<restoregoal> not implemented by Isabelle"
+ | PgipInput.Abortgoal _ => abortgoal inp
+ | PgipInput.Askids _ => askids inp
+ | PgipInput.Askrefs _ => askrefs inp
+ | PgipInput.Showid _ => showid inp
+ | PgipInput.Askguise _ => askguise inp
+ | PgipInput.Parsescript _ => parsescript inp
+ | PgipInput.Showproofstate _ => showproofstate inp
+ | PgipInput.Showctxt _ => showctxt inp
+ | PgipInput.Searchtheorems _ => searchtheorems inp
+ | PgipInput.Setlinewidth _ => setlinewidth inp
+ | PgipInput.Viewdoc _ => viewdoc inp
+ | PgipInput.Doitem _ => doitem inp
+ | PgipInput.Undoitem _ => undoitem inp
+ | PgipInput.Redoitem _ => redoitem inp
+ | PgipInput.Aborttheory _ => aborttheory inp
+ | PgipInput.Retracttheory _ => retracttheory inp
+ | PgipInput.Loadfile _ => loadfile inp
+ | PgipInput.Openfile _ => openfile inp
+ | PgipInput.Closefile _ => closefile inp
+ | PgipInput.Abortfile _ => abortfile inp
+ | PgipInput.Retractfile _ => retractfile inp
+ | PgipInput.Changecwd _ => changecwd inp
+ | PgipInput.Systemcmd _ => systemcmd inp
+ | PgipInput.Quitpgip _ => quitpgip inp
fun process_pgip_element pgipxml =
case pgipxml of
xml as (XML.Elem elem) =>
- (case Pgip.input elem of
+ (case PgipInput.input elem of
NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
(XML.string_of xml))
| SOME inp => (process_input inp)) (* errors later; packet discarded *)
--- a/src/Pure/ROOT Sat May 11 18:45:38 2013 +0200
+++ b/src/Pure/ROOT Sat May 11 20:10:24 2013 +0200
@@ -160,13 +160,11 @@
"Proof/proof_rewrite_rules.ML"
"Proof/proof_syntax.ML"
"Proof/reconstruct.ML"
- "ProofGeneral/pgip.ML"
"ProofGeneral/pgip_input.ML"
"ProofGeneral/pgip_isabelle.ML"
"ProofGeneral/pgip_markup.ML"
"ProofGeneral/pgip_output.ML"
"ProofGeneral/pgip_parser.ML"
- "ProofGeneral/pgip_tests.ML"
"ProofGeneral/pgip_types.ML"
"ProofGeneral/pgml.ML"
"ProofGeneral/preferences.ML"
--- a/src/Pure/ROOT.ML Sat May 11 18:45:38 2013 +0200
+++ b/src/Pure/ROOT.ML Sat May 11 20:10:24 2013 +0200
@@ -302,7 +302,6 @@
use "ProofGeneral/pgip_markup.ML";
use "ProofGeneral/pgip_input.ML";
use "ProofGeneral/pgip_output.ML";
-use "ProofGeneral/pgip.ML";
use "ProofGeneral/pgip_isabelle.ML";
@@ -348,8 +347,6 @@
toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
-use "ProofGeneral/pgip_tests.ML";
-
(* ML toplevel commands *)