# HG changeset patch # User wenzelm # Date 1368295824 -7200 # Node ID a60c6c90a4478551f975e4267a56c02d7d439e13 # Parent f196352201d678c9cb115a713bf3ec1b195a2d41 removed redundant modules; diff -r f196352201d6 -r a60c6c90a447 src/Pure/ProofGeneral/pgip.ML --- 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 diff -r f196352201d6 -r a60c6c90a447 src/Pure/ProofGeneral/pgip_tests.ML --- 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 ""); -val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1")) (XML.parse ""); -val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)])) - (XML.parse ""); - -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 ""); -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 "" (SOME (Askpgip())); -val _ = asseqi "" (SOME (Askpgml())); -val _ = asseqi "" (SOME (Askconfig())); -(* FIXME: new tests: -val _ = asseqi "" (SOME (Pgmlsymbolson())); -val _ = asseqi "" (SOME (Pgmlsymbolsoff())); -val _ = asseqi "" (SOME (Startquiet())); -val _ = asseqi "" (SOME (Stopquiet())); -*) -val _ = asseqi "" (SOME (Askrefs {url=NONE, thyname=SOME "foo", - objtype=SOME ObjTheory,name=NONE})); -val _ = asseqi "" 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 diff -r f196352201d6 -r a60c6c90a447 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 " not implemented by Isabelle" - | Pgip.Restoregoal _ => error " 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 " not implemented by Isabelle" + | PgipInput.Restoregoal _ => error " 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 *) diff -r f196352201d6 -r a60c6c90a447 src/Pure/ROOT --- 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" diff -r f196352201d6 -r a60c6c90a447 src/Pure/ROOT.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 *)