removed redundant modules;
authorwenzelm
Sat May 11 20:10:24 2013 +0200 (2013-05-11)
changeset 51933a60c6c90a447
parent 51932 f196352201d6
child 51934 203a9528bf7a
removed redundant modules;
src/Pure/ProofGeneral/pgip.ML
src/Pure/ProofGeneral/pgip_tests.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ProofGeneral/pgip.ML	Sat May 11 18:45:38 2013 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,22 +0,0 @@
     1.4 -(*  Title:      Pure/ProofGeneral/pgip.ML
     1.5 -    Author:     David Aspinall
     1.6 -
     1.7 -Prover-side PGIP abstraction.  
     1.8 -Not too closely tied to Isabelle, to help with reuse/porting.
     1.9 -*)
    1.10 -
    1.11 -signature PGIP =
    1.12 -sig
    1.13 -    include PGIPTYPES
    1.14 -    include PGIPMARKUP
    1.15 -    include PGIPINPUT
    1.16 -    include PGIPOUTPUT
    1.17 -end
    1.18 -
    1.19 -structure Pgip : PGIP = 
    1.20 -struct
    1.21 -   open PgipTypes
    1.22 -   open PgipMarkup
    1.23 -   open PgipInput
    1.24 -   open PgipOutput
    1.25 -end
     2.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML	Sat May 11 18:45:38 2013 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,129 +0,0 @@
     2.4 -(*  Title:      Pure/ProofGeneral/pgip_tests.ML
     2.5 -    Author:     David Aspinall
     2.6 -
     2.7 -A test suite for the PGIP abstraction code (in progress).
     2.8 -Run to provide some mild insurance against breakage in Isabelle here.
     2.9 -*)
    2.10 -
    2.11 -(** pgip_types.ML **)
    2.12 -
    2.13 -local
    2.14 -fun asseq_p toS a b =
    2.15 -    if a=b then ()
    2.16 -    else error("PGIP test: expected these two values to be equal:\n" ^
    2.17 -               (toS a) ^"\n and: \n" ^ (toS b))
    2.18 -
    2.19 -val asseqx = asseq_p XML.string_of
    2.20 -val asseqs = asseq_p I
    2.21 -val asseqb = asseq_p (fn b=>if b then "true" else "false")
    2.22 -
    2.23 -open PgipTypes;
    2.24 -in
    2.25 -
    2.26 -val _ = asseqx (pgiptype_to_xml Pgipnull) (XML.parse "<pgipnull/>");
    2.27 -val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse "<pgipbool/>");
    2.28 -val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse "<pgipint/>");
    2.29 -val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse "<pgipint min='5' max='7'/>");
    2.30 -val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse "<pgipint max='7'/>");
    2.31 -val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse "<pgipint min='-5'/>");
    2.32 -val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse "<pgipstring/>");
    2.33 -val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1"))  (XML.parse "<pgipconst name='radio1'/>");
    2.34 -val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
    2.35 -       (XML.parse "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
    2.36 -
    2.37 -val _ = asseqs (pgval_to_string (read_pgval Pgipbool "true")) "true";
    2.38 -val _ = asseqs (pgval_to_string (read_pgval Pgipbool "false")) "false";
    2.39 -val _ = asseqs (pgval_to_string (read_pgval (Pgipint(NONE,NONE)) "-37")) "-37";
    2.40 -val _ = asseqs (pgval_to_string (read_pgval Pgipnat "45")) "45";
    2.41 -val _ = asseqs (pgval_to_string (read_pgval Pgipstring "stringvalue")) "stringvalue";
    2.42 -
    2.43 -local
    2.44 -    val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat), 
    2.45 -                              Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
    2.46 -in
    2.47 -val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45";
    2.48 -val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo";
    2.49 -val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true";
    2.50 -val _ = asseqs (pgval_to_string (read_pgval choices "")) "";
    2.51 -val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37"; 
    2.52 -         error "pgip_tests: should fail") handle PGIP _ => ()
    2.53 -end
    2.54 -
    2.55 -val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
    2.56 -                 default=SOME "true", pgiptype=Pgipbool})
    2.57 -       (XML.parse "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
    2.58 -end
    2.59 -
    2.60 -
    2.61 -(** pgip_input.ML **)
    2.62 -local
    2.63 -
    2.64 -fun e str = case XML.parse str of 
    2.65 -                (XML.Elem args) => args
    2.66 -              | _ => error("Expected to get an XML Element")
    2.67 -
    2.68 -open PgipInput;
    2.69 -open PgipTypes;
    2.70 -open PgipIsabelle;
    2.71 -
    2.72 -fun asseqi a b =
    2.73 -    if input (e a) = b then ()
    2.74 -    else error("PGIP test: expected two inputs to be equal, for input:\n" ^ a)
    2.75 -
    2.76 -in
    2.77 -
    2.78 -val _ = asseqi "<askpgip/>" (SOME (Askpgip()));
    2.79 -val _ = asseqi "<askpgml/>" (SOME (Askpgml()));
    2.80 -val _ = asseqi "<askconfig/>" (SOME (Askconfig()));
    2.81 -(* FIXME: new tests:
    2.82 -val _ = asseqi "<pgmlsymbolson/>" (SOME (Pgmlsymbolson()));
    2.83 -val _ = asseqi "<pgmlsymbolsoff/>" (SOME (Pgmlsymbolsoff()));
    2.84 -val _ = asseqi "<startquiet/>" (SOME (Startquiet()));
    2.85 -val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
    2.86 -*)
    2.87 -val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
    2.88 -                                                                          objtype=SOME ObjTheory,name=NONE}));
    2.89 -val _ = asseqi "<otherelt/>" NONE;
    2.90 -
    2.91 -end
    2.92 -
    2.93 -(** pgip_markup.ML **)
    2.94 -local
    2.95 -open PgipMarkup
    2.96 -in
    2.97 -val _ = ()
    2.98 -end
    2.99 -
   2.100 -
   2.101 -(** pgip_output.ML **)
   2.102 -local
   2.103 -open PgipOutput
   2.104 -in
   2.105 -val _ = ()
   2.106 -end
   2.107 -
   2.108 -
   2.109 -(** pgip_parser.ML **)
   2.110 -local
   2.111 -open PgipMarkup
   2.112 -open PgipParser
   2.113 -open PgipIsabelle
   2.114 -
   2.115 -fun asseqp a b =
   2.116 -    if pgip_parser Position.none a = b then ()
   2.117 -    else error("PGIP test: expected two parses to be equal, for input:\n" ^ a)
   2.118 -
   2.119 -in
   2.120 -val _ = 
   2.121 -    asseqp "theory A imports Bthy Cthy Dthy begin"
   2.122 -    [Opentheory
   2.123 -         {text = "theory A imports Bthy Cthy Dthy begin",
   2.124 -          thyname = SOME "A",
   2.125 -          parentnames = ["Bthy", "Cthy", "Dthy"]},
   2.126 -     Openblock {metavarid=NONE,name=NONE,objtype=SOME ObjTheoryBody}];
   2.127 -
   2.128 -val _ = 
   2.129 -    asseqp "end" 
   2.130 -   [Closeblock {}, Closetheory {text = "end"}];
   2.131 -
   2.132 -end
     3.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 11 18:45:38 2013 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 11 20:10:24 2013 +0200
     3.3 @@ -26,7 +26,10 @@
     3.4  structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
     3.5  struct
     3.6  
     3.7 -open Pgip;
     3.8 +open PgipTypes;
     3.9 +open PgipMarkup;
    3.10 +open PgipInput;
    3.11 +open PgipOutput;
    3.12  
    3.13  
    3.14  (** print mode **)
    3.15 @@ -845,50 +848,50 @@
    3.16  fun quitpgip _ = raise PGIP_QUIT
    3.17  
    3.18  fun process_input inp = case inp
    3.19 - of Pgip.Askpgip _          => askpgip inp
    3.20 -  | Pgip.Askpgml _          => askpgml inp
    3.21 -  | Pgip.Askprefs _         => askprefs inp
    3.22 -  | Pgip.Askconfig _        => askconfig inp
    3.23 -  | Pgip.Getpref _          => getpref inp
    3.24 -  | Pgip.Setpref _          => setpref inp
    3.25 -  | Pgip.Proverinit _       => proverinit inp
    3.26 -  | Pgip.Proverexit _       => proverexit inp
    3.27 -  | Pgip.Setproverflag _    => setproverflag inp
    3.28 -  | Pgip.Dostep _           => dostep inp
    3.29 -  | Pgip.Undostep _         => undostep inp
    3.30 -  | Pgip.Redostep _         => redostep inp
    3.31 -  | Pgip.Forget _           => error "<forget> not implemented by Isabelle"
    3.32 -  | Pgip.Restoregoal _      => error "<restoregoal> not implemented by Isabelle"
    3.33 -  | Pgip.Abortgoal _        => abortgoal inp
    3.34 -  | Pgip.Askids _           => askids inp
    3.35 -  | Pgip.Askrefs _          => askrefs inp
    3.36 -  | Pgip.Showid _           => showid inp
    3.37 -  | Pgip.Askguise _         => askguise inp
    3.38 -  | Pgip.Parsescript _      => parsescript inp
    3.39 -  | Pgip.Showproofstate _   => showproofstate inp
    3.40 -  | Pgip.Showctxt _         => showctxt inp
    3.41 -  | Pgip.Searchtheorems _   => searchtheorems inp
    3.42 -  | Pgip.Setlinewidth _     => setlinewidth inp
    3.43 -  | Pgip.Viewdoc _          => viewdoc inp
    3.44 -  | Pgip.Doitem _           => doitem inp
    3.45 -  | Pgip.Undoitem _         => undoitem inp
    3.46 -  | Pgip.Redoitem _         => redoitem inp
    3.47 -  | Pgip.Aborttheory _      => aborttheory inp
    3.48 -  | Pgip.Retracttheory _    => retracttheory inp
    3.49 -  | Pgip.Loadfile _         => loadfile inp
    3.50 -  | Pgip.Openfile _         => openfile inp
    3.51 -  | Pgip.Closefile _        => closefile inp
    3.52 -  | Pgip.Abortfile _        => abortfile inp
    3.53 -  | Pgip.Retractfile _      => retractfile inp
    3.54 -  | Pgip.Changecwd _        => changecwd inp
    3.55 -  | Pgip.Systemcmd _        => systemcmd inp
    3.56 -  | Pgip.Quitpgip _         => quitpgip inp
    3.57 + of PgipInput.Askpgip _          => askpgip inp
    3.58 +  | PgipInput.Askpgml _          => askpgml inp
    3.59 +  | PgipInput.Askprefs _         => askprefs inp
    3.60 +  | PgipInput.Askconfig _        => askconfig inp
    3.61 +  | PgipInput.Getpref _          => getpref inp
    3.62 +  | PgipInput.Setpref _          => setpref inp
    3.63 +  | PgipInput.Proverinit _       => proverinit inp
    3.64 +  | PgipInput.Proverexit _       => proverexit inp
    3.65 +  | PgipInput.Setproverflag _    => setproverflag inp
    3.66 +  | PgipInput.Dostep _           => dostep inp
    3.67 +  | PgipInput.Undostep _         => undostep inp
    3.68 +  | PgipInput.Redostep _         => redostep inp
    3.69 +  | PgipInput.Forget _           => error "<forget> not implemented by Isabelle"
    3.70 +  | PgipInput.Restoregoal _      => error "<restoregoal> not implemented by Isabelle"
    3.71 +  | PgipInput.Abortgoal _        => abortgoal inp
    3.72 +  | PgipInput.Askids _           => askids inp
    3.73 +  | PgipInput.Askrefs _          => askrefs inp
    3.74 +  | PgipInput.Showid _           => showid inp
    3.75 +  | PgipInput.Askguise _         => askguise inp
    3.76 +  | PgipInput.Parsescript _      => parsescript inp
    3.77 +  | PgipInput.Showproofstate _   => showproofstate inp
    3.78 +  | PgipInput.Showctxt _         => showctxt inp
    3.79 +  | PgipInput.Searchtheorems _   => searchtheorems inp
    3.80 +  | PgipInput.Setlinewidth _     => setlinewidth inp
    3.81 +  | PgipInput.Viewdoc _          => viewdoc inp
    3.82 +  | PgipInput.Doitem _           => doitem inp
    3.83 +  | PgipInput.Undoitem _         => undoitem inp
    3.84 +  | PgipInput.Redoitem _         => redoitem inp
    3.85 +  | PgipInput.Aborttheory _      => aborttheory inp
    3.86 +  | PgipInput.Retracttheory _    => retracttheory inp
    3.87 +  | PgipInput.Loadfile _         => loadfile inp
    3.88 +  | PgipInput.Openfile _         => openfile inp
    3.89 +  | PgipInput.Closefile _        => closefile inp
    3.90 +  | PgipInput.Abortfile _        => abortfile inp
    3.91 +  | PgipInput.Retractfile _      => retractfile inp
    3.92 +  | PgipInput.Changecwd _        => changecwd inp
    3.93 +  | PgipInput.Systemcmd _        => systemcmd inp
    3.94 +  | PgipInput.Quitpgip _         => quitpgip inp
    3.95  
    3.96  
    3.97  fun process_pgip_element pgipxml =
    3.98      case pgipxml of
    3.99          xml as (XML.Elem elem) =>
   3.100 -        (case Pgip.input elem of
   3.101 +        (case PgipInput.input elem of
   3.102               NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
   3.103                                (XML.string_of xml))
   3.104             | SOME inp => (process_input inp)) (* errors later; packet discarded *)
     4.1 --- a/src/Pure/ROOT	Sat May 11 18:45:38 2013 +0200
     4.2 +++ b/src/Pure/ROOT	Sat May 11 20:10:24 2013 +0200
     4.3 @@ -160,13 +160,11 @@
     4.4      "Proof/proof_rewrite_rules.ML"
     4.5      "Proof/proof_syntax.ML"
     4.6      "Proof/reconstruct.ML"
     4.7 -    "ProofGeneral/pgip.ML"
     4.8      "ProofGeneral/pgip_input.ML"
     4.9      "ProofGeneral/pgip_isabelle.ML"
    4.10      "ProofGeneral/pgip_markup.ML"
    4.11      "ProofGeneral/pgip_output.ML"
    4.12      "ProofGeneral/pgip_parser.ML"
    4.13 -    "ProofGeneral/pgip_tests.ML"
    4.14      "ProofGeneral/pgip_types.ML"
    4.15      "ProofGeneral/pgml.ML"
    4.16      "ProofGeneral/preferences.ML"
     5.1 --- a/src/Pure/ROOT.ML	Sat May 11 18:45:38 2013 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Sat May 11 20:10:24 2013 +0200
     5.3 @@ -302,7 +302,6 @@
     5.4  use "ProofGeneral/pgip_markup.ML";
     5.5  use "ProofGeneral/pgip_input.ML";
     5.6  use "ProofGeneral/pgip_output.ML";
     5.7 -use "ProofGeneral/pgip.ML";
     5.8  
     5.9  use "ProofGeneral/pgip_isabelle.ML";
    5.10  
    5.11 @@ -348,8 +347,6 @@
    5.12  
    5.13  toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
    5.14  
    5.15 -use "ProofGeneral/pgip_tests.ML";
    5.16 -
    5.17  
    5.18  (* ML toplevel commands *)
    5.19