Needs Update!


Interaction with Minlog.
========================

This text describes how to start Minlog and how to interact with Minlog
via Emacs.


The very first time
-------------------

Extend your .emacs file with the following definition:

(defun run-minlog ()
 "Start Minlog von Herrn Schwichtenberg"
 (interactive)
 (run-scheme "scheme -emacs -band /home/math/schwicht/minlog/src/minlog.com")


Every new session
-----------------

You can start a minlog session from Emacs, with the command:
  M-x run-minlog

This results in a new buffer for Scheme interaction, called
*scheme*. Here Scheme is active, with the definitions of minlog added
to the current environment. In this buffer you can type any
expression, using Emacs as editor. To evaluate an expression type C-x
C-e immediately after an expression. The result will be computed by
the Scheme-interpreter, and the result will be inserted in the
buffer. In the bottom of the Scheme-window you see:
Scheme: n [evaluator].  This n should always be 1. If an
(Scheme-)error occurs, this number is raised to n+1. You are in a copy
of Scheme, to be used for debugging. To proceed with Scheme, type 
C-c C-c to reenter level 1. If you forget this, new definitions may be
get lost. To learn more about the Emacs scheme-mode, try C-h m, or
describe-mode under the Help pull down menu.


Using the Interactive Theorem Prover
------------------------------------

A minlog-command is just a scheme function. You can call it by typing
a Scheme-expression as explained before. The minlog functions involved
with interactive theorem proving are special: They return no value,
but work via side-effects. One of the side effects is the manipulation
of the global variable pproof (the current partial proof). Another
side-effect is that the current goal and context are printed on the
screen.


Keeping a separate vernacular file
----------------------------------

It is handy to keep a separate file for the commandos you enter to
Minlog. In this way you can reproduce a minlog-session. To do this,
You split your window (with C-x 2) after starting Minlog. In the
second window, you load a file with "C-x C-f file". This file can be a
new file, or an existing one. If this file has the extension ".scm",
Emacs will understand that this buffer will serve as input buffer for
scheme.  Otherwise, you have to type "M-x scheme-mode" first.  In this
input buffer you can edit Scheme-expressions. With "C-x C-e" these
commands are evaluated by Scheme. The output appears in the *scheme*
window. In this way you can separate input and output. After a session
you can save the input (with C-x s) for later use.


Loading a vernacular file.
--------------------------

To load a file with scheme expressions (for example the commands of 
a previous minlog-session), you evaluate the scheme-expression:
(load "file"). This has the effect that all the commands in "file" are
executed.


Looking at the source file
--------------------------

It is often useful to have a look at the minlog-source file. There
is a quick way to find the definition of a minlog-function, using
the tag-file.

The command for looking for a tag is: 
  M-.      to get the source-code in this window.
  C-x 4 .  to get the source-code in another window.
  C-x 5 .  to get the source-code in another frame.

After typing M-. Emacs ask what to look for. The default is the word
under the cursor. Then Emacs ask where the tag-table is. This is in
"~schwicht/minlog/src".