diff options
Diffstat (limited to 'html/features.phtml')
| -rw-r--r-- | html/features.phtml | 117 |
1 files changed, 72 insertions, 45 deletions
diff --git a/html/features.phtml b/html/features.phtml index 4dc01cef..0b3fee7d 100644 --- a/html/features.phtml +++ b/html/features.phtml @@ -5,12 +5,27 @@ It doesn't matter if you're an Emacs militant or a pacifist! </p> <p> -Proof General will be useful to you if you use a proof -assistant, and you'd like some of the following features: +Proof General is designed to be useful for novices and expert users alike. +<br> +It will be useful to you if you use a proof assistant, and +you'd like an interface with the following features: +<a href="#script">script management</a>, +<a href="#multiple">multiple file scripting</a>, +<a href="#pbp">proof by pointing</a>, +<a href="#toolbar">toolbar and menus</a>, +<a href="#fontlock">syntax highlighting</a>, +<a href="#xsymbol">real symbols</a>, +<a href="#funcmenu">definitions menu</a>, +<a href="#tags">tags</a>, +and finally, +<a href="#generic">adaptability</a>. +<br> +Are you convinced yet? +If not, read on… </p> - +</hrule> <dl> - <?php dt("Script management.") ?> + <a name="script"><?php dt("Script management.") ?></a> <dd> A <em>proof script</em> is a sequence of commands sent to a proof assistant to construct a proof, usually stored in @@ -32,39 +47,33 @@ assistant, and you'd like some of the following features: of Proof General to see script managament in action. </p> </dd> - <?php dt("Multiple files.") ?> + <a name="multiple"><?php dt("Multiple files.") ?></a> <dd> Script management in Proof General can work across many script - files. When a script is visited in the editor, it is - coloured to reflect whether the proof assistant has loaded it in - this session. + files. When a script is visited in the editor, it is locked + (coloured) to reflect whether the proof assistant has loaded it in + this session. When a file is unlocked, all of the files which + depend on it are automatically unlocked too. <p> - Dependencies between script files are - communicated from the proof assistant to Proof General. - If you want to edit a file which has been loaded into the - proof assistant already, Proof General will unlock the file - and all the files which depend on it. This connects the - editor with the theory dependency or make system of the - proof assistant. + Dependencies between script files are either communicated from the + proof assistant to Proof General, or maintained automatically by + Proof General (based on the order in which files were processed). </p> - <?php footnote("Multiple files currently supported in LEGO and Isabelle only")?> </dd> - <?php dt("Proof by Pointing.") ?> + <a name="pbp"><?php dt("Proof by Pointing.") ?></a> <dd> <em>Proof by pointing</em> allows you to click on a subterm of a goal to be proved, and apply an appropriate rule or tactic automatically. <p> - Proof by pointing uses the - interface to highlight subterms under the mouse, and Proof General - uses the subterm structure to make it easy - to cut and paste complicated subterms. + Proof by pointing uses the interface to highlight subterms under the + mouse, and sends messages asking the prover for hints to proceed. + Proof General also uses the subterm structure to make it easy to cut + and paste from complicated terms. </p> - <?php footnote("No assistant fully supports proof-by-pointing in Proof General - yet. LEGO provides subterm markup for exploring term - structure.") ?> + <?php footnote("Proof by pointing for Proof General is only supported by LEGO (experimentally) at the moment. We need help from each proof assistant implementors to add it elsewhere.") ?> </dd> - <?php dt("Toolbar.") ?> + <a name="toolbar"><?php dt("Toolbar and menus") ?></a> <dd> Proof General has a toolbar with buttons for examining the proof state, starting a proof, manoeuvring in the proof script, @@ -73,10 +82,14 @@ assistant, and you'd like some of the following features: <p> Using the toolbar, you can replay proofs without knowing any low-level commands of the proof assistant or any Emacs hot-keys! + <p> + Additionally, the toolbar commands and many more besides are + available on menus; you don't need to know magical key presses for + any features. </p> <?php footnote("Toolbar is available in XEmacs only") ?> </dd> - <?php dt("Syntax highlighting.") ?> + <a name="fontlock"><?php dt("Syntax highlighting.") ?></a> <dd> Syntax highlighting is an editing feature which decorates a file with different colours or fonts according to the syntax of some @@ -87,19 +100,21 @@ assistant, and you'd like some of the following features: assumptions, for example. </p> </dd> - <?php dt("Tags.") ?> + <a name="xsymbol"><?php dt("Real symbols.") ?></a> <dd> - Tags are an editing feature which allow you to quickly locate - the definition or declaration of a particular identifier. + Proof General has a close integration with the + powerful + <a href="http://www.fmi.uni-passau.de/~wedler/x-symbol">X-Symbol</a> + package, which makes it easy to transparently use real symbols and + Greek letters in your proofs. + <br> Instead of seeing "not P", you see "¬ </dd>P", instead + of "a * b", you see "a × b", etc. <br> + [the examples above are simple so they will work on most browsers + without needing images] <p> - Proof General is supplied with utilities to make tag indexes - for Emacs. This makes it easy to quickly access definitions from a - standard library, for example, and in large proof developments - split across multiple files. - <?php footnote("Tags programs are provided for LEGO and Coq") ?> - <p></p> + <?php footnote("X-Symbol currently works in XEmacs only") ?> </dd> - <?php dt("Definitions Menu.") ?> + <a name="funcmenu"><?php dt("Definitions Menu.") ?></a> <dd> A pull-down menu gives easy access to definitions, declarations and proofs in the current @@ -113,18 +128,31 @@ assistant, and you'd like some of the following features: remotely, while your files and editor reside on your local machine. <p></p> </dd> - <?php dt("Adaptability.") ?> + <a name="tags"><?php dt("Tags.") ?></a> <dd> - Proof General is designed to be generic, so you can adapt it - to a new proof assistant if you know a little bit of Emacs - Lisp. + Tags are an editing feature which allow you to quickly locate the + definition or declaration of a particular identifier. Proof General + is supplied with utilities to make tag indexes for Emacs, for the + proof assistants LEGO and Coq. This makes it easy to quickly access + definitions from a standard library, for example, and in large proof + developments split across multiple files. +<!-- <?php footnote("Tags programs are provided for LEGO and Coq") ?> --> + <p></p> + </dd> + <a name="generic"><?php dt("Adaptability.") ?></a> + <dd> + Proof General is designed to be adaptable. Many aspects + of its behaviour can be easily customized (using dialogue boxes and + buttons, no text file editing!). + <p> + Most importantly, Proof General is generic, so you can adapt it to + a new proof assistant with surprisingly little effort. <p> Adapting for a new proof assistant is mainly a matter of setting some variables with regular expressions to help parse output from the prover, and setting other variables with commands to send to the - prover. - To get the most from Proof General (proof-by-pointing, for example), - it may be necessary to augment the output routines of the + prover. To get the most from Proof General (proof by pointing, for + example), it may be necessary to augment the output routines of the proof assistant. </p> Please feel free to download Proof General to customize it for a new @@ -133,9 +161,8 @@ assistant, and you'd like some of the following features: how you get on. </dd> </dl> - <p> -For more details of the above features, see the +For (even) more details of the above features, see the <?php link_root("doc","documentation page.") ?> </p> |