Add abstraction for objtypes and documents.
--- 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$
--- 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"
+*)
--- 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
--- 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),
--- 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
| _ => ""
--- 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
--- 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
--- 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))))]
--- 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 ("<openfile> 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 ("<closefile> 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 ("<openfile> 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 ("<closefile> 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