Utilities for Proof General Eclipse


TPWrapper is a simple java utility for networking a command-line theorem prover (not: does not work for MS Windows). It turns a command-line interface into a socket-based interface. I wrote it in order to access Isabelle from my Windows laptop.

The program comprises two classes (TPWrapper and TP!WrapperServerThread). To run it:

  1. Find TPWrapper.class in your Proof General installation under ed.inf.proofgeneral/bin
  2. Use java TPWrapper [port-number] [command] to run (note: you probably want to run this as a background process). This will cause TPWrapper to listen at [port-number]. It responds to connection attempts by executing [command] in a child process, and linking the port input and output streams to the process's input and output streams.


  • Can anyone help us resolve the problem that Isabelle complains about Windows-style directory qualifiers here?

  <- <pgip class="pa" id="PG-Eclipse" seq="2"><changecwd dir="C:\Dokumente und Einstellungen\cxl\Eigene Dateien\pgeclipse-test\eclipse"/></pgip>
TP -> Exception-
TP ->    ERROR
TP ->       "Illegal character(s) \"\\\", \":\" in path element specification: \ "C:\\Dokumente und Einstellungen\\cxl\\Eigene Dateien\\pgeclipse-test\\eclipse\" "
TP ->    raised

This topic: PG > WebHome > ProofGeneralKit > ProofGeneralEclipse > PGEclipseInstall > PGEclipseUtils
Topic revision: r2 - 09 Oct 2006 - 17:33:02 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies