--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Thu Jul 12 00:15:36 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Thu Jul 12 00:15:37 2007 +0200
@@ -10,7 +10,7 @@
val isabelle_pgml_version_supported : string
val isabelle_pgip_version_supported : string
val systemid : string
- val accepted_inputs : (string * bool * (string list)) list
+ val accepted_inputs : (string * bool * (string list)) list
val location_of_position : Position.T -> PgipTypes.location
@@ -25,7 +25,7 @@
val ObjTheoremSet : PgipTypes.objtype
val ObjOracle : PgipTypes.objtype
val ObjLocale : PgipTypes.objtype
-
+
end
structure PgipIsabelle : PGIP_ISABELLE =
@@ -35,19 +35,20 @@
val isabelle_pgip_version_supported = "2.0"
val systemid = "Isabelle"
+
(** Accepted commands **)
local
(* These element names are a subset of those in pgip_input.ML.
They must be handled in proof_general_pgip.ML/process_pgip_element. *)
-
+
val accepted_names =
(* not implemented: "askconfig", "forget", "restoregoal" *)
["askpgip","askpgml","askprefs","getpref","setpref",
"proverinit","proverexit","startquiet","stopquiet",
"pgmlsymbolson", "pgmlsymbolsoff",
- "dostep", "undostep", "redostep", "abortgoal",
+ "dostep", "undostep", "redostep", "abortgoal",
"askids", "showid", "askguise",
"parsescript",
"showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
@@ -55,36 +56,36 @@
"retracttheory", "loadfile", "openfile", "closefile",
"abortfile", "retractfile", "changecwd", "systemcmd"];
- fun element_async p =
- false (* single threaded only *)
+ fun element_async p =
+ false (* single threaded only *)
fun supported_optional_attrs p = (case p of
- "undostep" => ["times"]
- (* TODO: we could probably extend these too:
- | "redostep" => ["times"]
- | "undoitem" => ["times"]
- | "redoitem" => ["times"] *)
- | _ => [])
+ "undostep" => ["times"]
+ (* TODO: we could probably extend these too:
+ | "redostep" => ["times"]
+ | "undoitem" => ["times"]
+ | "redoitem" => ["times"] *)
+ | _ => [])
in
-val accepted_inputs =
+val accepted_inputs =
(map (fn p=> (p, element_async p, supported_optional_attrs p))
accepted_names);
end
-fun location_of_position pos =
+fun location_of_position pos =
let val line = Position.line_of pos
- val (url,descr) =
- (case Position.file_of pos of
- NONE => (NONE, NONE)
- | SOME fname =>
- let val path = Path.explode fname in
- case ThyLoad.check_file NONE path of
- SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
- | NONE => (NONE, SOME fname)
- end);
+ val (url,descr) =
+ (case Position.file_of pos of
+ NONE => (NONE, NONE)
+ | SOME fname =>
+ let val path = Path.explode fname in
+ case ThyLoad.check_file NONE path of
+ SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
+ | NONE => (NONE, SOME fname)
+ end);
in
- { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
+ { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
end
@@ -97,17 +98,15 @@
ObjTheoremSet,
ObjOracle,
ObjLocale] =
- map PgipTypes.ObjOther
- ["theory body",
- "theory declaration",
- "theory subsection",
- "proof body",
- "formal comment",
- "class",
- "theorem set declaration",
- "oracle",
- "locale"];
+ map PgipTypes.ObjOther
+ ["theory body",
+ "theory declaration",
+ "theory subsection",
+ "proof body",
+ "formal comment",
+ "class",
+ "theorem set declaration",
+ "oracle",
+ "locale"];
-
end
-
--- 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;