A REST view on the Broker

Although a proof-in-progress is dynamic, we can structure URLs using a static format, e.g.

http://localhost:7007/Example.thy/proofsteps/line/43

which might display the output from the theorem prover after line 43 of Example.thy has been processed, with a link back to Example.thy. (That could then be coloured by the usual conventions, assuming a linear-ordered progression through the script).

We assume here that Example.thy is read-only, so the results of processing it can be cached as the URL is requested. If Example.thy is changed, we ought to include version numbers inside the URL.

We may enable other views of the same resource, e.g.:

http://localhost:7007/Example.thy/proofsteps/theorem/conj_comms

which is the same as the line view that corresponds to the end of the proof of the theorem conj_comms

For more info on REST, see e.g.

Topic revision: r1 - 05 Sep 2006 - 17:32:11 - 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