# HG changeset patch
# User aspinall
# Date 1186652369 -7200
# Node ID 4eccd4bb8b64ccd42de55b74a222703d71919422
# Parent  333f0a4bcc55319f748a2d83b8954f69de9d8973
PGIP change: thyname is optional in opentheory, markup even in case of header parse failure

diff -r 333f0a4bcc55 -r 4eccd4bb8b64 src/Pure/ProofGeneral/parsing.ML
--- a/src/Pure/ProofGeneral/parsing.ML	Thu Aug 09 11:37:27 2007 +0200
+++ b/src/Pure/ProofGeneral/parsing.ML	Thu Aug 09 11:39:29 2007 +0200
@@ -96,7 +96,7 @@
         let
             val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
         in
-            [D.Opentheory { thyname=thyname, 
+            [D.Opentheory { thyname=SOME thyname, 
 			    parentnames = imports,
 			    text = str },
 	     D.Openblock { metavarid=NONE,name=NONE,objtype=SOME I.ObjTheoryBody }]
diff -r 333f0a4bcc55 -r 4eccd4bb8b64 src/Pure/ProofGeneral/pgip_markup.ML
--- a/src/Pure/ProofGeneral/pgip_markup.ML	Thu Aug 09 11:37:27 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_markup.ML	Thu Aug 09 11:39:29 2007 +0200
@@ -12,7 +12,7 @@
     Openblock     of { metavarid: string option, name: string option,
                        objtype: PgipTypes.objtype option }
   | Closeblock    of { }
-  | Opentheory    of { thyname: string, parentnames: string list , text: string}
+  | Opentheory    of { thyname: string option, parentnames: string list , text: string}
   | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
   | Closetheory   of { text: string }
   | Opengoal      of { thmname: string option, text: string }
@@ -50,7 +50,7 @@
     Openblock     of { metavarid: string option, name: string option,
                        objtype: PgipTypes.objtype option }
   | Closeblock    of { }
-  | Opentheory    of { thyname: string, parentnames: string list, text: string}
+  | Opentheory    of { thyname: string option, parentnames: string list, text: string}
   | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
   | Closetheory   of { text: string }
   | Opengoal      of { thmname: string option, text: string }
@@ -86,7 +86,7 @@
 
          | Opentheory vs  =>
            XML.Elem("opentheory",
-                    attr "thyname" (#thyname vs) @
+                    opt_attr "thyname" (#thyname vs) @
                     opt_attr "parentnames"
                              (case (#parentnames vs)
                                of [] => NONE
diff -r 333f0a4bcc55 -r 4eccd4bb8b64 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Thu Aug 09 11:37:27 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu Aug 09 11:39:29 2007 +0200
@@ -22,10 +22,10 @@
 
 fun thy_begin text =
   (case try (ThyHeader.read Position.none) (Source.of_string text) of
-    NONE => [D.Unparseable {text = text}]
+    NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
   | SOME (name, imports, _) =>
-      [D.Opentheory {thyname = name, parentnames = imports, text = text},
-       D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}]);
+       D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
+  :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
 
 fun thy_heading text =
   [D.Closeblock {},
diff -r 333f0a4bcc55 -r 4eccd4bb8b64 src/Pure/ProofGeneral/pgip_tests.ML
--- a/src/Pure/ProofGeneral/pgip_tests.ML	Thu Aug 09 11:37:27 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_tests.ML	Thu Aug 09 11:39:29 2007 +0200
@@ -123,7 +123,7 @@
     asseqp "theory A imports Bthy Cthy Dthy begin"
     [Opentheory
          {text = "theory A imports Bthy Cthy Dthy begin",
-          thyname = "A",
+          thyname = SOME "A",
           parentnames = ["Bthy", "Cthy", "Dthy"]},
      Openblock {metavarid=NONE,name=NONE,objtype=SOME ObjTheoryBody}];