--- a/src/Pure/ProofGeneral/pgip_tests.ML Sat Dec 16 20:27:56 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_tests.ML Sun Dec 17 22:43:50 2006 +0100
@@ -82,6 +82,14 @@
end
+(** pgip_markup.ML **)
+local
+open PgipMarkup
+in
+val _ = ()
+end
+
+
(** pgip_output.ML **)
local
open PgipOutput
@@ -89,3 +97,25 @@
val _ = ()
end
+
+(** parsing.ML **)
+local
+open PgipMarkup
+open PgipParser
+fun asseqp a b =
+ if (pgip_parser 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 = "A",
+ parentnames = ["Bthy", "Cthy", "Dthy"]}];
+
+val _ =
+ asseqp "end"
+ [Closetheory {text = "end"}];
+
+end