--- a/src/Pure/ProofGeneral/pgip_markup.ML Thu Jul 12 00:15:36 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_markup.ML Thu Jul 12 00:15:37 2007 +0200
@@ -8,15 +8,16 @@
signature PGIPMARKUP =
sig
(* Generic markup on sequential, non-overlapping pieces of proof text *)
- datatype pgipdoc =
- Openblock of { metavarid: string option, name: string option, objtype: PgipTypes.objtype option }
+ datatype pgipdoc =
+ Openblock of { metavarid: string option, name: string option,
+ objtype: PgipTypes.objtype option }
| Closeblock of { }
| Opentheory of { thyname: string, 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 }
+ | Opengoal of { thmname: string option, text: string }
| Proofstep of { text: string }
- | Closegoal of { text: string }
+ | Closegoal of { text: string }
| Giveupgoal of { text: string }
| Postponegoal of { text: string }
| Comment of { text: string }
@@ -24,18 +25,18 @@
| Whitespace of { text: string }
| Spuriouscmd of { text: string }
| Badcmd of { text: string }
- | Unparseable of { text: string }
- | Metainfo of { name: string option, text: string }
+ | Unparseable of { text: string }
+ | Metainfo of { name: string option, text: string }
(* Last three for PGIP literate markup only: *)
- | Litcomment of { format: string option, content: XML.content }
- | Showcode of { show: bool }
- | Setformat of { format: string }
+ | Litcomment of { format: string option, content: XML.content }
+ | Showcode of { show: bool }
+ | Setformat of { format: string }
type pgipdocument = pgipdoc list
type pgip_parser = string -> pgipdocument (* system must provide a parser P *)
- val unparse_doc : pgipdocument -> string list (* s.t. unparse (P x) = x *)
+ val unparse_doc : pgipdocument -> string list (* s.t. unparse (P x) = x *)
val output_doc : pgipdocument -> XML.content
- val doc_markup_elements : string list (* used in pgip_input *)
+ val doc_markup_elements : string list (* used in pgip_input *)
val doc_markup_elements_ignored : string list (* used in pgip_input *)
end
@@ -45,15 +46,16 @@
open PgipTypes
(* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *)
- datatype pgipdoc =
- Openblock of { metavarid: string option, name: string option, objtype: PgipTypes.objtype option }
+ datatype pgipdoc =
+ Openblock of { metavarid: string option, name: string option,
+ objtype: PgipTypes.objtype option }
| Closeblock of { }
| Opentheory of { thyname: string, 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 }
+ | Opengoal of { thmname: string option, text: string }
| Proofstep of { text: string }
- | Closegoal of { text: string }
+ | Closegoal of { text: string }
| Giveupgoal of { text: string }
| Postponegoal of { text: string }
| Comment of { text: string }
@@ -61,98 +63,98 @@
| Whitespace of { text: string }
| Spuriouscmd of { text: string }
| Badcmd of { text: string }
- | Unparseable of { text: string }
- | Metainfo of { name: string option, text: string }
- | Litcomment of { format: string option, content: XML.content }
- | Showcode of { show: bool }
- | Setformat of { format: string }
+ | Unparseable of { text: string }
+ | Metainfo of { name: string option, text: string }
+ | Litcomment of { format: string option, content: XML.content }
+ | Showcode of { show: bool }
+ | Setformat of { format: string }
type pgipdocument = pgipdoc list
type pgip_parser = string -> pgipdocument
- fun xml_of docelt =
+ fun xml_of docelt =
case docelt of
- Openblock vs =>
- XML.Elem("openblock", opt_attr "name" (#metavarid vs) @
- opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
- opt_attr "metavarid" (#metavarid vs),
- [])
-
- | Closeblock vs =>
- XML.Elem("closeblock", [], [])
-
- | Opentheory vs =>
- XML.Elem("opentheory",
- attr "thyname" (#thyname vs) @
- opt_attr "parentnames"
- (case (#parentnames vs)
- of [] => NONE
- | ps => SOME (space_implode ";" ps)),
- [XML.Text (#text vs)])
+ Openblock vs =>
+ XML.Elem("openblock", opt_attr "name" (#metavarid vs) @
+ opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
+ opt_attr "metavarid" (#metavarid vs),
+ [])
+
+ | Closeblock vs =>
+ XML.Elem("closeblock", [], [])
+
+ | Opentheory vs =>
+ XML.Elem("opentheory",
+ attr "thyname" (#thyname vs) @
+ opt_attr "parentnames"
+ (case (#parentnames vs)
+ of [] => NONE
+ | ps => SOME (space_implode ";" ps)),
+ [XML.Text (#text vs)])
- | Theoryitem vs =>
- XML.Elem("theoryitem",
- opt_attr "name" (#name vs) @
- opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs),
- [XML.Text (#text vs)])
-
- | Closetheory vs =>
- XML.Elem("closetheory", [], [XML.Text (#text vs)])
-
- | Opengoal vs =>
- XML.Elem("opengoal",
- opt_attr "thmname" (#thmname vs),
- [XML.Text (#text vs)])
+ | Theoryitem vs =>
+ XML.Elem("theoryitem",
+ opt_attr "name" (#name vs) @
+ opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs),
+ [XML.Text (#text vs)])
+
+ | Closetheory vs =>
+ XML.Elem("closetheory", [], [XML.Text (#text vs)])
- | Proofstep vs =>
- XML.Elem("proofstep", [], [XML.Text (#text vs)])
+ | Opengoal vs =>
+ XML.Elem("opengoal",
+ opt_attr "thmname" (#thmname vs),
+ [XML.Text (#text vs)])
- | Closegoal vs =>
- XML.Elem("closegoal", [], [XML.Text (#text vs)])
+ | Proofstep vs =>
+ XML.Elem("proofstep", [], [XML.Text (#text vs)])
+
+ | Closegoal vs =>
+ XML.Elem("closegoal", [], [XML.Text (#text vs)])
- | Giveupgoal vs =>
- XML.Elem("giveupgoal", [], [XML.Text (#text vs)])
+ | Giveupgoal vs =>
+ XML.Elem("giveupgoal", [], [XML.Text (#text vs)])
- | Postponegoal vs =>
- XML.Elem("postponegoal", [], [XML.Text (#text vs)])
+ | Postponegoal vs =>
+ XML.Elem("postponegoal", [], [XML.Text (#text vs)])
- | Comment vs =>
- XML.Elem("comment", [], [XML.Text (#text vs)])
+ | Comment vs =>
+ XML.Elem("comment", [], [XML.Text (#text vs)])
- | Whitespace vs =>
- XML.Elem("whitespace", [], [XML.Text (#text vs)])
+ | Whitespace vs =>
+ XML.Elem("whitespace", [], [XML.Text (#text vs)])
- | Doccomment vs =>
- XML.Elem("doccomment", [], [XML.Text (#text vs)])
+ | Doccomment vs =>
+ XML.Elem("doccomment", [], [XML.Text (#text vs)])
- | Spuriouscmd vs =>
- XML.Elem("spuriouscmd", [], [XML.Text (#text vs)])
+ | Spuriouscmd vs =>
+ XML.Elem("spuriouscmd", [], [XML.Text (#text vs)])
- | Badcmd vs =>
- XML.Elem("badcmd", [], [XML.Text (#text vs)])
+ | Badcmd vs =>
+ XML.Elem("badcmd", [], [XML.Text (#text vs)])
- | Unparseable vs =>
- XML.Elem("unparseable", [], [XML.Text (#text vs)])
+ | Unparseable vs =>
+ XML.Elem("unparseable", [], [XML.Text (#text vs)])
- | Metainfo vs =>
- XML.Elem("metainfo", opt_attr "name" (#name vs),
- [XML.Text (#text vs)])
+ | Metainfo vs =>
+ XML.Elem("metainfo", opt_attr "name" (#name vs),
+ [XML.Text (#text vs)])
- | Litcomment vs =>
- XML.Elem("litcomment", opt_attr "format" (#format vs),
- #content vs)
+ | Litcomment vs =>
+ XML.Elem("litcomment", opt_attr "format" (#format vs),
+ #content vs)
- | Showcode vs =>
- XML.Elem("showcode",
- attr "show" (PgipTypes.bool_to_pgstring (#show vs)), [])
+ | Showcode vs =>
+ XML.Elem("showcode",
+ attr "show" (PgipTypes.bool_to_pgstring (#show vs)), [])
- | Setformat vs =>
- XML.Elem("setformat", attr "format" (#format vs), [])
+ | Setformat vs =>
+ XML.Elem("setformat", attr "format" (#format vs), [])
val output_doc = map xml_of
- fun unparse_elt docelt =
+ fun unparse_elt docelt =
case docelt of
Openblock vs => ""
| Closeblock vs => ""
@@ -181,31 +183,32 @@
val doc_markup_elements =
["openblock",
"closeblock",
- "opentheory",
- "theoryitem",
- "closetheory",
- "opengoal",
- "proofstep",
- "closegoal",
- "giveupgoal",
- "postponegoal",
- "comment",
- "doccomment",
- "whitespace",
- "spuriouscmd",
- "badcmd",
- (* the prover shouldn't really receive the next ones,
- but we include them here so that they are harmlessly
+ "opentheory",
+ "theoryitem",
+ "closetheory",
+ "opengoal",
+ "proofstep",
+ "closegoal",
+ "giveupgoal",
+ "postponegoal",
+ "comment",
+ "doccomment",
+ "whitespace",
+ "spuriouscmd",
+ "badcmd",
+ (* the prover shouldn't really receive the next ones,
+ but we include them here so that they are harmlessly
ignored. *)
- "unparseable",
- "metainfo",
+ "unparseable",
+ "metainfo",
(* Broker document format *)
- "litcomment",
- "showcode",
- "setformat"]
+ "litcomment",
+ "showcode",
+ "setformat"]
(* non-document/empty text, must be ignored *)
val doc_markup_elements_ignored =
[ "metainfo", "openblock", "closeblock",
- "litcomment", "showcode", "setformat" ]
-end
+ "litcomment", "showcode", "setformat" ]
+
+end;