PG Kit Filespace Handling

The current handling of files is that we quietly assume that the broker and the display live in the same filespace, as otherwise the user has to guess which file to open.

This is particularly unhelpful in the Eclipse framework, which maps buffers to so-called resources. (I forgot the details!)

A more systematic way to handle this would be to only allow the broker to access the filespace, and have a protocol for browsing the (broker-side) filespace.

-- ChristophLueth - 26 Sep 2006

Where are the local files?

NB: according to pgip.rnc we use URIs for resource specification whose syntax follows RFC 3986. There is a question over the interpretation of URIs beginning file:///. First proposal: we interpret these as meaning broker-side filespace, which is not necessarily accessible directly to displays or provers.

Displays should be able to intuit whether they have the same locality as the Broker based on how they connect to the Broker. Then the Broker is obliged to make the mapping for provers: unfortunately this is particularly challenging if the prover is going to load dependent files automatically when running on another machine where the Broker may not have file access (read or write)! We ought to mandate what the prover will do in this situation. It might be possible (but ugly) to require the prover to make file access via the Broker, for example.

In the case of Eclipse, Eclipse 3.2 has (in)conveniently introduced the possibility that resources are no longer necessarily in the local file system. See the 3.2 Plugin migration FAQ at The API is described in the documentation of the package org.eclipse.core.filesystem.

This means that we may be able to implement the Broker as a backing-storage mechanism by implementing this API! The requirements of the API may also give us a guide to which file services we need PGIP to implement. I guess future/present Eclipse plugins may also provide implementations which allow editing files over FTP, etc (after all, Eclipse is working towards being Emacs, who can do this).

But: encoding a file system protocol into PGIP seems a bit heavy and overkill and we should avoid it as far as possible!! Possible alternative ideas:

  • Use shared interpretation of URIs between display and Broker.
    If the display cannot access the file system of the Broker, tough, it will not be able to browse it.
  • Use standard http for browsing via the Broker (recalling the idea for a REST-like view on the broker)
    Needs work.
  • Others?

-- DavidAspinall - 29 Sep 2006

Topic revision: r3 - 29 Sep 2006 - 15:46:07 - 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