# HG changeset patch # User wenzelm # Date 1184192137 -7200 # Node ID 20f58293fc5e95a0db8de8ecf198143e64a2e77e # Parent fac9ea4d58ab23bb7e4c85bf7b72b0662acd49a3 tuned spacing; diff -r fac9ea4d58ab -r 20f58293fc5e src/Pure/ProofGeneral/pgip_isabelle.ML --- 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 - diff -r fac9ea4d58ab -r 20f58293fc5e src/Pure/ProofGeneral/pgip_markup.ML --- 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;