1.1 --- a/src/Pure/Isar/locale.ML Wed Aug 27 11:49:50 2008 +0200
1.2 +++ b/src/Pure/Isar/locale.ML Wed Aug 27 12:00:28 2008 +0200
1.3 @@ -1595,10 +1595,10 @@
1.4 val id' = prep_id id
1.5 val eqns' = case get_reg id'
1.6 of NONE => eqns
1.7 - | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
1.8 + | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
1.9 handle Termtab.DUP t =>
1.10 - error ("Conflicting interpreting equations for term " ^
1.11 - quote (Syntax.string_of_term ctxt t))
1.12 + error ("Conflicting interpreting equations for term " ^
1.13 + quote (Syntax.string_of_term ctxt t))
1.14 in ((id', eqns'), eqns') end;
1.15
1.16
2.1 --- a/src/Pure/ProofGeneral/pgip_input.ML Wed Aug 27 11:49:50 2008 +0200
2.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML Wed Aug 27 12:00:28 2008 +0200
2.3 @@ -30,15 +30,15 @@
2.4 | Restoregoal of { thmname : string }
2.5 (* context inspection commands *)
2.6 | Askids of { url: PgipTypes.pgipurl option,
2.7 - thyname: PgipTypes.objname option,
2.8 - objtype: PgipTypes.objtype option }
2.9 + thyname: PgipTypes.objname option,
2.10 + objtype: PgipTypes.objtype option }
2.11 | Askrefs of { url: PgipTypes.pgipurl option,
2.12 - thyname: PgipTypes.objname option,
2.13 - objtype: PgipTypes.objtype option,
2.14 - name: PgipTypes.objname option }
2.15 + thyname: PgipTypes.objname option,
2.16 + objtype: PgipTypes.objtype option,
2.17 + name: PgipTypes.objname option }
2.18 | Showid of { thyname: PgipTypes.objname option,
2.19 - objtype: PgipTypes.objtype,
2.20 - name: PgipTypes.objname }
2.21 + objtype: PgipTypes.objtype,
2.22 + name: PgipTypes.objname }
2.23 | Askguise of { }
2.24 | Parsescript of { text: string, location: PgipTypes.location,
2.25 systemdata: string option }
2.26 @@ -74,59 +74,59 @@
2.27 (*** PGIP input ***)
2.28
2.29 datatype pgipinput =
2.30 - (* protocol/prover config *)
2.31 - Askpgip of { }
2.32 - | Askpgml of { }
2.33 - | Askconfig of { }
2.34 - | Askprefs of { }
2.35 - | Setpref of { name:string, prefcategory:string option, value:string }
2.36 - | Getpref of { name:string, prefcategory:string option }
2.37 + (* protocol/prover config *)
2.38 + Askpgip of { }
2.39 + | Askpgml of { }
2.40 + | Askconfig of { }
2.41 + | Askprefs of { }
2.42 + | Setpref of { name:string, prefcategory:string option, value:string }
2.43 + | Getpref of { name:string, prefcategory:string option }
2.44 (* prover control *)
2.45 - | Proverinit of { }
2.46 - | Proverexit of { }
2.47 + | Proverinit of { }
2.48 + | Proverexit of { }
2.49 | Setproverflag of { flagname:string, value: bool }
2.50 (* improper proof commands: control proof state *)
2.51 - | Dostep of { text: string }
2.52 - | Undostep of { times: int }
2.53 - | Redostep of { }
2.54 - | Abortgoal of { }
2.55 - | Forget of { thyname: string option, name: string option,
2.56 - objtype: PgipTypes.objtype option }
2.57 + | Dostep of { text: string }
2.58 + | Undostep of { times: int }
2.59 + | Redostep of { }
2.60 + | Abortgoal of { }
2.61 + | Forget of { thyname: string option, name: string option,
2.62 + objtype: PgipTypes.objtype option }
2.63 | Restoregoal of { thmname : string }
2.64 (* context inspection commands *)
2.65 | Askids of { url: PgipTypes.pgipurl option,
2.66 - thyname: PgipTypes.objname option,
2.67 - objtype: PgipTypes.objtype option }
2.68 + thyname: PgipTypes.objname option,
2.69 + objtype: PgipTypes.objtype option }
2.70 | Askrefs of { url: PgipTypes.pgipurl option,
2.71 - thyname: PgipTypes.objname option,
2.72 - objtype: PgipTypes.objtype option,
2.73 - name: PgipTypes.objname option }
2.74 + thyname: PgipTypes.objname option,
2.75 + objtype: PgipTypes.objtype option,
2.76 + name: PgipTypes.objname option }
2.77 | Showid of { thyname: PgipTypes.objname option,
2.78 - objtype: PgipTypes.objtype,
2.79 - name: PgipTypes.objname }
2.80 - | Askguise of { }
2.81 - | Parsescript of { text: string, location: location,
2.82 - systemdata: string option }
2.83 + objtype: PgipTypes.objtype,
2.84 + name: PgipTypes.objname }
2.85 + | Askguise of { }
2.86 + | Parsescript of { text: string, location: location,
2.87 + systemdata: string option }
2.88 | Showproofstate of { }
2.89 - | Showctxt of { }
2.90 + | Showctxt of { }
2.91 | Searchtheorems of { arg: string }
2.92 | Setlinewidth of { width: int }
2.93 - | Viewdoc of { arg: string }
2.94 + | Viewdoc of { arg: string }
2.95 (* improper theory-level commands *)
2.96 - | Doitem of { text: string }
2.97 - | Undoitem of { }
2.98 - | Redoitem of { }
2.99 - | Aborttheory of { }
2.100 + | Doitem of { text: string }
2.101 + | Undoitem of { }
2.102 + | Redoitem of { }
2.103 + | Aborttheory of { }
2.104 | Retracttheory of { thyname: string }
2.105 - | Loadfile of { url: pgipurl }
2.106 - | Openfile of { url: pgipurl }
2.107 - | Closefile of { }
2.108 - | Abortfile of { }
2.109 + | Loadfile of { url: pgipurl }
2.110 + | Openfile of { url: pgipurl }
2.111 + | Closefile of { }
2.112 + | Abortfile of { }
2.113 | Retractfile of { url: pgipurl }
2.114 - | Changecwd of { url: pgipurl }
2.115 - | Systemcmd of { arg: string }
2.116 + | Changecwd of { url: pgipurl }
2.117 + | Systemcmd of { arg: string }
2.118 (* unofficial escape command for debugging *)
2.119 - | Quitpgip of { }
2.120 + | Quitpgip of { }
2.121
2.122 (* Extracting content from input XML elements to make a PGIPinput *)
2.123 local
2.124 @@ -140,12 +140,12 @@
2.125 val value_attr = get_attr "value"
2.126
2.127 fun objtype_attro attrs = if has_attr "objtype" attrs then
2.128 - SOME (objtype_of_attrs attrs)
2.129 - else NONE
2.130 + SOME (objtype_of_attrs attrs)
2.131 + else NONE
2.132
2.133 fun pgipurl_attro attrs = if has_attr "url" attrs then
2.134 - SOME (pgipurl_of_attrs attrs)
2.135 - else NONE
2.136 + SOME (pgipurl_of_attrs attrs)
2.137 + else NONE
2.138
2.139 val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
2.140 val prefcat_attr = get_attr_opt "prefcategory"
2.141 @@ -171,39 +171,39 @@
2.142 (* proverconfig *)
2.143 | "askprefs" => Askprefs { }
2.144 | "getpref" => Getpref { name = name_attr attrs,
2.145 - prefcategory = prefcat_attr attrs }
2.146 + prefcategory = prefcat_attr attrs }
2.147 | "setpref" => Setpref { name = name_attr attrs,
2.148 - prefcategory = prefcat_attr attrs,
2.149 - value = xmltext data }
2.150 + prefcategory = prefcat_attr attrs,
2.151 + value = xmltext data }
2.152 (* provercontrol *)
2.153 | "proverinit" => Proverinit { }
2.154 | "proverexit" => Proverexit { }
2.155 | "setproverflag" => Setproverflag { flagname = flagname_attr attrs,
2.156 - value = read_pgipbool (value_attr attrs) }
2.157 + value = read_pgipbool (value_attr attrs) }
2.158 (* improperproofcmd: improper commands not in script *)
2.159 | "dostep" => Dostep { text = xmltext data }
2.160 | "undostep" => Undostep { times = times_attr attrs }
2.161 | "redostep" => Redostep { }
2.162 | "abortgoal" => Abortgoal { }
2.163 | "forget" => Forget { thyname = thyname_attro attrs,
2.164 - name = name_attro attrs,
2.165 - objtype = objtype_attro attrs }
2.166 + name = name_attro attrs,
2.167 + objtype = objtype_attro attrs }
2.168 | "restoregoal" => Restoregoal { thmname = thmname_attr attrs}
2.169 (* proofctxt: improper commands *)
2.170 | "askids" => Askids { url = pgipurl_attro attrs,
2.171 - thyname = thyname_attro attrs,
2.172 - objtype = objtype_attro attrs }
2.173 + thyname = thyname_attro attrs,
2.174 + objtype = objtype_attro attrs }
2.175 | "askrefs" => Askrefs { url = pgipurl_attro attrs,
2.176 - thyname = thyname_attro attrs,
2.177 - objtype = objtype_attro attrs,
2.178 - name = name_attro attrs }
2.179 + thyname = thyname_attro attrs,
2.180 + objtype = objtype_attro attrs,
2.181 + name = name_attro attrs }
2.182 | "showid" => Showid { thyname = thyname_attro attrs,
2.183 - objtype = objtype_of_attrs attrs,
2.184 - name = name_attr attrs }
2.185 + objtype = objtype_of_attrs attrs,
2.186 + name = name_attr attrs }
2.187 | "askguise" => Askguise { }
2.188 | "parsescript" => Parsescript { text = (xmltext data),
2.189 - systemdata = get_attr_opt "systemdata" attrs,
2.190 - location = location_of_attrs attrs }
2.191 + systemdata = get_attr_opt "systemdata" attrs,
2.192 + location = location_of_attrs attrs }
2.193 | "showproofstate" => Showproofstate { }
2.194 | "showctxt" => Showctxt { }
2.195 | "searchtheorems" => Searchtheorems { arg = xmltext data }
2.196 @@ -223,17 +223,17 @@
2.197 | "changecwd" => Changecwd { url = pgipurl_of_attrs attrs }
2.198 | "systemcmd" => Systemcmd { arg = xmltext data }
2.199 (* unofficial command for debugging *)
2.200 - | "quitpgip" => Quitpgip { }
2.201 + | "quitpgip" => Quitpgip { }
2.202
2.203 (* We allow sending proper document markup too; we map it back to dostep *)
2.204 (* and strip out metainfo elements. Markup correctness isn't checked: this *)
2.205 (* is a compatibility measure to make it easy for interfaces. *)
2.206 | x => if (x mem PgipMarkup.doc_markup_elements) then
2.207 - if (x mem PgipMarkup.doc_markup_elements_ignored) then
2.208 - raise NoAction
2.209 - else
2.210 - Dostep { text = xmltext data } (* could separate out Doitem too *)
2.211 - else raise Unknown)
2.212 + if (x mem PgipMarkup.doc_markup_elements_ignored) then
2.213 + raise NoAction
2.214 + else
2.215 + Dostep { text = xmltext data } (* could separate out Doitem too *)
2.216 + else raise Unknown)
2.217 handle Unknown => NONE | NoAction => NONE
2.218 end
2.219
3.1 --- a/src/Pure/ProofGeneral/pgip_output.ML Wed Aug 27 11:49:50 2008 +0200
3.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML Wed Aug 27 12:00:28 2008 +0200
3.3 @@ -32,21 +32,21 @@
3.4 prefs: PgipTypes.preference list }
3.5 | Prefval of { name: string, value: string }
3.6 | Setrefs of { url: PgipTypes.pgipurl option,
3.7 - thyname: PgipTypes.objname option,
3.8 - objtype: PgipTypes.objtype option,
3.9 - name: PgipTypes.objname option,
3.10 - idtables: PgipTypes.idtable list,
3.11 - fileurls : PgipTypes.pgipurl list }
3.12 + thyname: PgipTypes.objname option,
3.13 + objtype: PgipTypes.objtype option,
3.14 + name: PgipTypes.objname option,
3.15 + idtables: PgipTypes.idtable list,
3.16 + fileurls : PgipTypes.pgipurl list }
3.17 | Idvalue of { thyname: PgipTypes.objname option,
3.18 - objtype: PgipTypes.objtype,
3.19 - name: PgipTypes.objname,
3.20 - text: XML.tree list }
3.21 + objtype: PgipTypes.objtype,
3.22 + name: PgipTypes.objname,
3.23 + text: XML.tree list }
3.24 | Informguise of { file : PgipTypes.pgipurl option,
3.25 theory: PgipTypes.objname option,
3.26 theorem: PgipTypes.objname option,
3.27 proofpos: int option }
3.28 | Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument,
3.29 - errs: XML.tree list } (* errs to become PGML *)
3.30 + errs: XML.tree list } (* errs to become PGML *)
3.31 | Usespgip of { version: string,
3.32 pgipelems: (string * bool * string list) list }
3.33 | Usespgml of { version: string }
3.34 @@ -67,10 +67,10 @@
3.35 open PgipTypes
3.36
3.37 datatype pgipoutput =
3.38 - Normalresponse of { content: XML.tree list }
3.39 + Normalresponse of { content: XML.tree list }
3.40 | Errorresponse of { fatality: fatality,
3.41 location: location option,
3.42 - content: XML.tree list }
3.43 + content: XML.tree list }
3.44 | Informfileloaded of { url: Path.T, completed: bool }
3.45 | Informfileoutdated of { url: Path.T, completed: bool }
3.46 | Informfileretracted of { url: Path.T, completed: bool }
3.47 @@ -84,21 +84,21 @@
3.48 | Hasprefs of { prefcategory: string option, prefs: preference list }
3.49 | Prefval of { name: string, value: string }
3.50 | Idvalue of { thyname: PgipTypes.objname option,
3.51 - objtype: PgipTypes.objtype,
3.52 - name: PgipTypes.objname,
3.53 - text: XML.tree list }
3.54 + objtype: PgipTypes.objtype,
3.55 + name: PgipTypes.objname,
3.56 + text: XML.tree list }
3.57 | Setrefs of { url: PgipTypes.pgipurl option,
3.58 - thyname: PgipTypes.objname option,
3.59 - objtype: PgipTypes.objtype option,
3.60 - name: PgipTypes.objname option,
3.61 - idtables: PgipTypes.idtable list,
3.62 - fileurls : PgipTypes.pgipurl list }
3.63 + thyname: PgipTypes.objname option,
3.64 + objtype: PgipTypes.objtype option,
3.65 + name: PgipTypes.objname option,
3.66 + idtables: PgipTypes.idtable list,
3.67 + fileurls : PgipTypes.pgipurl list }
3.68 | Informguise of { file : PgipTypes.pgipurl option,
3.69 - theory: PgipTypes.objname option,
3.70 - theorem: PgipTypes.objname option,
3.71 - proofpos: int option }
3.72 + theory: PgipTypes.objname option,
3.73 + theorem: PgipTypes.objname option,
3.74 + proofpos: int option }
3.75 | Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
3.76 - errs: XML.tree list } (* errs to become PGML *)
3.77 + errs: XML.tree list } (* errs to become PGML *)
3.78 | Usespgip of { version: string,
3.79 pgipelems: (string * bool * string list) list }
3.80 | Usespgml of { version: string }
3.81 @@ -119,7 +119,7 @@
3.82 val content = #content vs
3.83 in
3.84 XML.Elem ("normalresponse",
3.85 - [],
3.86 + [],
3.87 content)
3.88 end
3.89
3.90 @@ -141,9 +141,9 @@
3.91 val completed = #completed vs
3.92 in
3.93 XML.Elem ("informfileloaded",
3.94 - attrs_of_pgipurl url @
3.95 - (attr "completed" (PgipTypes.bool_to_pgstring completed)),
3.96 - [])
3.97 + attrs_of_pgipurl url @
3.98 + (attr "completed" (PgipTypes.bool_to_pgstring completed)),
3.99 + [])
3.100 end
3.101
3.102 fun informfileoutdated (Informfileoutdated vs) =
3.103 @@ -152,9 +152,9 @@
3.104 val completed = #completed vs
3.105 in
3.106 XML.Elem ("informfileoutdated",
3.107 - attrs_of_pgipurl url @
3.108 - (attr "completed" (PgipTypes.bool_to_pgstring completed)),
3.109 - [])
3.110 + attrs_of_pgipurl url @
3.111 + (attr "completed" (PgipTypes.bool_to_pgstring completed)),
3.112 + [])
3.113 end
3.114
3.115 fun informfileretracted (Informfileretracted vs) =
3.116 @@ -163,9 +163,9 @@
3.117 val completed = #completed vs
3.118 in
3.119 XML.Elem ("informfileretracted",
3.120 - attrs_of_pgipurl url @
3.121 - (attr "completed" (PgipTypes.bool_to_pgstring completed)),
3.122 - [])
3.123 + attrs_of_pgipurl url @
3.124 + (attr "completed" (PgipTypes.bool_to_pgstring completed)),
3.125 + [])
3.126 end
3.127
3.128 fun metainforesponse (Metainforesponse vs) =
3.129 @@ -211,21 +211,21 @@
3.130
3.131 fun setrefs (Setrefs vs) =
3.132 let
3.133 - val url = #url vs
3.134 - val thyname = #thyname vs
3.135 - val objtype = #objtype vs
3.136 - val name = #name vs
3.137 + val url = #url vs
3.138 + val thyname = #thyname vs
3.139 + val objtype = #objtype vs
3.140 + val name = #name vs
3.141 val idtables = #idtables vs
3.142 val fileurls = #fileurls vs
3.143 - fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
3.144 + fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
3.145 in
3.146 XML.Elem ("setrefs",
3.147 - (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @
3.148 - (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
3.149 - (opt_attr "thyname" thyname) @
3.150 - (opt_attr "name" name),
3.151 - (map idtable_to_xml idtables) @
3.152 - (map fileurl_to_xml fileurls))
3.153 + (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @
3.154 + (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
3.155 + (opt_attr "thyname" thyname) @
3.156 + (opt_attr "name" name),
3.157 + (map idtable_to_xml idtables) @
3.158 + (map fileurl_to_xml fileurls))
3.159 end
3.160
3.161 fun addids (Addids vs) =
3.162 @@ -260,16 +260,16 @@
3.163
3.164 fun idvalue (Idvalue vs) =
3.165 let
3.166 - val objtype_attrs = attrs_of_objtype (#objtype vs)
3.167 - val thyname = #thyname vs
3.168 + val objtype_attrs = attrs_of_objtype (#objtype vs)
3.169 + val thyname = #thyname vs
3.170 val name = #name vs
3.171 val text = #text vs
3.172 in
3.173 XML.Elem("idvalue",
3.174 - objtype_attrs @
3.175 - (opt_attr "thyname" thyname) @
3.176 - (attr "name" name),
3.177 - text)
3.178 + objtype_attrs @
3.179 + (opt_attr "thyname" thyname) @
3.180 + (attr "name" name),
3.181 + text)
3.182 end
3.183
3.184 fun informguise (Informguise vs) =
3.185 @@ -295,7 +295,7 @@
3.186 val attrs = #attrs vs
3.187 val doc = #doc vs
3.188 val errs = #errs vs
3.189 - val xmldoc = PgipMarkup.output_doc doc
3.190 + val xmldoc = PgipMarkup.output_doc doc
3.191 in
3.192 XML.Elem("parseresult", attrs, errs @ xmldoc)
3.193 end
4.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML Wed Aug 27 11:49:50 2008 +0200
4.2 +++ b/src/Pure/ProofGeneral/pgip_tests.ML Wed Aug 27 12:00:28 2008 +0200
4.3 @@ -12,7 +12,7 @@
4.4 fun asseq_p toS a b =
4.5 if a=b then ()
4.6 else error("PGIP test: expected these two values to be equal:\n" ^
4.7 - (toS a) ^"\n and: \n" ^ (toS b))
4.8 + (toS a) ^"\n and: \n" ^ (toS b))
4.9
4.10 val asseqx = asseq_p XML.string_of
4.11 val asseqs = asseq_p I
4.12 @@ -40,18 +40,18 @@
4.13
4.14 local
4.15 val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat),
4.16 - Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
4.17 + Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
4.18 in
4.19 val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45";
4.20 val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo";
4.21 val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true";
4.22 val _ = asseqs (pgval_to_string (read_pgval choices "")) "";
4.23 val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37";
4.24 - error "pgip_tests: should fail") handle PGIP _ => ()
4.25 + error "pgip_tests: should fail") handle PGIP _ => ()
4.26 end
4.27
4.28 val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
4.29 - default=SOME "true", pgiptype=Pgipbool})
4.30 + default=SOME "true", pgiptype=Pgipbool})
4.31 (XML.parse "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
4.32 end
4.33
4.34 @@ -60,8 +60,8 @@
4.35 local
4.36
4.37 fun e str = case XML.parse str of
4.38 - (XML.Elem args) => args
4.39 - | _ => error("Expected to get an XML Element")
4.40 + (XML.Elem args) => args
4.41 + | _ => error("Expected to get an XML Element")
4.42
4.43 open PgipInput;
4.44 open PgipTypes;
4.45 @@ -83,7 +83,7 @@
4.46 val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
4.47 *)
4.48 val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
4.49 - objtype=SOME ObjTheory,name=NONE}));
4.50 + objtype=SOME ObjTheory,name=NONE}));
4.51 val _ = asseqi "<otherelt/>" NONE;
4.52
4.53 end
5.1 --- a/src/Pure/ProofGeneral/pgip_types.ML Wed Aug 27 11:49:50 2008 +0200
5.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML Wed Aug 27 12:00:28 2008 +0200
5.3 @@ -11,7 +11,7 @@
5.4 (* Object types: the types of values which can be manipulated externally.
5.5 Ideally a list of other types would be configured as a parameter. *)
5.6 datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment
5.7 - | ObjTerm | ObjType | ObjOther of string
5.8 + | ObjTerm | ObjType | ObjOther of string
5.9
5.10 (* Names for values of objtypes (i.e. prover identifiers). Could be a parameter.
5.11 Names for ObjFiles are URIs. *)
5.12 @@ -24,7 +24,7 @@
5.13 (* Types and values (used for preferences and dialogs) *)
5.14
5.15 datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat
5.16 - | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
5.17 + | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
5.18
5.19 and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *)
5.20
5.21 @@ -44,17 +44,17 @@
5.22
5.23 (* File location *)
5.24 type location = { descr: string option,
5.25 - url: pgipurl option,
5.26 - line: int option,
5.27 - column: int option,
5.28 - char: int option,
5.29 - length: int option }
5.30 + url: pgipurl option,
5.31 + line: int option,
5.32 + column: int option,
5.33 + char: int option,
5.34 + length: int option }
5.35
5.36 (* Prover preference *)
5.37 type preference = { name: string,
5.38 - descr: string option,
5.39 - default: string option,
5.40 - pgiptype: pgiptype }
5.41 + descr: string option,
5.42 + default: string option,
5.43 + pgiptype: pgiptype }
5.44 end
5.45
5.46 signature PGIPTYPES_OPNS =
5.47 @@ -64,21 +64,21 @@
5.48 (* Object types *)
5.49 val name_of_objtype : objtype -> string
5.50 val attrs_of_objtype : objtype -> XML.attributes
5.51 - val objtype_of_attrs : XML.attributes -> objtype (* raises PGIP *)
5.52 + val objtype_of_attrs : XML.attributes -> objtype (* raises PGIP *)
5.53 val idtable_to_xml : idtable -> XML.tree
5.54
5.55 (* Values as XML strings *)
5.56 - val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *)
5.57 - val read_pgipnat : string -> int (* raises PGIP *)
5.58 - val read_pgipbool : string -> bool (* raises PGIP *)
5.59 - val read_pgipstring : string -> string (* raises PGIP *)
5.60 - val int_to_pgstring : int -> string
5.61 + val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *)
5.62 + val read_pgipnat : string -> int (* raises PGIP *)
5.63 + val read_pgipbool : string -> bool (* raises PGIP *)
5.64 + val read_pgipstring : string -> string (* raises PGIP *)
5.65 + val int_to_pgstring : int -> string
5.66 val bool_to_pgstring : bool -> string
5.67 val string_to_pgstring : string -> string
5.68
5.69 (* PGIP datatypes *)
5.70 val pgiptype_to_xml : pgiptype -> XML.tree
5.71 - val read_pgval : pgiptype -> string -> pgipval (* raises PGIP *)
5.72 + val read_pgval : pgiptype -> string -> pgipval (* raises PGIP *)
5.73 val pgval_to_string : pgipval -> string
5.74
5.75 val attrs_of_displayarea : displayarea -> XML.attributes
5.76 @@ -88,8 +88,8 @@
5.77
5.78 val haspref : preference -> XML.tree
5.79
5.80 - val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *)
5.81 - val pgipurl_of_string : string -> pgipurl (* raises PGIP *)
5.82 + val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *)
5.83 + val pgipurl_of_string : string -> pgipurl (* raises PGIP *)
5.84 val pgipurl_of_path : Path.T -> pgipurl
5.85 val path_of_pgipurl : pgipurl -> Path.T
5.86 val string_of_pgipurl : pgipurl -> string
5.87 @@ -98,7 +98,7 @@
5.88
5.89 (* XML utils, only for PGIP code *)
5.90 val has_attr : string -> XML.attributes -> bool
5.91 - val attr : string -> string -> XML.attributes
5.92 + val attr : string -> string -> XML.attributes
5.93 val opt_attr : string -> string option -> XML.attributes
5.94 val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes
5.95 val get_attr : string -> XML.attributes -> string (* raises PGIP *)
5.96 @@ -137,11 +137,11 @@
5.97 (** Objtypes **)
5.98
5.99 datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment
5.100 - | ObjTerm | ObjType | ObjOther of string
5.101 + | ObjTerm | ObjType | ObjOther of string
5.102
5.103 fun name_of_objtype obj =
5.104 case obj of
5.105 - ObjFile => "file"
5.106 + ObjFile => "file"
5.107 | ObjTheory => "theory"
5.108 | ObjTheorem => "theorem"
5.109 | ObjComment => "comment"
5.110 @@ -183,7 +183,7 @@
5.111
5.112 fun read_pgipbool s =
5.113 (case s of
5.114 - "false" => false
5.115 + "false" => false
5.116 | "true" => true
5.117 | _ => raise PGIP ("Invalid boolean value: " ^ quote s))
5.118
5.119 @@ -195,21 +195,21 @@
5.120 in
5.121 fun read_pgipint range s =
5.122 (case Int.fromString s of
5.123 - SOME i => if int_in_range range i then i
5.124 - else raise PGIP ("Out of range integer value: " ^ quote s)
5.125 + SOME i => if int_in_range range i then i
5.126 + else raise PGIP ("Out of range integer value: " ^ quote s)
5.127 | NONE => raise PGIP ("Invalid integer value: " ^ quote s))
5.128 end;
5.129
5.130 fun read_pgipnat s =
5.131 (case Int.fromString s of
5.132 - SOME i => if i >= 0 then i
5.133 + SOME i => if i >= 0 then i
5.134 else raise PGIP ("Invalid natural number: " ^ quote s)
5.135 | NONE => raise PGIP ("Invalid natural number: " ^ quote s))
5.136
5.137 (* NB: we can maybe do without xml decode/encode here. *)
5.138 fun read_pgipstring s = (* non-empty strings, XML escapes decoded *)
5.139 (case XML.parse_string s of
5.140 - SOME s => s
5.141 + SOME s => s
5.142 | NONE => raise PGIP ("Expected a non-empty string: " ^ quote s))
5.143 handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s)
5.144
5.145 @@ -237,53 +237,53 @@
5.146
5.147
5.148 datatype pgiptype =
5.149 - Pgipnull (* unit type: unique element is empty string *)
5.150 - | Pgipbool (* booleans: "true" or "false" *)
5.151 + Pgipnull (* unit type: unique element is empty string *)
5.152 + | Pgipbool (* booleans: "true" or "false" *)
5.153 | Pgipint of int option * int option (* ranged integers, should be XSD canonical *)
5.154 - | Pgipnat (* naturals: non-negative integers (convenience) *)
5.155 - | Pgipstring (* non-empty strings *)
5.156 - | Pgipconst of string (* singleton type *)
5.157 - | Pgipchoice of pgipdtype list (* union type *)
5.158 + | Pgipnat (* naturals: non-negative integers (convenience) *)
5.159 + | Pgipstring (* non-empty strings *)
5.160 + | Pgipconst of string (* singleton type *)
5.161 + | Pgipchoice of pgipdtype list (* union type *)
5.162
5.163 (* Compared with the PGIP schema, we push descriptions of types inside choices. *)
5.164
5.165 and pgipdtype = Pgipdtype of string option * pgiptype
5.166
5.167 datatype pgipuval = Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int
5.168 - | Pgvalstring of string | Pgvalconst of string
5.169 + | Pgvalstring of string | Pgvalconst of string
5.170
5.171 -type pgipval = pgiptype * pgipuval (* type-safe values *)
5.172 +type pgipval = pgiptype * pgipuval (* type-safe values *)
5.173
5.174 fun pgipdtype_to_xml (desco,ty) =
5.175 let
5.176 - val desc_attr = opt_attr "descr" desco
5.177 + val desc_attr = opt_attr "descr" desco
5.178
5.179 - val elt = case ty of
5.180 - Pgipnull => "pgipnull"
5.181 - | Pgipbool => "pgipbool"
5.182 - | Pgipint _ => "pgipint"
5.183 - | Pgipnat => "pgipint"
5.184 - | Pgipstring => "pgipstring"
5.185 - | Pgipconst _ => "pgipconst"
5.186 - | Pgipchoice _ => "pgipchoice"
5.187 + val elt = case ty of
5.188 + Pgipnull => "pgipnull"
5.189 + | Pgipbool => "pgipbool"
5.190 + | Pgipint _ => "pgipint"
5.191 + | Pgipnat => "pgipint"
5.192 + | Pgipstring => "pgipstring"
5.193 + | Pgipconst _ => "pgipconst"
5.194 + | Pgipchoice _ => "pgipchoice"
5.195
5.196 - fun range_attr r v = attr r (int_to_pgstring v)
5.197 + fun range_attr r v = attr r (int_to_pgstring v)
5.198
5.199 - val attrs = case ty of
5.200 - Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)
5.201 - | Pgipint (SOME min,NONE) => (range_attr "min" min)
5.202 - | Pgipint (NONE,SOME max) => (range_attr "max" max)
5.203 - | Pgipnat => (range_attr "min" 0)
5.204 - | Pgipconst nm => attr "name" nm
5.205 - | _ => []
5.206 + val attrs = case ty of
5.207 + Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)
5.208 + | Pgipint (SOME min,NONE) => (range_attr "min" min)
5.209 + | Pgipint (NONE,SOME max) => (range_attr "max" max)
5.210 + | Pgipnat => (range_attr "min" 0)
5.211 + | Pgipconst nm => attr "name" nm
5.212 + | _ => []
5.213
5.214 - fun destpgipdtype (Pgipdtype x) = x
5.215 + fun destpgipdtype (Pgipdtype x) = x
5.216
5.217 - val typargs = case ty of
5.218 - Pgipchoice ds => map destpgipdtype ds
5.219 - | _ => []
5.220 + val typargs = case ty of
5.221 + Pgipchoice ds => map destpgipdtype ds
5.222 + | _ => []
5.223 in
5.224 - XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
5.225 + XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
5.226 end
5.227
5.228 val pgiptype_to_xml = pgipdtype_to_xml o pair NONE
5.229 @@ -302,18 +302,18 @@
5.230 else raise PGIP ("Expecting non-empty string, empty string illegal.")
5.231 | read_pguval (Pgipchoice tydescs) s =
5.232 let
5.233 - (* Union type: match first in list *)
5.234 - fun getty (Pgipdtype(_, ty)) = ty
5.235 - val uval = get_first
5.236 - (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
5.237 - (map getty tydescs)
5.238 + (* Union type: match first in list *)
5.239 + fun getty (Pgipdtype(_, ty)) = ty
5.240 + val uval = get_first
5.241 + (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
5.242 + (map getty tydescs)
5.243 in
5.244 - case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^
5.245 - " against any allowed types.")
5.246 + case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^
5.247 + " against any allowed types.")
5.248 end
5.249
5.250 fun read_pgval ty s = (ty, read_pguval ty s)
5.251 -
5.252 +
5.253 fun pgval_to_string (_, Pgvalnull) = ""
5.254 | pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b
5.255 | pgval_to_string (_, Pgvalnat n) = int_to_pgstring n
5.256 @@ -329,11 +329,11 @@
5.257 datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug
5.258
5.259 type location = { descr: string option,
5.260 - url: pgipurl option,
5.261 - line: int option,
5.262 - column: int option,
5.263 - char: int option,
5.264 - length: int option }
5.265 + url: pgipurl option,
5.266 + line: int option,
5.267 + column: int option,
5.268 + char: int option,
5.269 + length: int option }
5.270
5.271
5.272
5.273 @@ -341,10 +341,10 @@
5.274
5.275
5.276 fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
5.277 - case Url.explode url of
5.278 + case Url.explode url of
5.279 (Url.File path) => path
5.280 - | _ => raise PGIP ("Cannot access non-local URL " ^ quote url)
5.281 -
5.282 + | _ => raise PGIP ("Cannot access non-local URL " ^ quote url)
5.283 +
5.284 fun pgipurl_of_path p = p
5.285
5.286 fun path_of_pgipurl p = p (* potentially raises PGIP, but not with this implementation *)
5.287 @@ -385,51 +385,51 @@
5.288
5.289 fun attrs_of_location ({ descr, url, line, column, char, length }:location) =
5.290 let
5.291 - val descr = opt_attr "location_descr" descr
5.292 - val url = opt_attr_map attrval_of_pgipurl "location_url" url
5.293 - val line = opt_attr_map int_to_pgstring "locationline" line
5.294 - val column = opt_attr_map int_to_pgstring "locationcolumn" column
5.295 - val char = opt_attr_map int_to_pgstring "locationcharacter" char
5.296 - val length = opt_attr_map int_to_pgstring "locationlength" length
5.297 + val descr = opt_attr "location_descr" descr
5.298 + val url = opt_attr_map attrval_of_pgipurl "location_url" url
5.299 + val line = opt_attr_map int_to_pgstring "locationline" line
5.300 + val column = opt_attr_map int_to_pgstring "locationcolumn" column
5.301 + val char = opt_attr_map int_to_pgstring "locationcharacter" char
5.302 + val length = opt_attr_map int_to_pgstring "locationlength" length
5.303 in
5.304 - descr @ url @ line @ column @ char @ length
5.305 + descr @ url @ line @ column @ char @ length
5.306 end
5.307
5.308 fun pgipint_of_string err s =
5.309 - case Int.fromString s of
5.310 - SOME i => i
5.311 - | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.")
5.312 + case Int.fromString s of
5.313 + SOME i => i
5.314 + | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.")
5.315
5.316 fun location_of_attrs attrs =
5.317 let
5.318 - val descr = get_attr_opt "location_descr" attrs
5.319 - val url = Option.map pgipurl_of_string (get_attr_opt "location_url" attrs)
5.320 - val line = Option.map (pgipint_of_string "location element line attribute")
5.321 - (get_attr_opt "locationline" attrs)
5.322 - val column = Option.map (pgipint_of_string "location element column attribute")
5.323 - (get_attr_opt "locationcolumn" attrs)
5.324 - val char = Option.map (pgipint_of_string "location element char attribute")
5.325 - (get_attr_opt "locationcharacter" attrs)
5.326 - val length = Option.map (pgipint_of_string "location element length attribute")
5.327 - (get_attr_opt "locationlength" attrs)
5.328 + val descr = get_attr_opt "location_descr" attrs
5.329 + val url = Option.map pgipurl_of_string (get_attr_opt "location_url" attrs)
5.330 + val line = Option.map (pgipint_of_string "location element line attribute")
5.331 + (get_attr_opt "locationline" attrs)
5.332 + val column = Option.map (pgipint_of_string "location element column attribute")
5.333 + (get_attr_opt "locationcolumn" attrs)
5.334 + val char = Option.map (pgipint_of_string "location element char attribute")
5.335 + (get_attr_opt "locationcharacter" attrs)
5.336 + val length = Option.map (pgipint_of_string "location element length attribute")
5.337 + (get_attr_opt "locationlength" attrs)
5.338 in
5.339 - {descr=descr, url=url, line=line, column=column, char=char, length=length}
5.340 + {descr=descr, url=url, line=line, column=column, char=char, length=length}
5.341 end
5.342 end
5.343
5.344 (** Preferences **)
5.345
5.346 type preference = { name: string,
5.347 - descr: string option,
5.348 - default: string option,
5.349 - pgiptype: pgiptype }
5.350 + descr: string option,
5.351 + default: string option,
5.352 + pgiptype: pgiptype }
5.353
5.354 fun haspref ({ name, descr, default, pgiptype}:preference) =
5.355 XML.Elem ("haspref",
5.356 - attr "name" name @
5.357 - opt_attr "descr" descr @
5.358 - opt_attr "default" default,
5.359 - [pgiptype_to_xml pgiptype])
5.360 + attr "name" name @
5.361 + opt_attr "descr" descr @
5.362 + opt_attr "default" default,
5.363 + [pgiptype_to_xml pgiptype])
5.364
5.365 end
5.366
6.1 --- a/src/Pure/ProofGeneral/pgml.ML Wed Aug 27 11:49:50 2008 +0200
6.2 +++ b/src/Pure/ProofGeneral/pgml.ML Wed Aug 27 12:00:28 2008 +0200
6.3 @@ -18,29 +18,29 @@
6.4 datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
6.5
6.6 datatype pgmlaction = Toggle | Button | Menu
6.7 -
6.8 +
6.9 datatype pgmlterm =
6.10 - Atoms of { kind: string option, content: pgmlatom list }
6.11 - | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
6.12 - | Break of { mandatory: bool option, indent: int option }
6.13 - | Subterm of { kind: string option,
6.14 - param: string option,
6.15 - place: pgmlplace option,
6.16 - name: string option,
6.17 - decoration: pgmldec option,
6.18 - action: pgmlaction option,
6.19 - pos: string option,
6.20 - xref: PgipTypes.pgipurl option,
6.21 - content: pgmlterm list }
6.22 - | Alt of { kind: string option, content: pgmlterm list }
6.23 - | Embed of XML.tree list
6.24 - | Raw of XML.tree
6.25 + Atoms of { kind: string option, content: pgmlatom list }
6.26 + | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
6.27 + | Break of { mandatory: bool option, indent: int option }
6.28 + | Subterm of { kind: string option,
6.29 + param: string option,
6.30 + place: pgmlplace option,
6.31 + name: string option,
6.32 + decoration: pgmldec option,
6.33 + action: pgmlaction option,
6.34 + pos: string option,
6.35 + xref: PgipTypes.pgipurl option,
6.36 + content: pgmlterm list }
6.37 + | Alt of { kind: string option, content: pgmlterm list }
6.38 + | Embed of XML.tree list
6.39 + | Raw of XML.tree
6.40
6.41 datatype pgml =
6.42 - Pgml of { version: string option, systemid: string option,
6.43 - area: PgipTypes.displayarea option,
6.44 - content: pgmlterm list }
6.45 -
6.46 + Pgml of { version: string option, systemid: string option,
6.47 + area: PgipTypes.displayarea option,
6.48 + content: pgmlterm list }
6.49 +
6.50 val pgmlterm_to_xml : pgmlterm -> XML.tree
6.51
6.52 val pgml_to_xml : pgml -> XML.tree
6.53 @@ -62,29 +62,29 @@
6.54 datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
6.55
6.56 datatype pgmlaction = Toggle | Button | Menu
6.57 -
6.58 +
6.59 datatype pgmlterm =
6.60 - Atoms of { kind: string option, content: pgmlatom list }
6.61 - | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
6.62 - | Break of { mandatory: bool option, indent: int option }
6.63 - | Subterm of { kind: string option,
6.64 - param: string option,
6.65 - place: pgmlplace option,
6.66 - name: string option,
6.67 - decoration: pgmldec option,
6.68 - action: pgmlaction option,
6.69 - pos: string option,
6.70 - xref: PgipTypes.pgipurl option,
6.71 - content: pgmlterm list }
6.72 - | Alt of { kind: string option, content: pgmlterm list }
6.73 - | Embed of XML.tree list
6.74 - | Raw of XML.tree
6.75 + Atoms of { kind: string option, content: pgmlatom list }
6.76 + | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
6.77 + | Break of { mandatory: bool option, indent: int option }
6.78 + | Subterm of { kind: string option,
6.79 + param: string option,
6.80 + place: pgmlplace option,
6.81 + name: string option,
6.82 + decoration: pgmldec option,
6.83 + action: pgmlaction option,
6.84 + pos: string option,
6.85 + xref: PgipTypes.pgipurl option,
6.86 + content: pgmlterm list }
6.87 + | Alt of { kind: string option, content: pgmlterm list }
6.88 + | Embed of XML.tree list
6.89 + | Raw of XML.tree
6.90
6.91 -
6.92 +
6.93 datatype pgml =
6.94 - Pgml of { version: string option, systemid: string option,
6.95 - area: PgipTypes.displayarea option,
6.96 - content: pgmlterm list }
6.97 + Pgml of { version: string option, systemid: string option,
6.98 + area: PgipTypes.displayarea option,
6.99 + content: pgmlterm list }
6.100
6.101 fun pgmlorient_to_string HOVOrient = "hov"
6.102 | pgmlorient_to_string HOrient = "h"
6.103 @@ -111,35 +111,35 @@
6.104 would be better not to *)
6.105 fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content])
6.106 | atom_to_xml (Str str) = XML.Output str
6.107 -
6.108 +
6.109 fun pgmlterm_to_xml (Atoms {kind, content}) =
6.110 - XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
6.111 + XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
6.112
6.113 | pgmlterm_to_xml (Box {orient, indent, content}) =
6.114 - XML.Elem("box",
6.115 - opt_attr_map pgmlorient_to_string "orient" orient @
6.116 - opt_attr_map int_to_pgstring "indent" indent,
6.117 - map pgmlterm_to_xml content)
6.118 + XML.Elem("box",
6.119 + opt_attr_map pgmlorient_to_string "orient" orient @
6.120 + opt_attr_map int_to_pgstring "indent" indent,
6.121 + map pgmlterm_to_xml content)
6.122
6.123 | pgmlterm_to_xml (Break {mandatory, indent}) =
6.124 - XML.Elem("break",
6.125 - opt_attr_map bool_to_pgstring "mandatory" mandatory @
6.126 - opt_attr_map int_to_pgstring "indent" indent, [])
6.127 + XML.Elem("break",
6.128 + opt_attr_map bool_to_pgstring "mandatory" mandatory @
6.129 + opt_attr_map int_to_pgstring "indent" indent, [])
6.130
6.131 | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
6.132 - XML.Elem("subterm",
6.133 - opt_attr "kind" kind @
6.134 - opt_attr "param" param @
6.135 - opt_attr_map pgmlplace_to_string "place" place @
6.136 - opt_attr "name" name @
6.137 - opt_attr_map pgmldec_to_string "decoration" decoration @
6.138 - opt_attr_map pgmlaction_to_string "action" action @
6.139 - opt_attr "pos" pos @
6.140 - opt_attr_map string_of_pgipurl "xref" xref,
6.141 - map pgmlterm_to_xml content)
6.142 + XML.Elem("subterm",
6.143 + opt_attr "kind" kind @
6.144 + opt_attr "param" param @
6.145 + opt_attr_map pgmlplace_to_string "place" place @
6.146 + opt_attr "name" name @
6.147 + opt_attr_map pgmldec_to_string "decoration" decoration @
6.148 + opt_attr_map pgmlaction_to_string "action" action @
6.149 + opt_attr "pos" pos @
6.150 + opt_attr_map string_of_pgipurl "xref" xref,
6.151 + map pgmlterm_to_xml content)
6.152
6.153 | pgmlterm_to_xml (Alt {kind, content}) =
6.154 - XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
6.155 + XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
6.156
6.157 | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
6.158
6.159 @@ -147,14 +147,14 @@
6.160
6.161
6.162 datatype pgml =
6.163 - Pgml of { version: string option, systemid: string option,
6.164 - area: PgipTypes.displayarea option,
6.165 - content: pgmlterm list }
6.166 + Pgml of { version: string option, systemid: string option,
6.167 + area: PgipTypes.displayarea option,
6.168 + content: pgmlterm list }
6.169
6.170 fun pgml_to_xml (Pgml {version,systemid,area,content}) =
6.171 - XML.Elem("pgml",
6.172 - opt_attr "version" version @
6.173 - opt_attr "systemid" systemid @
6.174 - Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
6.175 - map pgmlterm_to_xml content)
6.176 + XML.Elem("pgml",
6.177 + opt_attr "version" version @
6.178 + opt_attr "systemid" systemid @
6.179 + Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
6.180 + map pgmlterm_to_xml content)
6.181 end
7.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Aug 27 11:49:50 2008 +0200
7.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Aug 27 12:00:28 2008 +0200
7.3 @@ -178,7 +178,7 @@
7.4 let
7.5 val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
7.6 val deps = Symtab.keys (fold Proofterm.thms_of_proof'
7.7 - (map Thm.proof_of ths) Symtab.empty);
7.8 + (map Thm.proof_of ths) Symtab.empty);
7.9 in
7.10 if null names orelse null deps then ()
7.11 else thm_deps_message (spaces_quote names, spaces_quote deps)
8.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Aug 27 11:49:50 2008 +0200
8.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Aug 27 12:00:28 2008 +0200
8.3 @@ -763,7 +763,7 @@
8.4 val location = #location vs (* TODO: extract position *)
8.5
8.6 val _ = start_delay_msgs () (* gather parsing errs/warns *)
8.7 - val doc = PgipParser.pgip_parser Position.none text
8.8 + val doc = PgipParser.pgip_parser Position.none text
8.9 val errs = end_delayed_msgs ()
8.10
8.11 val sysattrs = PgipTypes.opt_attr "systemdata" systemdata