PGIP change: thyname is optional in opentheory, markup even in case of header parse failure
authoraspinall
Thu Aug 09 11:39:29 2007 +0200 (2007-08-09)
changeset 241924eccd4bb8b64
parent 24191 333f0a4bcc55
child 24193 926dde4d96de
PGIP change: thyname is optional in opentheory, markup even in case of header parse failure
src/Pure/ProofGeneral/parsing.ML
src/Pure/ProofGeneral/pgip_markup.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/ProofGeneral/pgip_tests.ML
     1.1 --- a/src/Pure/ProofGeneral/parsing.ML	Thu Aug 09 11:37:27 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/parsing.ML	Thu Aug 09 11:39:29 2007 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4          let
     1.5              val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
     1.6          in
     1.7 -            [D.Opentheory { thyname=thyname, 
     1.8 +            [D.Opentheory { thyname=SOME thyname, 
     1.9  			    parentnames = imports,
    1.10  			    text = str },
    1.11  	     D.Openblock { metavarid=NONE,name=NONE,objtype=SOME I.ObjTheoryBody }]
     2.1 --- a/src/Pure/ProofGeneral/pgip_markup.ML	Thu Aug 09 11:37:27 2007 +0200
     2.2 +++ b/src/Pure/ProofGeneral/pgip_markup.ML	Thu Aug 09 11:39:29 2007 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4      Openblock     of { metavarid: string option, name: string option,
     2.5                         objtype: PgipTypes.objtype option }
     2.6    | Closeblock    of { }
     2.7 -  | Opentheory    of { thyname: string, parentnames: string list , text: string}
     2.8 +  | Opentheory    of { thyname: string option, parentnames: string list , text: string}
     2.9    | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
    2.10    | Closetheory   of { text: string }
    2.11    | Opengoal      of { thmname: string option, text: string }
    2.12 @@ -50,7 +50,7 @@
    2.13      Openblock     of { metavarid: string option, name: string option,
    2.14                         objtype: PgipTypes.objtype option }
    2.15    | Closeblock    of { }
    2.16 -  | Opentheory    of { thyname: string, parentnames: string list, text: string}
    2.17 +  | Opentheory    of { thyname: string option, parentnames: string list, text: string}
    2.18    | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
    2.19    | Closetheory   of { text: string }
    2.20    | Opengoal      of { thmname: string option, text: string }
    2.21 @@ -86,7 +86,7 @@
    2.22  
    2.23           | Opentheory vs  =>
    2.24             XML.Elem("opentheory",
    2.25 -                    attr "thyname" (#thyname vs) @
    2.26 +                    opt_attr "thyname" (#thyname vs) @
    2.27                      opt_attr "parentnames"
    2.28                               (case (#parentnames vs)
    2.29                                 of [] => NONE
     3.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Thu Aug 09 11:37:27 2007 +0200
     3.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu Aug 09 11:39:29 2007 +0200
     3.3 @@ -22,10 +22,10 @@
     3.4  
     3.5  fun thy_begin text =
     3.6    (case try (ThyHeader.read Position.none) (Source.of_string text) of
     3.7 -    NONE => [D.Unparseable {text = text}]
     3.8 +    NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
     3.9    | SOME (name, imports, _) =>
    3.10 -      [D.Opentheory {thyname = name, parentnames = imports, text = text},
    3.11 -       D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}]);
    3.12 +       D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
    3.13 +  :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    3.14  
    3.15  fun thy_heading text =
    3.16    [D.Closeblock {},
     4.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML	Thu Aug 09 11:37:27 2007 +0200
     4.2 +++ b/src/Pure/ProofGeneral/pgip_tests.ML	Thu Aug 09 11:39:29 2007 +0200
     4.3 @@ -123,7 +123,7 @@
     4.4      asseqp "theory A imports Bthy Cthy Dthy begin"
     4.5      [Opentheory
     4.6           {text = "theory A imports Bthy Cthy Dthy begin",
     4.7 -          thyname = "A",
     4.8 +          thyname = SOME "A",
     4.9            parentnames = ["Bthy", "Cthy", "Dthy"]},
    4.10       Openblock {metavarid=NONE,name=NONE,objtype=SOME ObjTheoryBody}];
    4.11