# HG changeset patch # User aspinall # Date 1166391830 -3600 # Node ID 8750fbc28d5c879d46ffb61ab2d5b07a6fa3e4af # Parent d589f6f5da65e98ad7f92f1aa087ca4dcc99a749 Add abstraction for objtypes and documents. diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/README --- a/src/Pure/ProofGeneral/README Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/README Sun Dec 17 22:43:50 2006 +0100 @@ -31,6 +31,7 @@ For the full PGIP schema and an explanation of it, see: http://proofgeneral.inf.ed.ac.uk/kit + http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIP David Aspinall, Dec. 2006. $Id$ diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/ROOT.ML --- a/src/Pure/ProofGeneral/ROOT.ML Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/ROOT.ML Sun Dec 17 22:43:50 2006 +0100 @@ -3,11 +3,16 @@ use "pgip_input.ML"; use "pgip_output.ML"; use "pgip.ML"; -use "pgip_tests.ML"; use "pgip_isabelle.ML"; use "preferences.ML"; use "parsing.ML"; +use "pgip_tests.ML"; + (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_pgip.ML"; (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_emacs.ML"; + +(* desirable to have tests on UI connection: + use "pgip_isabelle_tests.ML" +*) diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/parsing.ML --- a/src/Pure/ProofGeneral/parsing.ML Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/parsing.ML Sun Dec 17 22:43:50 2006 +0100 @@ -2,12 +2,12 @@ ID: $Id$ Author: David Aspinall -Parsing theory files to add PGIP markup. +Parsing Isabelle theory files to add PGIP markup. *) signature PGIP_PARSER = sig - val xmls_of_str: string -> XML.content + val pgip_parser: PgipMarkup.pgip_parser end structure PgipParser : PGIP_PARSER = @@ -18,6 +18,8 @@ structure P = OuterParse; +structure D = PgipMarkup; + (* Notes. This is quite tricky, because 1) we need to put back whitespace which was removed during parsing so we can provide markup around commands; @@ -27,7 +29,7 @@ Markus June '04) helps do this, but the mechanism is still a bad mess. If we had proper parse trees it would be easy, although having a - fixed type of trees might be tricky with Isar's extensible parser. + fixed type of trees might be hard with Isar's extensible parser. Probably the best solution is to produce the meta-information at the same time as the parse, for each command, e.g. by recording a @@ -53,31 +55,17 @@ *) local - fun markup_text str elt = [XML.Elem(elt, [], [XML.Text str])] - fun markup_text_attrs str elt attrs = [XML.Elem(elt, attrs, [XML.Text str])] - fun empty elt = [XML.Elem(elt, [], [])] - fun whitespace str = XML.Elem("whitespace", [], [XML.Text str]) + fun whitespace str = D.Whitespace { text=str } (* an extra token is needed to terminate the command *) val sync = OuterSyntax.scan "\\<^sync>"; - fun named_item_elt_with nameattr toks str elt nameP objtyp = - let - val name = (fst (nameP (toks@sync))) - handle _ => (error ("Error occurred in name parser for " ^ elt ^ - "(objtype: " ^ objtyp ^ ")"); - "") - - in - [XML.Elem(elt, - ((if name="" then [] else [(nameattr, name)])@ - (if objtyp="" then [] else [("objtype", objtyp)])), - [XML.Text str])] - end - - val named_item_elt = named_item_elt_with "name" - val thmnamed_item_elt = named_item_elt_with "thmname" + fun nameparse elt objtyp nameP toks = + (fst (nameP (toks@sync))) + handle _ => (error ("Error occurred in name parser for " ^ elt ^ + "(objtype: " ^ objtyp ^ ")"); + "") fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg) @@ -100,10 +88,9 @@ let val ((thyname,imports,files),_) = ThyHeader.args (toks@sync) in - markup_text_attrs str "opentheory" - ([("thyname",thyname)] @ - (if imports=[] then [] else - [("parentnames", (space_implode ";" imports) ^ ";")])) + [D.Opentheory { thyname=thyname, + parentnames = imports, + text = str }] end fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases *) @@ -125,9 +112,12 @@ "oracle", "declare"] - val plain_item = markup_text str "theoryitem" - val comment_item = markup_text str "doccomment" - val named_item = named_item_elt toks str "theoryitem" + fun named_item nameP ty = + [D.Theoryitem {text=str,name=SOME (nameparse "theoryitem" ty nameP toks),objtype=SOME ty}] + val plain_item = + [D.Theoryitem {text=str,name=NONE,objtype=NONE}] + val doccomment = + [D.Doccomment {text=str}] val opt_overloaded = P.opt_keyword "overloaded"; @@ -147,8 +137,8 @@ if member (op =) plain_items name then plain_item else case name of - "text" => comment_item - | "text_raw" => comment_item + "text" => doccomment + | "text_raw" => doccomment | "typedecl" => named_item (P.type_args |-- P.name) "type" | "types" => named_item (P.type_args |-- P.name) "type" | "classes" => named_item P.name "class" @@ -161,7 +151,8 @@ | "lemmas" => named_item thmnameP "thmset" | "oracle" => named_item P.name "oracle" | "locale" => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale" - | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item) + | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); + plain_item) end fun xmls_of_thy_goal (name,toks,str) = @@ -178,60 +169,65 @@ fst a) (* a : (bstring * Args.src list) *) val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "") - (* TODO: add preference values for attributes - val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)] - *) + val thmname = nameparse "opengoal" "theorem" nameP toks in - (thmnamed_item_elt toks str "opengoal" nameP "") @ - (empty "openblock") + [D.Opengoal {thmname=SOME thmname, text=str}, + D.Openblock {metavarid=NONE,name=NONE,objtype=SOME "theorem-proof"}] end - fun xmls_of_qed (name,markup) = + fun xmls_of_qed (name,str) = let val qedmarkup = (case name of - "sorry" => markup "postponegoal" - | "oops" => markup "giveupgoal" - | "done" => markup "closegoal" - | "by" => markup "closegoal" (* nested or toplevel *) - | "qed" => markup "closegoal" (* nested or toplevel *) - | "." => markup "closegoal" (* nested or toplevel *) - | ".." => markup "closegoal" (* nested or toplevel *) + "sorry" => D.Postponegoal {text=str} + | "oops" => D.Giveupgoal {text=str} + | "done" => D.Closegoal {text=str} + | "by" => D.Closegoal {text=str} (* nested or toplevel *) + | "qed" => D.Closegoal {text=str} (* nested or toplevel *) + | "." => D.Closegoal {text=str} (* nested or toplevel *) + | ".." => D.Closegoal {text=str} (* nested or toplevel *) | other => (* default to closegoal: may be wrong for extns *) (parse_warning ("Unrecognized qed command: " ^ quote other); - markup "closegoal")) - in qedmarkup @ (empty "closeblock") end + D.Closegoal {text=str})) + in qedmarkup :: [D.Closeblock {}] end fun xmls_of_kind kind (name,toks,str) = - let val markup = markup_text str in case kind of - "control" => markup "badcmd" - | "diag" => markup "spuriouscmd" + "control" => [D.Badcmd {text=str}] + | "diag" => [D.Theoryitem {name=NONE,objtype=NONE, + text=str}] (* FIXME: check NOT spuriouscmd *) (* theory/files *) | "theory-begin" => xmls_of_thy_begin (name,toks,str) | "theory-decl" => xmls_of_thy_decl (name,toks,str) - | "theory-heading" => markup "doccomment" - | "theory-script" => markup "theorystep" - | "theory-end" => markup "closetheory" + | "theory-heading" => [D.Doccomment {text=str}] + | "theory-script" => [D.Theoryitem {name=NONE,objtype=NONE,text=str}] + | "theory-end" => [D.Closetheory {text=str}] (* proof control *) | "theory-goal" => xmls_of_thy_goal (name,toks,str) - | "proof-heading" => markup "doccomment" - | "proof-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: have, show, ... *) - | "proof-block" => markup "proofstep" (* context-shift: proof, next; really "newgoal" *) - | "proof-open" => (empty "openblock") @ (markup "proofstep") - | "proof-close" => (markup "proofstep") @ (empty "closeblock") - | "proof-script" => markup "proofstep" - | "proof-chain" => markup "proofstep" - | "proof-decl" => markup "proofstep" - | "proof-asm" => markup "proofstep" - | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: obtain *) - | "qed" => xmls_of_qed (name,markup) - | "qed-block" => xmls_of_qed (name,markup) - | "qed-global" => xmls_of_qed (name,markup) - | other => (* default for anything else is "spuriouscmd", ignored for undo *) + | "proof-heading" => [D.Doccomment {text=str}] + + | "proof-goal" => (* nested proof: have, show, ... *) + [D.Opengoal {text=str,thmname=NONE}, + D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}] + + | "proof-block" => [D.Proofstep {text=str}] + | "proof-open" => [D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}, + D.Proofstep {text=str} ] + | "proof-close" => [D.Proofstep {text=str}, D.Closeblock {}] + | "proof-script" => [D.Proofstep {text=str}] + | "proof-chain" => [D.Proofstep {text=str}] + | "proof-decl" => [D.Proofstep {text=str}] + | "proof-asm" => [D.Proofstep {text=str}] + | "proof-asm-goal" => (* nested proof: obtain, ... *) + [D.Opengoal {text=str,thmname=NONE}, + D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}] + + | "qed" => xmls_of_qed (name,str) + | "qed-block" => xmls_of_qed (name,str) + | "qed-global" => xmls_of_qed (name,str) + | other => (* default for anything else is "spuriouscmd", ***ignored for undo*** *) (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other); - markup "spuriouscmd") - end + [D.Spuriouscmd {text=str}]) in fun xmls_of_transition (name,str,toks) = @@ -241,22 +237,19 @@ SOME k => (xmls_of_kind k (name,toks,str)) | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *) (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd"); - markup_text str "spuriouscmd") + [D.Spuriouscmd {text=str}]) end -fun markup_toks [] _ = [] - | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x - fun markup_comment_whs [] = [] | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *) let val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks in if (prewhs <> []) then - whitespace (implode (map OuterLex.unparse prewhs)) + D.Whitespace {text=implode (map OuterLex.unparse prewhs)} :: (markup_comment_whs rest) else - (markup_text (OuterLex.unparse t) "comment") @ + D.Comment {text=OuterLex.unparse t} :: (markup_comment_whs ts) end @@ -277,22 +270,26 @@ in ((markup_comment_whs prewhs) @ (if (length rest2 = length rest1) then [] - else markup_text (implode - (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1)))) - "doccomment") @ - (markup_comment_whs postwhs), - Library.take (length rest3 - 1,rest3)) + else + [D.Doccomment + {text= implode + (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1)))}] + @ + (markup_comment_whs postwhs)), + Library.take (length rest3 - 1,rest3)) end fun xmls_of_impropers toks = let val (xmls,rest) = xmls_pre_cmd toks + val unparsed = + case rest of [] => [] + | _ => [D.Unparseable + {text= implode (map OuterLex.unparse rest)}] in - xmls @ (markup_toks rest "unparseable") + xmls @ unparsed end -fun markup_unparseable str = markup_text str "unparseable" - end @@ -307,7 +304,7 @@ else match_tokens (t::ts,ws,w::vs) | match_tokens _ = error ("match_tokens: mismatched input parse") in - fun xmls_of_str str = + fun pgip_parser str = let (* parsing: See outer_syntax.ML/toplevel_source *) fun parse_loop ([],[],xmls) = xmls @@ -332,7 +329,7 @@ in parse_loop (OuterSyntax.read toks, toks, []) end) - handle _ => markup_unparseable str + handle _ => [D.Unparseable {text=str}] end end diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/pgip_input.ML --- a/src/Pure/ProofGeneral/pgip_input.ML Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_input.ML Sun Dec 17 22:43:50 2006 +0100 @@ -29,11 +29,15 @@ | Redostep of { } | Abortgoal of { } | Forget of { thyname: string option, name: string option, - objtype: string option } + objtype: PgipTypes.objtype option } | Restoregoal of { thmname : string } (* context inspection commands *) - | Askids of { thyname:string option, objtype:string option } - | Showid of { thyname:string option, objtype:string, name:string } + | Askids of { url: PgipTypes.pgipurl option, + thyname: PgipTypes.objname option, + objtype: PgipTypes.objtype option } + | Showid of { thyname: PgipTypes.objname option, + objtype: PgipTypes.objtype, + name: PgipTypes.objname } | Askguise of { } | Parsescript of { text: string, location: PgipTypes.location, systemdata: string option } @@ -89,11 +93,15 @@ | Redostep of { } | Abortgoal of { } | Forget of { thyname: string option, name: string option, - objtype: string option } + objtype: PgipTypes.objtype option } | Restoregoal of { thmname : string } (* context inspection commands *) - | Askids of { thyname:string option, objtype:string option } - | Showid of { thyname:string option, objtype:string, name:string } + | Askids of { url: PgipTypes.pgipurl option, + thyname: PgipTypes.objname option, + objtype: PgipTypes.objtype option } + | Showid of { thyname: PgipTypes.objname option, + objtype: PgipTypes.objtype, + name: PgipTypes.objname } | Askguise of { } | Parsescript of { text: string, location: location, systemdata: string option } @@ -123,12 +131,18 @@ val thyname_attro = get_attr_opt "thyname" val thyname_attr = get_attr "thyname" - val objtype_attro = get_attr_opt "objtype" - val objtype_attr = get_attr "objtype" val name_attr = get_attr "name" val name_attro = get_attr_opt "name" val thmname_attr = get_attr "thmname" + fun objtype_attro attrs = if has_attr "objtype" attrs then + SOME (objtype_of_attrs attrs) + else NONE + + fun pgipurl_attro attrs = if has_attr "url" attrs then + SOME (pgipurl_of_attrs attrs) + else NONE + val times_attr = read_pgipnat o (get_attr_dflt "times" "1") val prefcat_attr = get_attr_opt "prefcategory" @@ -173,10 +187,11 @@ objtype = objtype_attro attrs } | "restoregoal" => Restoregoal { thmname = thmname_attr attrs} (* proofctxt: improper commands *) - | "askids" => Askids { thyname = thyname_attro attrs, + | "askids" => Askids { url = pgipurl_attro attrs, + thyname = thyname_attro attrs, objtype = objtype_attro attrs } | "showid" => Showid { thyname = thyname_attro attrs, - objtype = objtype_attr attrs, + objtype = objtype_of_attrs attrs, name = name_attr attrs } | "askguise" => Askguise { } | "parsescript" => Parsescript { text = (xmltext data), diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/pgip_markup.ML --- a/src/Pure/ProofGeneral/pgip_markup.ML Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_markup.ML Sun Dec 17 22:43:50 2006 +0100 @@ -9,9 +9,9 @@ sig (* Generic markup on sequential, non-overlapping pieces of proof text *) datatype pgipdoc = - Openblock of { metavarid: string option } + Openblock of { metavarid: string option, name: string option, objtype: string option } | Closeblock of { } - | Opentheory of { thyname: string option, parentnames: string list , text: string} + | Opentheory of { thyname: string, parentnames: string list , text: string} | Theoryitem of { name: string option, objtype: string option, text: string } | Closetheory of { text: string } | Opengoal of { thmname: string option, text: string } @@ -24,6 +24,7 @@ | Whitespace of { text: string } | Spuriouscmd of { text: string } | Badcmd of { 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 } @@ -43,10 +44,11 @@ struct open PgipTypes +(* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *) datatype pgipdoc = - Openblock of { metavarid: string option } + Openblock of { metavarid: string option, name: string option, objtype: string option } | Closeblock of { } - | Opentheory of { thyname: string option, parentnames: string list , text: string} + | Opentheory of { thyname: string, parentnames: string list, text: string} | Theoryitem of { name: string option, objtype: string option, text: string } | Closetheory of { text: string } | Opengoal of { thmname: string option, text: string } @@ -59,6 +61,7 @@ | 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 } @@ -76,6 +79,15 @@ | 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) @ @@ -105,6 +117,9 @@ | Comment vs => XML.Elem("comment", [], [XML.Text (#text vs)]) + | Whitespace vs => + XML.Elem("whitespace", [], [XML.Text (#text vs)]) + | Doccomment vs => XML.Elem("doccomment", [], [XML.Text (#text vs)]) @@ -114,6 +129,9 @@ | Badcmd vs => XML.Elem("badcmd", [], [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)]) @@ -148,6 +166,7 @@ | Whitespace vs => #text vs | Spuriouscmd vs => #text vs | Badcmd vs => #text vs + | Unparseable vs => #text vs | Metainfo vs => #text vs | _ => "" diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/pgip_output.ML --- a/src/Pure/ProofGeneral/pgip_output.ML Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_output.ML Sun Dec 17 22:43:50 2006 +0100 @@ -30,21 +30,21 @@ descr: string, url: Url.T, filenameextns: string } - | Idtable of { objtype: string, - context: string option, - ids: string list } - | Setids of { idtables: XML.content } - | Delids of { idtables: XML.content } - | Addids of { idtables: XML.content } + | Setids of { idtables: PgipTypes.idtable list } + | Delids of { idtables: PgipTypes.idtable list } + | Addids of { idtables: PgipTypes.idtable list } | Hasprefs of { prefcategory: string option, prefs: PgipTypes.preference list } | Prefval of { name: string, value: string } - | Idvalue of { name: string, objtype: string, text: XML.content } + | Idvalue of { name: PgipTypes.objname, + objtype: PgipTypes.objtype, + text: XML.content } | Informguise of { file : PgipTypes.pgipurl option, - theory: string option, - theorem: string option, + theory: PgipTypes.objname option, + theorem: PgipTypes.objname option, proofpos: int option } - | Parseresult of { attrs: XML.attributes, content: XML.content } + | Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, + errs: XML.content } (* errs to become PGML *) | Usespgip of { version: string, pgipelems: (string * bool * string list) list } | Usespgml of { version: string } @@ -77,16 +77,20 @@ | Lexicalstructure of { content: XML.content } | Proverinfo of { name: string, version: string, instance: string, descr: string, url: Url.T, filenameextns: string } - | Idtable of { objtype: string, context: string option, ids: string list } - | Setids of { idtables: XML.content } - | Delids of { idtables: XML.content } - | Addids of { idtables: XML.content } + | Setids of { idtables: PgipTypes.idtable list } + | Delids of { idtables: PgipTypes.idtable list } + | Addids of { idtables: PgipTypes.idtable list } | Hasprefs of { prefcategory: string option, prefs: preference list } | Prefval of { name: string, value: string } - | Idvalue of { name: string, objtype: string, text: XML.content } - | Informguise of { file : pgipurl option, theory: string option, - theorem: string option, proofpos: int option } - | Parseresult of { attrs: XML.attributes, content: XML.content } + | Idvalue of { name: PgipTypes.objname, + objtype: PgipTypes.objtype, + text: XML.content } + | Informguise of { file : PgipTypes.pgipurl option, + theory: PgipTypes.objname option, + theorem: PgipTypes.objname option, + proofpos: int option } + | Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument, + errs: XML.content } (* errs to become PGML *) | Usespgip of { version: string, pgipelems: (string * bool * string list) list } | Usespgml of { version: string } @@ -189,39 +193,25 @@ []) end -fun idtable vs = - let - val objtype = #objtype vs - val objtype_attrs = attr "objtype" objtype - val context = #context vs - val context_attrs = opt_attr "context" context - val ids = #ids vs - val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids - in - XML.Elem ("idtable", - objtype_attrs @ context_attrs, - ids_content) - end - fun setids vs = let val idtables = #idtables vs in - XML.Elem ("setids",[],idtables) + XML.Elem ("setids",[],map idtable_to_xml idtables) end fun addids vs = let val idtables = #idtables vs in - XML.Elem ("addids",[],idtables) + XML.Elem ("addids",[],map idtable_to_xml idtables) end fun delids vs = let val idtables = #idtables vs in - XML.Elem ("delids",[],idtables) + XML.Elem ("delids",[],map idtable_to_xml idtables) end @@ -258,10 +248,10 @@ fun idvalue vs = let val name = #name vs - val objtype = #objtype vs + val objtype_attrs = attrs_of_objtype (#objtype vs) val text = #text vs in - XML.Elem("idvalue", [("name",name),("objtype",objtype)], text) + XML.Elem("idvalue", attr "name" name @ objtype_attrs, text) end @@ -286,9 +276,11 @@ fun parseresult vs = let val attrs = #attrs vs - val content = #content vs + val doc = #doc vs + val errs = #errs vs + val xmldoc = PgipMarkup.output_doc doc in - XML.Elem("parseresult", attrs, content) + XML.Elem("parseresult", attrs, errs@xmldoc) end fun usespgip vs = @@ -341,7 +333,6 @@ | Metainforesponse vs => metainforesponse vs | Lexicalstructure vs => lexicalstructure vs | Proverinfo vs => proverinfo vs - | Idtable vs => idtable vs | Setids vs => setids vs | Addids vs => addids vs | Delids vs => delids vs diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/pgip_tests.ML --- a/src/Pure/ProofGeneral/pgip_tests.ML Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_tests.ML Sun Dec 17 22:43:50 2006 +0100 @@ -82,6 +82,14 @@ end +(** pgip_markup.ML **) +local +open PgipMarkup +in +val _ = () +end + + (** pgip_output.ML **) local open PgipOutput @@ -89,3 +97,25 @@ val _ = () end + +(** parsing.ML **) +local +open PgipMarkup +open PgipParser +fun asseqp a b = + if (pgip_parser a)=b then () + else error("PGIP test: expected two parses to be equal, for input:\n" ^ a) + +in +val _ = + asseqp "theory A imports Bthy Cthy Dthy begin" + [Opentheory + {text = "theory A imports Bthy Cthy Dthy begin", + thyname = "A", + parentnames = ["Bthy", "Cthy", "Dthy"]}]; + +val _ = + asseqp "end" + [Closetheory {text = "end"}]; + +end diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/pgip_types.ML --- a/src/Pure/ProofGeneral/pgip_types.ML Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_types.ML Sun Dec 17 22:43:50 2006 +0100 @@ -5,9 +5,22 @@ PGIP abstraction: types and conversions *) -(* TODO: add objtypes and PGML *) +(* TODO: PGML *) signature PGIPTYPES = sig + (* Object types: the types of values which can be manipulated externally. + Ideally a list of other types would be configured as a parameter. *) + datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment + | ObjTerm | ObjType | ObjOther of string + + (* Names for values of objtypes (i.e. prover identifiers). Could be a parameter. + Names for ObjFiles are URIs. *) + type objname = string + + type idtable = { context: objname option, (* container's objname *) + objtype: objtype, + ids: objname list } + (* Types and values (used for preferences and dialogs) *) datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat @@ -50,6 +63,12 @@ signature PGIPTYPES_OPNS = sig include PGIPTYPES + + (* Object types *) + val name_of_objtype : objtype -> string + val attrs_of_objtype : objtype -> XML.attributes + val objtype_of_attrs : XML.attributes -> objtype (* raises PGIP *) + val idtable_to_xml : idtable -> XML.tree (* Values as XML strings *) val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *) @@ -76,10 +95,12 @@ val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *) val pgipurl_of_string : string -> pgipurl (* raises PGIP *) val pgipurl_of_path : Path.T -> pgipurl + val path_of_pgipurl : pgipurl -> Path.T val attrs_of_pgipurl : pgipurl -> XML.attributes val pgipurl_of_attrs : XML.attributes -> pgipurl (* raises PGIP *) (* XML utils, only for PGIP code *) + val has_attr : string -> XML.attributes -> bool val attr : string -> string -> XML.attributes val opt_attr : string -> string option -> XML.attributes val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes @@ -92,7 +113,9 @@ struct exception PGIP of string -(** Utils **) +(** XML utils **) + +fun has_attr attr attrs = AList.defined (op =) attrs attr fun get_attr_opt attr attrs = AList.lookup (op =) attrs attr @@ -113,6 +136,50 @@ val opt_attr = opt_attr_map I + +(** Objtypes **) + +datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment + | ObjTerm | ObjType | ObjOther of string + +fun name_of_objtype obj = + case obj of + ObjFile => "file" + | ObjTheory => "theory" + | ObjTheorem => "theorem" + | ObjComment => "comment" + | ObjTerm => "term" + | ObjType => "type" + | ObjOther s => s + +val attrs_of_objtype = (attr "objtype") o name_of_objtype + +fun objtype_of_attrs attrs = case get_attr "objtype" attrs of + "file" => ObjFile + | "theory" => ObjTheory + | "theorem" => ObjTheorem + | "comment" => ObjComment + | "term" => ObjTerm + | "type" => ObjType + | s => ObjOther s (* where s mem other_objtypes_parameter *) + +type objname = string +type idtable = { context: objname option, (* container's objname *) + objtype: objtype, + ids: objname list } + +fun idtable_to_xml {context, objtype, ids} = + let + val objtype_attrs = attrs_of_objtype objtype + val context_attrs = opt_attr "context" context + val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids + in + XML.Elem ("idtable", + objtype_attrs @ context_attrs, + ids_content) + end + + (** Types and values **) (* readers and writers for values represented in XML strings *) @@ -258,9 +325,7 @@ | pgval_to_string (_,(Pgvalstring s)) = string_to_pgstring s -(** URLs: only local files **) - -type pgipurl = Path.T +type pgipurl = Path.T (* URLs: only local files *) datatype displayarea = Status | Message | Display | Other of string @@ -278,6 +343,7 @@ (** Url operations **) + fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *) case Url.explode url of (Url.File path) => path @@ -285,6 +351,8 @@ fun pgipurl_of_path p = p +fun path_of_pgipurl p = p (* potentially raises PGIP *) + fun attrs_of_pgipurl purl = [("url", "file:" ^ (XML.text (File.platform_path (File.full_path purl))))] diff -r d589f6f5da65 -r 8750fbc28d5c src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Dec 16 20:27:56 2006 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Dec 17 22:43:50 2006 +0100 @@ -294,7 +294,6 @@ val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name; val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name; -val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name; fun proper_inform_file_processed file state = let val name = thy_name file in @@ -414,37 +413,6 @@ end -(* PGIP identifier tables (prover objects). [incomplete] *) - -local - (* TODO: objtypes should be in pgip_types.ML *) - val objtype_thy = "theory" - val objtype_thm = "theorem" - val objtype_term = "term" - val objtype_type = "type" - - fun xml_idtable ty ctx ids = - PgipOutput.output (Idtable {objtype=ty,context=ctx,ids=ids}) -in - -fun setids t = issue_pgip (Setids {idtables = [t]}) -fun addids t = issue_pgip (Addids {idtables = [t]}) -fun delids t = issue_pgip (Delids {idtables = [t]}) - -fun delallids ty = setids (xml_idtable ty NONE []) - -fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys) -fun clear_thy_idtable () = delallids objtype_thy - -fun send_thm_idtable ctx thy = - addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy))); - -fun clear_thm_idtable () = delallids objtype_thm - -(* fun send_type_idtable thy = TODO, it's a bit low-level messy - & maybe not so useful anyway *) - -end (* Sending commands to Isar *) @@ -469,7 +437,7 @@ end -(**** PGIP actions ****) +(******* PGIP actions *******) (* Responses to each of the PGIP input commands. @@ -558,21 +526,45 @@ fun abortgoal vs = isarcmd "ProofGeneral.kill_proof" +(*** PGIP identifier tables ***) + +fun setids t = issue_pgip (Setids {idtables = [t]}) +fun addids t = issue_pgip (Addids {idtables = [t]}) +fun delids t = issue_pgip (Delids {idtables = [t]}) + +(* + fun delallids ty = + issue_pgip (Setids {idtables = + [{context=NONE,objtype=ty,ids=[]}]}) *) + fun askids vs = let - val thyname = #thyname vs - val objtype = #objtype vs + val url = #url vs (* ask for identifiers within a file *) + val thyname = #thyname vs (* ask for identifiers within a theory *) + val objtype = #objtype vs (* ask for identifiers of a particular type *) + + fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} + + val thms_of_thy = (map fst) o PureThy.thms_of o ThyInfo.get_theory in +(* case (url_attr,thyname,objtype) of + (NONE,NONE,NONE) => +*) (* top-level: return *) + (* TODO: add askids for "file" here, which returns single theory with same name *) + (* FIXME: objtypes on both sides *) case (thyname,objtype) of - (* only theories known in top context *) - (NONE, NONE) => send_thy_idtable NONE (ThyInfo.names()) - | (NONE, SOME "theory") => send_thy_idtable NONE (ThyInfo.names()) - | (SOME thy, SOME "theory") => send_thy_idtable (SOME thy) (ThyInfo.get_preds thy) - | (SOME thy, SOME "theorem") => send_thm_idtable (SOME thy) (ThyInfo.get_theory thy) - | (SOME thy, NONE) => (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy); - send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)) - | (_, SOME ot) => error ("No objects of type "^(quote ot)^" are available here.") + (* only files known in top context *) + (NONE, NONE) => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris?*) + | (NONE, SOME ObjFile) => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *) + | (SOME fi, SOME ObjFile) => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *) + | (NONE, SOME ObjTheory) => setids (idtable ObjTheory NONE (ThyInfo.names())) + | (SOME thy, SOME ObjTheory) => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy)) + | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy)) + (* next case is both of above. FIXME: cleanup this *) + | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy)); + setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))) + | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.") end local @@ -590,7 +582,7 @@ let val thyname = #thyname vs val objtype = #objtype vs - val name = #objtype vs + val name = #name vs val topthy = Toplevel.theory_of o Toplevel.get_state fun idvalue objtype name strings = @@ -600,18 +592,20 @@ fun pthm thy name = print_thm (get_thm thy (Name name)) in case (thyname, objtype) of - (_,"theory") => - with_displaywrap (idvalue "theory" name) + (_,ObjTheory) => + with_displaywrap (idvalue ObjTheory name) (fn ()=>(print_theory (ThyInfo.get_theory name))) - | (SOME thy, "theorem") => - with_displaywrap (idvalue "theorem" name) + | (SOME thy, ObjTheorem) => + with_displaywrap (idvalue ObjTheorem name) (fn ()=>(pthm (ThyInfo.get_theory thy) name)) - | (NONE, "theorem") => - with_displaywrap (idvalue "theorem" name) + | (NONE, ObjTheorem) => + with_displaywrap (idvalue ObjTheorem name) (fn ()=>pthm (topthy()) name) - | (_, ot) => error ("Cannot show objects of type "^ot) + | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot)) end +(*** Inspecting state ***) + (* The file which is currently being processed interactively. In the pre-PGIP code, this was informed to Isabelle and the theory loader on completion, but that allows for circularity in case we read @@ -649,15 +643,16 @@ val systemdata = #systemdata vs val location = #location vs (* TODO: extract position *) - val _ = start_delay_msgs () (* gather parsing messages *) - val xmls = PgipParser.xmls_of_str text + val _ = start_delay_msgs () (* gather parsing errs/warns *) + val doc = PgipParser.pgip_parser text val errs = end_delayed_msgs () val sysattrs = PgipTypes.opt_attr "systemdata" systemdata val locattrs = PgipTypes.attrs_of_location location in issue_pgip (Parseresult { attrs= sysattrs@locattrs, - content = (map PgipOutput.output errs)@xmls }) + doc = doc, + errs = (map PgipOutput.output errs) }) end fun showproofstate vs = isarcmd "pr" @@ -685,6 +680,8 @@ isarcmd ("print_" ^ arg) (* FIXME: isatool doc?. Return URLs, maybe? *) end +(*** Theory ***) + fun doitem vs = let val text = #text vs @@ -708,6 +705,61 @@ isarcmd ("kill_thy " ^ quote thyname) end + +(*** Files ***) + +(* Path management: we allow theory files to have dependencies in + their own directory, but when we change directory for a new file we + remove the path. Leaving it there can cause confusion with + difference in batch mode. + NB: PGIP does not assume that the prover has a load path. +*) + +local + val current_working_dir = ref (NONE : string option) +in +fun changecwd_dir newdirpath = + let + val newdir = File.platform_path newdirpath + in + (case (!current_working_dir) of + NONE => () + | SOME dir => ThyLoad.del_path dir; + ThyLoad.add_path newdir; + current_working_dir := SOME newdir) + end +end + +fun changecwd vs = + let + val url = #url vs + val newdir = PgipTypes.path_of_pgipurl url + in + changecwd_dir url + end + +fun openfile vs = + let + val url = #url vs + val filepath = PgipTypes.path_of_pgipurl url + val filedir = Path.dir filepath + val thy_name = Path.implode o #1 o Path.split_ext o Path.base + val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name; + in + case !currently_open_file of + SOME f => raise PGIP (" when a file is already open! ") + | NONE => (openfile_retract filepath; + changecwd_dir filedir; + currently_open_file := SOME url) + end + +fun closefile vs = + case !currently_open_file of + SOME f => (proper_inform_file_processed (File.platform_path f) + (Isar.state()); + currently_open_file := NONE) + | NONE => raise PGIP (" when no file is open!") + fun loadfile vs = let val url = #url vs @@ -717,23 +769,6 @@ | NONE => use_thy_or_ml_file (File.platform_path url) end -fun openfile vs = - let - val url = #url vs - in - case !currently_open_file of - SOME f => raise PGIP (" when a file is already open! ") - | NONE => (openfile_retract (File.platform_path url); - currently_open_file := SOME url) (*(File.platform_path url))*) - end - -fun closefile vs = - case !currently_open_file of - SOME f => (proper_inform_file_processed (File.platform_path f) - (Isar.state()); - currently_open_file := NONE) - | NONE => raise PGIP (" when no file is open!") - fun abortfile vs = case !currently_open_file of SOME f => (isarcmd "init_toplevel"; @@ -749,29 +784,8 @@ | NONE => inform_file_retracted (File.platform_path url) end -(* Path management: we allow theory files to have dependencies in - their own directory, but when we change directory for a new file we - remove the path. Leaving it there can cause confusion with - difference in batch mode. - NB: PGIP does not assume that the prover has a load path. -*) -local - val current_working_dir = ref (NONE : string option) -in -fun changecwd vs = - let - val url = #url vs - val newdir = File.platform_path url - in - (case (!current_working_dir) of - NONE => () - | SOME dir => ThyLoad.del_path dir; - ThyLoad.add_path newdir; - current_working_dir := SOME newdir) - end -end - +(*** System ***) fun systemcmd vs = let