src/Pure/ProofGeneral/pgip_markup.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 26548 41bbcaf3e481
child 29606 fedb8be05f24
permissions -rw-r--r--
map_const: soft version, no failure here;
     1 (*  Title:      Pure/ProofGeneral/pgip_markup.ML
     2     ID:         $Id$
     3     Author:     David Aspinall
     4 
     5 PGIP abstraction: document markup for proof scripts (in progress).
     6 *)
     7 
     8 signature PGIPMARKUP =
     9 sig
    10   (* Generic markup on sequential, non-overlapping pieces of proof text *)
    11   datatype pgipdoc =
    12     Openblock     of { metavarid: string option, name: string option,
    13                        objtype: PgipTypes.objtype option }
    14   | Closeblock    of { }
    15   | Opentheory    of { thyname: string option, parentnames: string list , text: string}
    16   | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
    17   | Closetheory   of { text: string }
    18   | Opengoal      of { thmname: string option, text: string }
    19   | Proofstep     of { text: string }
    20   | Closegoal     of { text: string }
    21   | Giveupgoal    of { text: string }
    22   | Postponegoal  of { text: string }
    23   | Comment       of { text: string }
    24   | Doccomment    of { text: string }
    25   | Whitespace    of { text: string }
    26   | Spuriouscmd   of { text: string }
    27   | Badcmd        of { text: string }
    28   | Unparseable   of { text: string }
    29   | Metainfo      of { name: string option, text: string }
    30   (* Last three for PGIP literate markup only: *)
    31   | Litcomment    of { format: string option, content: XML.tree list }
    32   | Showcode      of { show: bool }
    33   | Setformat     of { format: string }
    34 
    35   type pgipdocument = pgipdoc list
    36   type pgip_parser  = string -> pgipdocument       (* system must provide a parser P *)
    37   val unparse_doc : pgipdocument -> string list    (* s.t. unparse (P x) = x         *)
    38   val output_doc : pgipdocument -> XML.tree list
    39   val doc_markup_elements : string list            (* used in pgip_input *)
    40   val doc_markup_elements_ignored : string list    (* used in pgip_input *)
    41 end
    42 
    43 
    44 structure PgipMarkup : PGIPMARKUP =
    45 struct
    46    open PgipTypes
    47 
    48 (* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *)
    49   datatype pgipdoc =
    50     Openblock     of { metavarid: string option, name: string option,
    51                        objtype: PgipTypes.objtype option }
    52   | Closeblock    of { }
    53   | Opentheory    of { thyname: string option, parentnames: string list, text: string}
    54   | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
    55   | Closetheory   of { text: string }
    56   | Opengoal      of { thmname: string option, text: string }
    57   | Proofstep     of { text: string }
    58   | Closegoal     of { text: string }
    59   | Giveupgoal    of { text: string }
    60   | Postponegoal  of { text: string }
    61   | Comment       of { text: string }
    62   | Doccomment    of { text: string }
    63   | Whitespace    of { text: string }
    64   | Spuriouscmd   of { text: string }
    65   | Badcmd        of { text: string }
    66   | Unparseable   of { text: string }
    67   | Metainfo      of { name: string option, text: string }
    68   | Litcomment    of { format: string option, content: XML.tree list }
    69   | Showcode      of { show: bool }
    70   | Setformat     of { format: string }
    71 
    72   type pgipdocument = pgipdoc list
    73   type pgip_parser  = string -> pgipdocument
    74 
    75    fun xml_of docelt =
    76        case docelt of
    77 
    78            Openblock vs  =>
    79            XML.Elem("openblock", opt_attr "name" (#metavarid vs) @
    80                                  opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
    81                                  opt_attr "metavarid" (#metavarid vs),
    82                     [])
    83 
    84          | Closeblock _ =>
    85            XML.Elem("closeblock", [], [])
    86 
    87          | Opentheory vs  =>
    88            XML.Elem("opentheory",
    89                     opt_attr "thyname" (#thyname vs) @
    90                     opt_attr "parentnames"
    91                              (case (#parentnames vs)
    92                                of [] => NONE
    93                                 | ps => SOME (space_implode ";" ps)),
    94                     [XML.Text (#text vs)])
    95 
    96          | Theoryitem vs =>
    97            XML.Elem("theoryitem",
    98                     opt_attr "name" (#name vs) @
    99                     opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs),
   100                     [XML.Text (#text vs)])
   101 
   102          | Closetheory vs =>
   103            XML.Elem("closetheory", [], [XML.Text (#text vs)])
   104 
   105          | Opengoal vs =>
   106            XML.Elem("opengoal",
   107                     opt_attr "thmname" (#thmname vs),
   108                     [XML.Text (#text vs)])
   109 
   110          | Proofstep vs =>
   111            XML.Elem("proofstep", [], [XML.Text (#text vs)])
   112 
   113          | Closegoal vs =>
   114            XML.Elem("closegoal", [], [XML.Text (#text vs)])
   115 
   116          | Giveupgoal vs =>
   117            XML.Elem("giveupgoal", [], [XML.Text (#text vs)])
   118 
   119          | Postponegoal vs =>
   120            XML.Elem("postponegoal", [], [XML.Text (#text vs)])
   121 
   122          | Comment vs =>
   123            XML.Elem("comment", [], [XML.Text (#text vs)])
   124 
   125          | Whitespace vs =>
   126            XML.Elem("whitespace", [], [XML.Text (#text vs)])
   127 
   128          | Doccomment vs =>
   129            XML.Elem("doccomment", [], [XML.Text (#text vs)])
   130 
   131          | Spuriouscmd vs =>
   132            XML.Elem("spuriouscmd", [], [XML.Text (#text vs)])
   133 
   134          | Badcmd vs =>
   135            XML.Elem("badcmd", [], [XML.Text (#text vs)])
   136 
   137          | Unparseable vs =>
   138            XML.Elem("unparseable", [], [XML.Text (#text vs)])
   139 
   140          | Metainfo vs =>
   141            XML.Elem("metainfo", opt_attr "name" (#name vs),
   142                     [XML.Text (#text vs)])
   143 
   144          | Litcomment vs =>
   145            XML.Elem("litcomment", opt_attr "format" (#format vs),
   146                    #content vs)
   147 
   148          | Showcode vs =>
   149            XML.Elem("showcode",
   150                     attr "show" (PgipTypes.bool_to_pgstring (#show vs)), [])
   151 
   152          | Setformat vs =>
   153            XML.Elem("setformat", attr "format" (#format vs), [])
   154 
   155    val output_doc = map xml_of
   156 
   157    fun unparse_elt docelt =
   158    case docelt of
   159        Openblock _ => ""
   160      | Closeblock _ => ""
   161      | Opentheory vs => #text vs
   162      | Theoryitem vs => #text vs
   163      | Closetheory vs => #text vs
   164      | Opengoal vs => #text vs
   165      | Proofstep vs => #text vs
   166      | Closegoal vs => #text vs
   167      | Giveupgoal vs => #text vs
   168      | Postponegoal vs => #text vs
   169      | Comment vs => #text vs
   170      | Doccomment vs => #text vs
   171      | Whitespace vs => #text vs
   172      | Spuriouscmd vs => #text vs
   173      | Badcmd vs => #text vs
   174      | Unparseable vs => #text vs
   175      | Metainfo vs => #text vs
   176      | _ => ""
   177 
   178 
   179    val unparse_doc = map unparse_elt
   180 
   181 
   182    (* Names of all PGIP document markup elements *)
   183    val doc_markup_elements =
   184        ["openblock",
   185         "closeblock",
   186         "opentheory",
   187         "theoryitem",
   188         "closetheory",
   189         "opengoal",
   190         "proofstep",
   191         "closegoal",
   192         "giveupgoal",
   193         "postponegoal",
   194         "comment",
   195         "doccomment",
   196         "whitespace",
   197         "spuriouscmd",
   198         "badcmd",
   199         (* the prover shouldn't really receive the next ones,
   200            but we include them here so that they are harmlessly
   201            ignored. *)
   202         "unparseable",
   203         "metainfo",
   204         (* Broker document format *)
   205         "litcomment",
   206         "showcode",
   207         "setformat"]
   208 
   209    (* non-document/empty text, must be ignored *)
   210    val doc_markup_elements_ignored =
   211        [ "metainfo", "openblock", "closeblock",
   212          "litcomment", "showcode", "setformat" ]
   213 
   214 end;