Support PGIP communication for preferences in Emacs mode.
authoraspinall
Tue Dec 05 13:56:43 2006 +0100 (2006-12-05)
changeset 2164940e6fdd26f82
parent 21648 c8a0370c9b93
child 21650 257850c4a3ea
Support PGIP communication for preferences in Emacs mode.
src/Pure/ProofGeneral/TODO
src/Pure/ProofGeneral/pgip_input.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/TODO	Tue Dec 05 01:17:32 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/TODO	Tue Dec 05 13:56:43 2006 +0100
     1.3 @@ -1,16 +1,13 @@
     1.4  Major:
     1.5  
     1.6 - proof_general_emacs.ML fixups/PG compatibility: ongoing
     1.7 -
     1.8   Complete pgip_types: add PGML and objtypes
     1.9  
    1.10   Complete pgip_markup: provide markup abstraction for parsing.ML
    1.11  
    1.12 +Minor:
    1.13  
    1.14 -Minor:
    1.15 + cleanups: signatures & structures, concrete types in XML attrs, etc.
    1.16 +
    1.17 + further tests in pgip_tests.ML
    1.18  
    1.19   <pgipquit> broken
    1.20 -
    1.21 - cleanups: signatures & structures
    1.22 -
    1.23 - further tests in pgip_tests.ML
     2.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Tue Dec 05 01:17:32 2006 +0100
     2.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Tue Dec 05 13:56:43 2006 +0100
     2.3 @@ -9,54 +9,54 @@
     2.4  sig
     2.5      (* These are the PGIP commands to which we respond. *) 
     2.6      datatype pgipinput = 
     2.7 -       (* protocol/prover config *)
     2.8 -	 Askpgip 	of { }
     2.9 -       | Askpgml 	of { } 
    2.10 -       | Askconfig	of { }
    2.11 -       | Askprefs	of { }
    2.12 -       | Setpref 	of { name:string, prefcategory:string option, value:string }
    2.13 -       | Getpref 	of { name:string, prefcategory:string option }
    2.14 -       (* prover control *)
    2.15 -       | Proverinit 	of { }
    2.16 -       | Proverexit 	of { }
    2.17 -       | Startquiet 	of { }
    2.18 -       | Stopquiet	of { } 
    2.19 -       | Pgmlsymbolson  of { } 
    2.20 -       | Pgmlsymbolsoff of { }
    2.21 -       (* improper proof commands: control proof state *)
    2.22 -       | Dostep		of { text: string }
    2.23 -       | Undostep	of { times: int }
    2.24 -       | Redostep	of { }
    2.25 -       | Abortgoal	of { }
    2.26 -       | Forget		of { thyname: string option, name: string option, 
    2.27 -			     objtype: string option }
    2.28 -       | Restoregoal    of { thmname : string }
    2.29 -       (* context inspection commands *)
    2.30 -       | Askids		of { thyname:string option, objtype:string option }
    2.31 -       | Showid		of { thyname:string option, objtype:string, name:string }
    2.32 -       | Askguise	of { }
    2.33 -       | Parsescript	of { text: string, location: PgipTypes.location,
    2.34 -			     systemdata: string option } 
    2.35 -       | Showproofstate of { }
    2.36 -       | Showctxt	of { }
    2.37 -       | Searchtheorems of { arg: string }
    2.38 -       | Setlinewidth   of { width: int }
    2.39 -       | Viewdoc	of { arg: string }
    2.40 -       (* improper theory-level commands *)
    2.41 -       | Doitem		of { text: string }
    2.42 -       | Undoitem	of { }
    2.43 -       | Redoitem	of { }
    2.44 -       | Aborttheory	of { }
    2.45 -       | Retracttheory  of { thyname: string }
    2.46 -       | Loadfile 	of { url: PgipTypes.pgipurl }
    2.47 -       | Openfile 	of { url: PgipTypes.pgipurl }
    2.48 -       | Closefile	of { }
    2.49 -       | Abortfile	of { }
    2.50 -       | Retractfile    of { url: PgipTypes.pgipurl }
    2.51 -       | Changecwd 	of { url: PgipTypes.pgipurl }
    2.52 -       | Systemcmd 	of { arg: string }
    2.53 -       (* unofficial escape command for debugging *)
    2.54 -       | Quitpgip	of { }
    2.55 +    (* protocol/prover config *)
    2.56 +      Askpgip        of { }
    2.57 +    | Askpgml        of { } 
    2.58 +    | Askconfig      of { }
    2.59 +    | Askprefs       of { }
    2.60 +    | Setpref        of { name:string, prefcategory:string option, value:string }
    2.61 +    | Getpref        of { name:string, prefcategory:string option }
    2.62 +    (* prover control *)
    2.63 +    | Proverinit     of { }
    2.64 +    | Proverexit     of { }
    2.65 +    | Startquiet     of { }
    2.66 +    | Stopquiet      of { } 
    2.67 +    | Pgmlsymbolson  of { } 
    2.68 +    | Pgmlsymbolsoff of { }
    2.69 +    (* improper proof commands: control proof state *)
    2.70 +    | Dostep         of { text: string }
    2.71 +    | Undostep       of { times: int }
    2.72 +    | Redostep       of { }
    2.73 +    | Abortgoal      of { }
    2.74 +    | Forget         of { thyname: string option, name: string option, 
    2.75 +                          objtype: string option }
    2.76 +    | Restoregoal    of { thmname : string }
    2.77 +    (* context inspection commands *)
    2.78 +    | Askids         of { thyname:string option, objtype:string option }
    2.79 +    | Showid         of { thyname:string option, objtype:string, name:string }
    2.80 +    | Askguise       of { }
    2.81 +    | Parsescript    of { text: string, location: PgipTypes.location,
    2.82 +                          systemdata: string option } 
    2.83 +    | Showproofstate of { }
    2.84 +    | Showctxt       of { }
    2.85 +    | Searchtheorems of { arg: string }
    2.86 +    | Setlinewidth   of { width: int }
    2.87 +    | Viewdoc        of { arg: string }
    2.88 +    (* improper theory-level commands *)
    2.89 +    | Doitem         of { text: string }
    2.90 +    | Undoitem       of { }
    2.91 +    | Redoitem       of { }
    2.92 +    | Aborttheory    of { }
    2.93 +    | Retracttheory  of { thyname: string }
    2.94 +    | Loadfile       of { url: PgipTypes.pgipurl }
    2.95 +    | Openfile       of { url: PgipTypes.pgipurl }
    2.96 +    | Closefile      of { }
    2.97 +    | Abortfile      of { }
    2.98 +    | Retractfile    of { url: PgipTypes.pgipurl }
    2.99 +    | Changecwd      of { url: PgipTypes.pgipurl }
   2.100 +    | Systemcmd      of { arg: string }
   2.101 +    (* unofficial escape command for debugging *)
   2.102 +    | Quitpgip       of { }
   2.103  
   2.104      val input           : XML.element -> pgipinput option        (* raises PGIP *)
   2.105  end
     3.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Tue Dec 05 01:17:32 2006 +0100
     3.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Tue Dec 05 13:56:43 2006 +0100
     3.3 @@ -9,55 +9,55 @@
     3.4  sig
     3.5      (* These are the PGIP messages which the prover emits. *) 
     3.6      datatype pgipoutput = 
     3.7 -	     Cleardisplay        of { area: PgipTypes.displayarea }
     3.8 -	   | Normalresponse      of { area: PgipTypes.displayarea, 
     3.9 -				      urgent: bool, 
    3.10 -				      messagecategory: PgipTypes.messagecategory, 
    3.11 -				      content: XML.tree list }
    3.12 -	   | Errorresponse       of { fatality: PgipTypes.fatality, 
    3.13 -				      area: PgipTypes.displayarea option, 
    3.14 -				      location: PgipTypes.location option, 
    3.15 -				      content: XML.tree list }
    3.16 -	   | Informfileloaded    of { url: PgipTypes.pgipurl }
    3.17 -	   | Informfileretracted of { url: PgipTypes.pgipurl }
    3.18 -	   | Proofstate	         of { pgml: XML.tree list }
    3.19 -	   | Metainforesponse    of { attrs: XML.attributes, 
    3.20 -				      content: XML.tree list }
    3.21 -	   | Lexicalstructure    of { content: XML.tree list }
    3.22 -	   | Proverinfo	         of { name: string, 
    3.23 -				      version: string, 
    3.24 -				      instance: string,
    3.25 -				      descr: string, 
    3.26 -				      url: Url.T, 
    3.27 -				      filenameextns: string }
    3.28 -	   | Idtable	         of { objtype: string, 
    3.29 -				      context: string option, 
    3.30 -				      ids: string list }
    3.31 -           | Setids		 of { idtables: XML.tree list }
    3.32 -           | Delids		 of { idtables: XML.tree list }
    3.33 -           | Addids		 of { idtables: XML.tree list }
    3.34 -	   | Hasprefs	         of { prefcategory: string option, 
    3.35 -				      prefs: PgipTypes.preference list }
    3.36 -           | Prefval		 of { name: string, value: string }
    3.37 -           | Idvalue		 of { name: string, objtype: string, text: XML.tree list }
    3.38 -	   | Informguise	 of { file : PgipTypes.pgipurl option,  
    3.39 -				      theory: string option, 
    3.40 -				      theorem: string option, 
    3.41 -				      proofpos: int option }
    3.42 -	   | Parseresult	 of { attrs: XML.attributes, content: XML.tree list }
    3.43 -           | Usespgip		 of { version: string, 
    3.44 -				      pgipelems: (string * bool * string list) list }
    3.45 -           | Usespgml		 of { version: string }
    3.46 -	   | Pgip		 of { tag: string option, 
    3.47 -				      class: string, 
    3.48 -				      seq: int, id: string, 
    3.49 -				      destid: string option,
    3.50 -				      refid: string option,
    3.51 -				      refseq: int option,
    3.52 -				      content: XML.tree list }
    3.53 -	   | Ready		 of { }
    3.54 +      Cleardisplay        of { area: PgipTypes.displayarea }
    3.55 +    | Normalresponse      of { area: PgipTypes.displayarea, 
    3.56 +                               urgent: bool, 
    3.57 +                               messagecategory: PgipTypes.messagecategory, 
    3.58 +                               content: XML.tree list }
    3.59 +    | Errorresponse       of { fatality: PgipTypes.fatality, 
    3.60 +                               area: PgipTypes.displayarea option, 
    3.61 +                               location: PgipTypes.location option, 
    3.62 +                               content: XML.tree list }
    3.63 +    | Informfileloaded    of { url: PgipTypes.pgipurl }
    3.64 +    | Informfileretracted of { url: PgipTypes.pgipurl }
    3.65 +    | Proofstate          of { pgml: XML.tree list }
    3.66 +    | Metainforesponse    of { attrs: XML.attributes, 
    3.67 +                               content: XML.tree list }
    3.68 +    | Lexicalstructure    of { content: XML.tree list }
    3.69 +    | Proverinfo          of { name: string, 
    3.70 +                               version: string, 
    3.71 +                               instance: string,
    3.72 +                               descr: string, 
    3.73 +                               url: Url.T, 
    3.74 +                               filenameextns: string }
    3.75 +    | Idtable             of { objtype: string, 
    3.76 +                               context: string option, 
    3.77 +                               ids: string list }
    3.78 +    | Setids              of { idtables: XML.tree list }
    3.79 +    | Delids              of { idtables: XML.tree list }
    3.80 +    | Addids              of { idtables: XML.tree list }
    3.81 +    | Hasprefs            of { prefcategory: string option, 
    3.82 +                               prefs: PgipTypes.preference list }
    3.83 +    | Prefval             of { name: string, value: string }
    3.84 +    | Idvalue             of { name: string, objtype: string, text: XML.tree list }
    3.85 +    | Informguise         of { file : PgipTypes.pgipurl option,  
    3.86 +                               theory: string option, 
    3.87 +                               theorem: string option, 
    3.88 +                               proofpos: int option }
    3.89 +    | Parseresult         of { attrs: XML.attributes, content: XML.tree list }
    3.90 +    | Usespgip            of { version: string, 
    3.91 +                               pgipelems: (string * bool * string list) list }
    3.92 +    | Usespgml            of { version: string }
    3.93 +    | Pgip                of { tag: string option, 
    3.94 +                               class: string, 
    3.95 +                               seq: int, id: string, 
    3.96 +                               destid: string option,
    3.97 +                               refid: string option,
    3.98 +                               refseq: int option,
    3.99 +                               content: XML.tree list }
   3.100 +    | Ready               of { }
   3.101  
   3.102 -    val output : pgipoutput -> XML.tree					 
   3.103 +    val output : pgipoutput -> XML.tree                                  
   3.104  end
   3.105  
   3.106  structure PgipOutput : PGIPOUTPUT =
   3.107 @@ -65,88 +65,84 @@
   3.108  open PgipTypes
   3.109  
   3.110  datatype pgipoutput = 
   3.111 -	 Cleardisplay        of { area: displayarea }
   3.112 +         Cleardisplay        of { area: displayarea }
   3.113         | Normalresponse      of { area: displayarea, urgent: bool, 
   3.114 -				  messagecategory: messagecategory, content: XML.tree list }
   3.115 +                                  messagecategory: messagecategory, content: XML.tree list }
   3.116         | Errorresponse       of { area: displayarea option, fatality: fatality, 
   3.117 -				  location: location option, content: XML.tree list }
   3.118 +                                  location: location option, content: XML.tree list }
   3.119         | Informfileloaded    of { url: Path.T }
   3.120         | Informfileretracted of { url: Path.T }
   3.121 -       | Proofstate	     of { pgml: XML.tree list }
   3.122 +       | Proofstate          of { pgml: XML.tree list }
   3.123         | Metainforesponse    of { attrs: XML.attributes, content: XML.tree list }
   3.124         | Lexicalstructure    of { content: XML.tree list }
   3.125 -       | Proverinfo	     of { name: string, version: string, instance: string,
   3.126 -				  descr: string, url: Url.T, filenameextns: string }
   3.127 -       | Idtable	     of { objtype: string, context: string option, ids: string list }
   3.128 -       | Setids		     of { idtables: XML.tree list }
   3.129 -       | Delids		     of { idtables: XML.tree list }
   3.130 -       | Addids		     of { idtables: XML.tree list }
   3.131 -       | Hasprefs	     of { prefcategory: string option, prefs: preference list }
   3.132 -       | Prefval  	     of { name: string, value: string }
   3.133 -       | Idvalue	     of { name: string, objtype: string, text: XML.tree list }
   3.134 -       | Informguise	     of { file : pgipurl option,  theory: string option, 
   3.135 -				  theorem: string option, proofpos: int option }
   3.136 -       | Parseresult	     of { attrs: XML.attributes, content: XML.tree list }
   3.137 -       | Usespgip	     of { version: string, 
   3.138 -				  pgipelems: (string * bool * string list) list }
   3.139 -       | Usespgml	     of { version: string }
   3.140 -       | Pgip		     of { tag: string option, 
   3.141 -				  class: string, 
   3.142 -				  seq: int, id: string, 
   3.143 -				  destid: string option,
   3.144 -				  refid: string option,
   3.145 -				  refseq: int option,
   3.146 -				  content: XML.tree list}
   3.147 -       | Ready		     of { }
   3.148 +       | Proverinfo          of { name: string, version: string, instance: string,
   3.149 +                                  descr: string, url: Url.T, filenameextns: string }
   3.150 +       | Idtable             of { objtype: string, context: string option, ids: string list }
   3.151 +       | Setids              of { idtables: XML.tree list }
   3.152 +       | Delids              of { idtables: XML.tree list }
   3.153 +       | Addids              of { idtables: XML.tree list }
   3.154 +       | Hasprefs            of { prefcategory: string option, prefs: preference list }
   3.155 +       | Prefval             of { name: string, value: string }
   3.156 +       | Idvalue             of { name: string, objtype: string, text: XML.tree list }
   3.157 +       | Informguise         of { file : pgipurl option,  theory: string option, 
   3.158 +                                  theorem: string option, proofpos: int option }
   3.159 +       | Parseresult         of { attrs: XML.attributes, content: XML.tree list }
   3.160 +       | Usespgip            of { version: string, 
   3.161 +                                  pgipelems: (string * bool * string list) list }
   3.162 +       | Usespgml            of { version: string }
   3.163 +       | Pgip                of { tag: string option, 
   3.164 +                                  class: string, 
   3.165 +                                  seq: int, id: string, 
   3.166 +                                  destid: string option,
   3.167 +                                  refid: string option,
   3.168 +                                  refseq: int option,
   3.169 +                                  content: XML.tree list}
   3.170 +       | Ready               of { }
   3.171  
   3.172  
   3.173 -(* util *)
   3.174 -
   3.175 -fun attrsome attr f x = case x of NONE => [] | SOME x => [(attr,f x)]
   3.176 -
   3.177  (* Construct output XML messages *)
   3.178 -	
   3.179 +        
   3.180  fun cleardisplay vs = 
   3.181      let
   3.182 -	val area = #area vs
   3.183 +        val area = #area vs
   3.184      in
   3.185 -	XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
   3.186 +        XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
   3.187      end
   3.188  
   3.189  fun normalresponse vs =
   3.190      let 
   3.191 -	val area = #area vs
   3.192 -	val urgent = #urgent vs
   3.193 -	val messagecategory = #messagecategory vs
   3.194 -	val content = #content vs
   3.195 +        val area = #area vs
   3.196 +        val urgent = #urgent vs
   3.197 +        val messagecategory = #messagecategory vs
   3.198 +        val content = #content vs
   3.199      in
   3.200 -	XML.Elem ("normalresponse", 
   3.201 -		 (attrs_of_displayarea area) @
   3.202 -		 (if urgent then [("urgent", "true")] else []) @
   3.203 -		 (attrs_of_messagecategory messagecategory),
   3.204 -		 content)
   3.205 +        XML.Elem ("normalresponse", 
   3.206 +                 (attrs_of_displayarea area) @
   3.207 +                 (if urgent then [("urgent", "true")] else []) @
   3.208 +                 (attrs_of_messagecategory messagecategory),
   3.209 +                 content)
   3.210      end
   3.211 -				       
   3.212 +                                       
   3.213  fun errorresponse vs =
   3.214      let 
   3.215 -	val area = #area vs
   3.216 -	val fatality = #fatality vs
   3.217 -	val location = #location vs
   3.218 -	val content = #content vs
   3.219 +        val area = #area vs
   3.220 +        val fatality = #fatality vs
   3.221 +        val location = #location vs
   3.222 +        val content = #content vs
   3.223      in
   3.224 -	XML.Elem ("errorresponse",
   3.225 -		 (the_default [] (Option.map attrs_of_displayarea area)) @
   3.226 -		 (attrs_of_fatality fatality) @
   3.227 -		 (the_default [] (Option.map attrs_of_location location)),
   3.228 -		 content)
   3.229 +        XML.Elem ("errorresponse",
   3.230 +                 (the_default [] (Option.map attrs_of_displayarea area)) @
   3.231 +                 (attrs_of_fatality fatality) @
   3.232 +                 (the_default [] (Option.map attrs_of_location location)),
   3.233 +                 content)
   3.234      end
   3.235 -				       
   3.236 +                                       
   3.237  
   3.238  fun informfile lr vs =
   3.239      let 
   3.240 -	val url = #url vs
   3.241 +        val url = #url vs
   3.242      in
   3.243 -	XML.Elem ("informfile" ^ lr, attrs_of_pgipurl url, [])
   3.244 +        XML.Elem ("informfile" ^ lr, attrs_of_pgipurl url, [])
   3.245      end
   3.246  
   3.247  val informfileloaded = informfile "loaded"
   3.248 @@ -154,120 +150,118 @@
   3.249  
   3.250  fun proofstate vs =
   3.251      let
   3.252 -	val pgml = #pgml vs
   3.253 +        val pgml = #pgml vs
   3.254      in
   3.255 -	XML.Elem("proofstate", [], pgml)
   3.256 +        XML.Elem("proofstate", [], pgml)
   3.257      end
   3.258  
   3.259  fun metainforesponse vs =
   3.260      let 
   3.261 -	val attrs = #attrs vs
   3.262 -	val content = #content vs
   3.263 +        val attrs = #attrs vs
   3.264 +        val content = #content vs
   3.265      in
   3.266 -	XML.Elem ("metainforesponse", attrs, content)
   3.267 +        XML.Elem ("metainforesponse", attrs, content)
   3.268      end
   3.269  
   3.270  fun lexicalstructure vs =
   3.271      let
   3.272 -	val content = #content vs
   3.273 +        val content = #content vs
   3.274      in
   3.275 -	XML.Elem ("lexicalstructure", [], content)
   3.276 +        XML.Elem ("lexicalstructure", [], content)
   3.277      end
   3.278  
   3.279  fun proverinfo vs =
   3.280      let
   3.281 -	val name = #name vs
   3.282 -	val version = #version vs
   3.283 -	val instance = #instance vs
   3.284 -	val descr = #descr vs
   3.285 -	val url = #url vs
   3.286 -	val filenameextns = #filenameextns vs
   3.287 +        val name = #name vs
   3.288 +        val version = #version vs
   3.289 +        val instance = #instance vs
   3.290 +        val descr = #descr vs
   3.291 +        val url = #url vs
   3.292 +        val filenameextns = #filenameextns vs
   3.293      in 
   3.294 -	XML.Elem ("proverinfo",
   3.295 -		 [("name", name),
   3.296 -		  ("version", version),
   3.297 -		  ("instance", instance), 
   3.298 -		  ("descr", descr),
   3.299 -		  ("url", Url.pack url),
   3.300 -		  ("filenameextns", filenameextns)],
   3.301 -		 [])
   3.302 +        XML.Elem ("proverinfo",
   3.303 +                 [("name", name),
   3.304 +                  ("version", version),
   3.305 +                  ("instance", instance), 
   3.306 +                  ("descr", descr),
   3.307 +                  ("url", Url.pack url),
   3.308 +                  ("filenameextns", filenameextns)],
   3.309 +                 [])
   3.310      end
   3.311  
   3.312  fun idtable vs = 
   3.313      let 
   3.314 -	val objtype = #objtype vs
   3.315 -	val objtype_attrs = [("objtype", objtype)]
   3.316 -	val context = #context vs
   3.317 -	val context_attrs = opt_attr "context" context
   3.318 -	val ids = #ids vs
   3.319 -	val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
   3.320 +        val objtype = #objtype vs
   3.321 +        val objtype_attrs = attr [("objtype", objtype)]
   3.322 +        val context = #context vs
   3.323 +        val context_attrs = opt_attr "context" context
   3.324 +        val ids = #ids vs
   3.325 +        val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
   3.326      in 
   3.327 -	XML.Elem ("idtable",
   3.328 -		  objtype_attrs @ context_attrs,
   3.329 -		  ids_content)
   3.330 +        XML.Elem ("idtable",
   3.331 +                  objtype_attrs @ context_attrs,
   3.332 +                  ids_content)
   3.333      end
   3.334  
   3.335  fun setids vs =
   3.336      let
   3.337 -	val idtables = #idtables vs
   3.338 +        val idtables = #idtables vs
   3.339      in
   3.340 -	XML.Elem ("setids",[],idtables)
   3.341 +        XML.Elem ("setids",[],idtables)
   3.342      end
   3.343  
   3.344  fun addids vs =
   3.345      let
   3.346 -	val idtables = #idtables vs
   3.347 +        val idtables = #idtables vs
   3.348      in
   3.349 -	XML.Elem ("addids",[],idtables)
   3.350 +        XML.Elem ("addids",[],idtables)
   3.351      end
   3.352  
   3.353  fun delids vs =
   3.354      let
   3.355 -	val idtables = #idtables vs
   3.356 +        val idtables = #idtables vs
   3.357      in
   3.358 -	XML.Elem ("delids",[],idtables)
   3.359 +        XML.Elem ("delids",[],idtables)
   3.360      end
   3.361  
   3.362  
   3.363  fun acceptedpgipelems vs = 
   3.364      let
   3.365 -	val pgipelems = #pgipelems vs
   3.366 -	fun async_attrs b = if b then [("async","true")] else []
   3.367 -	fun attrs_attrs attrs = if attrs=[] then [] else [("attributes",space_implode "," attrs)]
   3.368 -	fun singlepgipelem (e,async,attrs) = 
   3.369 -	    XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[])
   3.370 -						      
   3.371 +        val pgipelems = #pgipelems vs
   3.372 +        fun async_attrs b = if b then [("async","true")] else []
   3.373 +        fun attrs_attrs attrs = if attrs=[] then [] else [("attributes",space_implode "," attrs)]
   3.374 +        fun singlepgipelem (e,async,attrs) = 
   3.375 +            XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[])
   3.376 +                                                      
   3.377      in
   3.378 -	XML.Elem ("acceptedpgipelems", [],
   3.379 -		 map singlepgipelem pgipelems)
   3.380 +        XML.Elem ("acceptedpgipelems", [],
   3.381 +                 map singlepgipelem pgipelems)
   3.382      end
   3.383  
   3.384  
   3.385 -fun attro x yo = case yo of NONE => [] | SOME y => [(x,y)] : XML.attributes
   3.386 -
   3.387  fun hasprefs vs =
   3.388    let 
   3.389        val prefcategory = #prefcategory vs
   3.390        val prefs = #prefs vs
   3.391    in 
   3.392 -      XML.Elem("hasprefs",attro "prefcategory" prefcategory, map haspref prefs)
   3.393 +      XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs)
   3.394    end
   3.395  
   3.396  fun prefval vs =
   3.397      let 
   3.398 -	val name = #name vs
   3.399 -	val value = #value vs
   3.400 +        val name = #name vs
   3.401 +        val value = #value vs
   3.402      in
   3.403 -	XML.Elem("prefval", [("name",name)], [XML.Text value])
   3.404 +        XML.Elem("prefval", [("name",name)], [XML.Text value])
   3.405      end 
   3.406  
   3.407  fun idvalue vs =
   3.408      let 
   3.409 -	val name = #name vs
   3.410 -	val objtype = #objtype vs
   3.411 -	val text = #text vs
   3.412 +        val name = #name vs
   3.413 +        val objtype = #objtype vs
   3.414 +        val text = #text vs
   3.415      in
   3.416 -	XML.Elem("idvalue", [("name",name),("objtype",objtype)], text)
   3.417 +        XML.Elem("idvalue", [("name",name),("objtype",objtype)], text)
   3.418      end 
   3.419  
   3.420  
   3.421 @@ -283,84 +277,83 @@
   3.422        val guisefile = elto "guisefile" attrs_of_pgipurl file
   3.423        val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
   3.424        val guiseproof = elto "guiseproof" 
   3.425 -			    (fn thm=>[("thmname",thm)]@
   3.426 -				     (attro "proofpos" (Option.map Int.toString proofpos))) theorem
   3.427 +                            (fn thm=>[("thmname",thm)]@
   3.428 +                                     (opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem
   3.429    in 
   3.430        XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
   3.431    end
   3.432  
   3.433  fun parseresult vs =
   3.434      let
   3.435 -	val attrs = #attrs vs
   3.436 -	val content = #content vs
   3.437 +        val attrs = #attrs vs
   3.438 +        val content = #content vs
   3.439      in 
   3.440 -	XML.Elem("parseresult", attrs, content)
   3.441 +        XML.Elem("parseresult", attrs, content)
   3.442      end
   3.443  
   3.444  fun usespgip vs =
   3.445      let
   3.446 -	val version = #version vs
   3.447 -	val acceptedelems = acceptedpgipelems vs
   3.448 +        val version = #version vs
   3.449 +        val acceptedelems = acceptedpgipelems vs
   3.450      in 
   3.451 -	XML.Elem("usespgip", [("version", version)], [acceptedelems])
   3.452 +        XML.Elem("usespgip", [("version", version)], [acceptedelems])
   3.453      end
   3.454  
   3.455  fun usespgml vs =
   3.456      let
   3.457 -	val version = #version vs
   3.458 +        val version = #version vs
   3.459      in 
   3.460 -	XML.Elem("usespgml", [("version", version)], [])
   3.461 +        XML.Elem("usespgml", [("version", version)], [])
   3.462      end
   3.463  
   3.464  fun pgip vs =
   3.465      let 
   3.466 -	val tag = #tag vs
   3.467 -	val class = #class vs
   3.468 -	val seq = #seq vs
   3.469 -	val id = #id vs
   3.470 -	val destid = #destid vs
   3.471 -	val refid = #refid vs
   3.472 -	val refseq = #refseq vs
   3.473 -	val content = #content vs
   3.474 +        val tag = #tag vs
   3.475 +        val class = #class vs
   3.476 +        val seq = #seq vs
   3.477 +        val id = #id vs
   3.478 +        val destid = #destid vs
   3.479 +        val refid = #refid vs
   3.480 +        val refseq = #refseq vs
   3.481 +        val content = #content vs
   3.482      in
   3.483 -	XML.Elem("pgip",
   3.484 -		 opt_attr "tag" tag @
   3.485 -		 [("id", id)] @
   3.486 -		 opt_attr "destid" destid @
   3.487 -		 [("class", class)] @
   3.488 -		 opt_attr "refid" refid @
   3.489 -		 opt_attr_map string_of_int "refseq" refseq @
   3.490 -		 [("seq", string_of_int seq)],
   3.491 -		 content)
   3.492 +        XML.Elem("pgip",
   3.493 +                 opt_attr "tag" tag @
   3.494 +                 [("id", id)] @
   3.495 +                 opt_attr "destid" destid @
   3.496 +                 [("class", class)] @
   3.497 +                 opt_attr "refid" refid @
   3.498 +                 opt_attr_map string_of_int "refseq" refseq @
   3.499 +                 [("seq", string_of_int seq)],
   3.500 +                 content)
   3.501      end
   3.502  
   3.503 -fun ready vs = 
   3.504 -    XML.Elem("ready",[],[])
   3.505 +fun ready vs = XML.Elem("ready",[],[])
   3.506  
   3.507  
   3.508  fun output pgipoutput = case pgipoutput of
   3.509 -   Cleardisplay vs 	   => cleardisplay vs
   3.510 +   Cleardisplay vs         => cleardisplay vs
   3.511   | Normalresponse vs       => normalresponse vs
   3.512   | Errorresponse vs        => errorresponse vs
   3.513 - | Informfileloaded vs	   => informfileloaded vs
   3.514 + | Informfileloaded vs     => informfileloaded vs
   3.515   | Informfileretracted vs  => informfileretracted vs
   3.516 - | Proofstate vs	   => proofstate vs
   3.517 - | Metainforesponse vs	   => metainforesponse vs
   3.518 - | Lexicalstructure vs	   => lexicalstructure vs
   3.519 - | Proverinfo vs	   => proverinfo vs
   3.520 - | Idtable vs		   => idtable vs
   3.521 - | Setids vs		   => setids vs
   3.522 - | Addids vs		   => addids vs
   3.523 - | Delids vs		   => delids vs
   3.524 - | Hasprefs vs		   => hasprefs vs
   3.525 - | Prefval vs		   => prefval vs
   3.526 - | Idvalue vs		   => idvalue vs
   3.527 - | Informguise vs	   => informguise vs
   3.528 - | Parseresult vs	   => parseresult vs
   3.529 - | Usespgip vs		   => usespgip vs
   3.530 - | Usespgml vs		   => usespgml vs
   3.531 - | Pgip vs		   => pgip vs
   3.532 - | Ready vs		   => ready vs
   3.533 + | Proofstate vs           => proofstate vs
   3.534 + | Metainforesponse vs     => metainforesponse vs
   3.535 + | Lexicalstructure vs     => lexicalstructure vs
   3.536 + | Proverinfo vs           => proverinfo vs
   3.537 + | Idtable vs              => idtable vs
   3.538 + | Setids vs               => setids vs
   3.539 + | Addids vs               => addids vs
   3.540 + | Delids vs               => delids vs
   3.541 + | Hasprefs vs             => hasprefs vs
   3.542 + | Prefval vs              => prefval vs
   3.543 + | Idvalue vs              => idvalue vs
   3.544 + | Informguise vs          => informguise vs
   3.545 + | Parseresult vs          => parseresult vs
   3.546 + | Usespgip vs             => usespgip vs
   3.547 + | Usespgml vs             => usespgml vs
   3.548 + | Pgip vs                 => pgip vs
   3.549 + | Ready vs                => ready vs
   3.550  
   3.551  end
   3.552  
     4.1 --- a/src/Pure/ProofGeneral/preferences.ML	Tue Dec 05 01:17:32 2006 +0100
     4.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Tue Dec 05 13:56:43 2006 +0100
     4.3 @@ -77,7 +77,8 @@
     4.4  	fun setn n = (print_depth n; pg_print_depth_val := n)
     4.5  	val set = setn o PgipTypes.read_pgipnat
     4.6      in
     4.7 -	mkpref get set PgipTypes.Pgipbool "print-depth" "Setting for the ML print depth"
     4.8 +	mkpref get set PgipTypes.Pgipnat
     4.9 +	       "print-depth" "Setting for the ML print depth"
    4.10      end
    4.11  
    4.12  
     5.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Dec 05 01:17:32 2006 +0100
     5.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Dec 05 13:56:43 2006 +0100
     5.3 @@ -240,7 +240,7 @@
     5.4  (* FIXME: check this uses non-transitive closure function here *)
     5.5  fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
     5.6    let
     5.7 -    val names = filter_out (equal "") (map Thm.name_of_thm ths);
     5.8 +    val names = filter_out (equal "") (map PureThy.get_name_hint ths);
     5.9      val deps = filter_out (equal "")
    5.10        (Symtab.keys (fold Proofterm.thms_of_proof
    5.11          (map Thm.proof_of ths) Symtab.empty));
    5.12 @@ -321,6 +321,7 @@
    5.13     (setmp warning_fn (K ()) init_outer_syntax ();
    5.14      setup_xsymbols_output ();
    5.15      setup_messages ();
    5.16 +    ProofGeneralPgip.init_pgip_channel (!priority_fn);
    5.17      setup_state ();
    5.18      setup_thy_loader ();
    5.19      setup_present_hook ();
     6.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Dec 05 01:17:32 2006 +0100
     6.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Dec 05 13:56:43 2006 +0100
     6.3 @@ -11,8 +11,9 @@
     6.4  sig
     6.5    val init_pgip: bool -> unit		  (* main PGIP loop with true; fail with false *)
     6.6  
     6.7 -  val process_pgip: string -> unit        (* process a command; only good for preferences *)
     6.8 -  val init_pgip_session_id: unit -> unit  (* call before using process_pgip *)
     6.9 +  (* These two are just to support the semi-PGIP Emacs mode *)
    6.10 +  val init_pgip_channel: (string -> unit) -> unit 
    6.11 +  val process_pgip: string -> unit     
    6.12  end
    6.13  
    6.14  structure ProofGeneralPgip : PROOF_GENERAL_PGIP  =
    6.15 @@ -146,10 +147,11 @@
    6.16  
    6.17  fun matching_pgip_id id = (id = !pgip_id)
    6.18  
    6.19 -val output_xml = writeln_default o XML.string_of_tree;  (* FIXME: use string buffer *)
    6.20 +val output_xml_fn = ref writeln_default  
    6.21 +fun output_xml s = (!output_xml_fn) (XML.string_of_tree s);  (* TODO: string buffer *)
    6.22  
    6.23  fun issue_pgip_rawtext str = 
    6.24 -    output_xml (PgipOutput.output (assemble_pgips [XML.Text str])) (* FIXME: don't escape!! *)
    6.25 +    output_xml (PgipOutput.output (assemble_pgips [XML.Rawtext str]))
    6.26  
    6.27  fun issue_pgips pgipops =
    6.28      output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops)));
    6.29 @@ -865,7 +867,9 @@
    6.30  			       (XML.string_of_tree xml));
    6.31  	     true))
    6.32  
    6.33 -val process_pgip = K () o process_pgip_tree o XML.tree_of_string
    6.34 +(* External input *)
    6.35 +
    6.36 +val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
    6.37  
    6.38  end
    6.39  
    6.40 @@ -963,7 +967,7 @@
    6.41  val process_pgipP =
    6.42    OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
    6.43      (P.text >> (Toplevel.no_timing oo
    6.44 -      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
    6.45 +      (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
    6.46  
    6.47  fun init_outer_syntax () = OuterSyntax.add_parsers
    6.48   [undoP, redoP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
    6.49 @@ -999,7 +1003,26 @@
    6.50  fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
    6.51    | init_pgip true = (init_setup (); pgip_toplevel tty_src);
    6.52  
    6.53 -fun write_keywords s = ()  (* NB: do nothing *)
    6.54 +
    6.55 +
    6.56 +(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
    6.57 +
    6.58 +local
    6.59 +    val pgip_output_channel = ref writeln_default
    6.60 +in
    6.61 +
    6.62 +(* Set recipient for PGIP results *)
    6.63 +fun init_pgip_channel writefn =
    6.64 +    (init_pgip_session_id();  
    6.65 +     pgip_output_channel := writefn)				  
    6.66 +
    6.67 +(* Process a PGIP command. 
    6.68 +   This works for preferences but not generally guaranteed 
    6.69 +   because we haven't done full setup here (e.g., no pgml mode)  *)
    6.70 +fun process_pgip str =
    6.71 +     setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
    6.72 +
    6.73 +end
    6.74  
    6.75  end;
    6.76