Renamed file

1 files changed, 182 insertions, 0 deletions

diff --git a/html/features.html b/html/features.html
new file mode 100644
index 00000000..372ab17b
--- /dev/null
+++ b/html/features.html
@@ -0,0 +1,182 @@
+<h2>Features of Proof General</h2>
+<p>
+It doesn't matter if you're an Emacs militant or a pacifist!
+</p>
+
+<p>
+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...
+</p>
+<dl>
+  <?php dt("Script management","script") ?>
+  <dd>
+  A <em>proof script</em> is a sequence of commands sent to
+  a proof assistant to construct a proof, usually stored in
+  a file.  <em>Script management</em> connects the editing of a 
+  proof script directly to an interactive proof process,
+  maintaining consistency between the edit buffer
+  and the state of the proof assistant.
+  <p>
+  Proof General colours a proof script to show the state in the proof
+  assistant.  Parts of a proof script that have been processed are
+  displayed in blue and are "locked" -- they cannot be edited.  Parts
+  of the script currently being processed by the proof assistant are
+  shown in red.  Proof General has commands for processing new parts
+  of the buffer, or undoing already processed parts.
+  </p>
+  <p>
+  Take a look at these
+  <a href="screenshot.phtml">screenshots</a>
+  of Proof General to see script managament in action.
+  </p>
+  </dd>
+  <?php dt("Simplified interaction","simple") ?>
+  <dd>
+  Proof General is designed for proof assistants which have a
+  command-line shell interpreter.  When using Proof General, the proof
+  assistant's shell is hidden from the user.  Communication takes
+  place via three buffers (Emacs text widgets).  The <i>script
+  buffer</i> holds input, the commands to construct a proof.  The
+  <i>goals buffer</i> displays the current list of subgoals to be
+  solved.  The <i>response buffer</i> displays other output from the
+  proof assistant.  By default, only two of these three buffers are
+  displayed at once.  This means that the user only sees the output
+  from the most recent interaction, rather than a screen full of
+  output from the proof assistant.
+  <p>
+  Despite this more friendly communication model, Proof General does not
+  commandeer the proof assistant shell: the user still has complete
+  access to it if necessary.
+  </p>
+</dd>
+  <?php dt("Multiple files","multiple") ?>
+  <dd>
+  Script management in Proof General can work across many script
+  files, integrating with the file handling of
+  the proof assistant.  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 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>
+  </dd>
+  <?php dt("Proof by Pointing","pbp") ?>
+  <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 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("Proof by pointing for Proof General is only supported by LEGO (experimentally) at the moment.  For others, we need help from each proof assistant implementor to add support for their system.  Please canvas the implementor of your favourite 
+proof assistant to add PBP support.")  ?>
+  </dd>
+  <?php dt("Toolbar and menus","toolbar") ?>
+  <dd>
+  Proof General has a toolbar with buttons for examining
+  the proof state, starting a proof, manoeuvring in the proof script, 
+  restarting the prover, saving a proof, searching for a theorem,
+  issuing a command, interrupting the assistant, and getting help.
+  <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","fontlock") ?>
+  <dd>
+  Syntax highlighting is an editing feature which decorates a file
+  with different colours or fonts according to the syntax of some
+  language (usually a programming language). 
+  <p>
+  Proof General decorates proof scripts: proof commands are
+  highlighted and different fonts may be used for definitions and
+  assumptions, for example.
+  </p>
+  </dd>
+  <?php dt("Real symbols","xsymbol") ?>
+  <dd>
+  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 "&not; P", instead
+   of "a * b", you see "a &times; b", etc. 
+  <br>
+   (Those examples are simple so they will work on most browsers 
+    without needing images, see the
+    <a href="screenshot.phtml">screenshots</a> for more examples.)
+  <p>
+  <?php footnote("X-Symbol currently works in XEmacs only") ?>
+  </dd>
+  <?php dt("Functions Menu","funcmenu") ?>
+  <dd>
+  A pull-down menu gives easy
+  navigations to theorems, definitions, and declarations
+  proved in the current buffer.  
+<!-- it is in FSF Emacs if you download func-menu.el from somewhere -->
+<!--   <?php footnote("Definitions menu is available in XEmacs only") ?> -->
+  <p>
+  </dd>
+  <?php dt("Remote proof assistant.") ?>
+  <dd>
+  Sometimes you may want to run a proof assistant on a powerful remote
+  machine.  Proof General can communicate with a proof assistant running
+  remotely, while your files and editor reside on your local machine.
+  <p></p>
+  </dd>
+  <?php dt("Tags","tags") ?>
+  <dd>
+  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.
+  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>
+  <?php dt("Adaptability","generic") ?>
+  <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.  See this basic
+ <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", 
+	  "example instance"); ?>.
+  To get the most from Proof General (proof by pointing, for
+  example), it may be necessary to put some hooks in
+  the output routines of the proof assistant.  
+  </p>
+  Please feel free to download Proof General to customize it for a new
+  system, and 
+  <?php hlink("feedback.phtml","tell us ","Feedback form")?>
+  how you get on.
+  </dd>
+</dl>
+<p>
+For (even) more details of the above features, see the 
+<?php link_root("doc","documentation page.") ?>
+</p>
+