/[mojave]/metaprl/doc/misc/UIDesign.html
ViewVC logotype

Diff of /metaprl/doc/misc/UIDesign.html

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3577 by nogin, Tue Apr 16 19:59:11 2002 UTC revision 3578 by nogin, Tue Apr 16 19:59:37 2002 UTC
# Line 12  Line 12 
12  </ul>  </ul>
13  <h2>Design requirements</h2>  <h2>Design requirements</h2>
14  We want the UI to be able to display the following kinds of items:  We want the UI to be able to display the following kinds of items:
15  <ul><li>Theory listing  <ul><li>Listing of a bunch of things
16  <li>Proof node  <li>Proof node
17  <li>Graph of a proof structure  <li>Graph of a proof structure
18  <li>Menu (global, local, submenu, etc)</li><br>  <li>Menu (global, local, submenu, etc)
19  <b>Question:</b> How about listing <i>of</i> theories, do we want a special  <li>Dialogs</li><br>
 item type for that?<br>  
20  <b>Question:</b> We have discussed that want to allow editing of certain items in a theory (e.g  <b>Question:</b> We have discussed that want to allow editing of certain items in a theory (e.g
21  comments, code objects, possibly - theorem statements). Do we want to allow  comments, code objects, possibly - theorem statements). Do we want to allow
22  editing them in a theory listing, or do we want to have a special item  editing them in a theory listing, or do we want to have a special item
# Line 31  Line 30 
30  <ul><li>Each kind of items should be displayed in a way appropriate for that  <ul><li>Each kind of items should be displayed in a way appropriate for that
31  kind of items. This probably means that each particular window should only  kind of items. This probably means that each particular window should only
32  be used to display items of one kind.  be used to display items of one kind.
33    <li>We do not want to decide on any particular layout of windows until we know
34    more about what kinds of windows we'll have and how they are going to look
35    like.
36  <li>Whenever we are displaying terms, we should do it in a way that is  <li>Whenever we are displaying terms, we should do it in a way that is
37  consistent with their internal structure.  consistent with their internal structure.
38  <li>Term display should allow <i>structured</i> selection (e.g. copy&amp;paste  <li>Term display should allow <i>structured</i> selection (e.g. copy&amp;paste
# Line 42  Line 44 
44  proof menu to be associated with it (supplied by the prover when requested by  proof menu to be associated with it (supplied by the prover when requested by
45  UI, not a part of the proof node item).  UI, not a part of the proof node item).
46  <li>The method (tactic) used to generate a node should be displayed as a part  <li>The method (tactic) used to generate a node should be displayed as a part
47  of the node and should be editable. The subgoals of a node (at least in the  of the node and should be editable. The subgoals of a node (in the case of a
48  case of a sequent calculus) should be displayed there as well.<br>  sequent calculus) or new hypotheses and goals generated by a node (in the case
49  <b>Question:</b> What should be displayed in the proof node display in case of  of a natural deduction calculus) should be displayed there as well.<br>
50  a natural deduction calculus?  In fact, we would probably want some sort of 3-pane display for the proof node
51    - original proof state (e.g. the goal), method used to modify the proof state
52    (e.g. tactic) and the modified proof state or modified parts of it (e.g.
53    subgoals)</li>
54  <li>In addition to default ("pretty printed") representation, the prover may  <li>In addition to default ("pretty printed") representation, the prover may
55  be capable of providing alternative representations of some items - for  be capable of providing alternative representations of some items - for
56  example, verbalized representation, source ("input") representation of terms,  example, verbalized representation, source ("input") representation of terms,
57  etc. The UI should not assume the prover supports some particular  etc. The UI should not assume the prover supports some particular
58  representation (except for the default one), but should be capable of  representation (except for the default one), but should be capable of
59  requesting and displaying those that the prover does support.  requesting and displaying those that the prover does support.
60    <li>We may have a generic (e.g. HTML forms-like) support for dialogs, but it
61    seems that support for a few common cases might be sufficient.
62  <li> All communication should be initiated by the UI (to avoid firewall  <li> All communication should be initiated by the UI (to avoid firewall
63  problems, etc), preferably in the form of HTTP GET and POST requests  problems, etc), preferably in the form of HTTP GET and POST requests
64  (including <a href="http://www.xmlrpc.org/">XML-RPC</a> queries).  (including <a href="http://www.xmlrpc.org/">XML-RPC</a> queries).
# Line 125  Line 132 
132  <ul><li>Do we have a name for the UI?  <ul><li>Do we have a name for the UI?
133  <li>Is it time to create a CVS repository for the project (and put this  <li>Is it time to create a CVS repository for the project (and put this
134  document there, for example)?  document there, for example)?
135  <li>Where should we create the repository - Omega CVS server or MetaPRL CVS  <li>Where should we create the repository - MathWeb CVS server
136  server?<br>  (<tt>cvs.methweb.org</tt>) or MetaPRL CVS server (<tt>cvs.metaprl.org</tt>)?<br>
137  The advantages of the MetaPRL server:  The advantages of the MetaPRL server:
138  <ul>  <ul>
139  <li>Better "anti-firewall" setup - CVS is available on ports 80 and 3000, this  <li>Better "anti-firewall" setup - CVS is available on ports 80 and 3000, this
# Line 146  Line 153 
153  <li>A separate administrative control - the project would have a separate  <li>A separate administrative control - the project would have a separate
154  set of accounts, that are not shared with anything else.  set of accounts, that are not shared with anything else.
155  </ul>  </ul>
156  The advantaged of the Omega server:  The advantaged of the MathWeb server:
157  <ul><li>More convenient for Omega group.  <ul><li>More convenient for MathWeb group (and probably the rest of the AGS
158  <li>???  group as well).
159    <li><b>???</b>
160  </ul>  </ul>
161  </ul>  </ul>
162    

Legend:
Removed from v.3577  
changed lines
  Added in v.3578

  ViewVC Help
Powered by ViewVC 1.1.26