Return-Path: Received: from EDRC.CMU.EDU by A.GP.CS.CMU.EDU id aa08174; 8 Mar 94 11:57:05 EST Received: from swan.cl.cam.ac.uk by EDRC.CMU.EDU id aa01752; 8 Mar 94 11:56:24 EST Received: from dcs.ed.ac.uk by swan.cl.cam.ac.uk via JANET with NIFTP (PP-6.5) id <27526-0@swan.cl.cam.ac.uk>; Tue, 8 Mar 1994 16:52:56 +0000 Received: from yell.dcs.ed.ac.uk by dcs.ed.ac.uk id aa12176; 8 Mar 94 16:51 GMT Message-Id: <19060.9403081651@yell.dcs.ed.ac.uk> Received: from da.localhost.dcs.ed.ac.uk by yell.dcs.ed.ac.uk; Tue, 8 Mar 94 16:51:45 GMT To: isabelle-users@cl.cam.ac.uk Subject: ANNOUNCEMENT: Isabelle mode for GNU Emacs Date: Tue, 08 Mar 94 16:51:43 GMT From: David Aspinall Dear Fellow Isabelle Users, I've developed an Emacs Lisp package which provides some useful facilities for Isabelle use. The hope is that the package will help make the learning curve for new Isabelle users less steep, whilst at the same time speeding up use for experienced users. More information follows below. Briefly (more details below), the facilities provided are: * Theory mode - for editing theory files * Isabelle mode - for interacting with Isabelle * Menus - including tactics and common proof commands * Listener - a buffer for recording interactive proofs * Proof-State - a buffer which displays the current proof state * Rule-table - rule names for the current logic Menus and mouse functions give Isabelle a primitive user-interface. They only work in the latest versions of Emacs - FSF GNU Emacs 19 (version 19.19 onwards) or Lucid GNU Emacs (version 19.6 onwards). The package is also compatible with GNU Emacs version 18.59. It is available by ftp from Edinburgh: ftp.dcs.ed.ac.uk directory /pub/da /pub/da/isa-mode directory containing package /pub/da/isa-mode.tar.gz compressed gzip'd tar file of above The code hasn't been tested extensively yet, so this version should be considered a beta-release for something more extensive and robust to follow. Please try it out and tell me of any problems or suggestions. Offers of help from any Emacs hackers out there would be particularly welcome! - David ------------ David Aspinall, email: David.Aspinall@dcs.ed.ac.uk Department of Computer Science, Tel: +44 31 650 5898 University of Edinburgh, King's Buildings, Edinburgh. ---------------------------------------------------------------------- Outline of Features provided by Isabelle Mode ---------------------------------------------------------------------- This package provides editing and interaction functions for the theorem prover Isabelle. When used with FSF Emacs 19 or Lucid Emacs, there is a system of menus and multiple windows. Here's what you get: * Theory mode - for editing theory files This mode understands the syntax for strings (automatic backslashes) and allows convenient switching to sml-mode in the "ML" section of theory files. It provides templates to help remind you of the syntax for theory files. There is a master menu to start-up an Isabelle session and view Isabelle documentation. * Isabelle mode - for interacting with Isabelle Isabelle is run in a shell-like buffer, based on the latest Emacs command-interpreter software. This provides useful command history, filename completion, tactic/tactical/command completion, and the usual advantages of running Isabelle inside Emacs. A collection of menus for common proof commands are provided. These insert command text into the Isabelle buffer. The interaction buffer can be used in conjunction with other special buffers... * Listener - a buffer for recording interactive proofs This receives a copy of the commands you type to Isabelle, to record interactive proofs. You can cut from this buffer and use "isa-batchify" (previously called "goalify") to very easily create batch proofs from interactive ones. Future versions of isa-mode will provide more advanced ways of using a "Listener"-like buffer, so that, for example, undo() commands may be interpreted. * Proof-State - a buffer which displays the current proof state This buffer maintains the display of the current proof state, removing it from the output in the Isabelle interaction buffer. The cursor keys can be used in this buffer to page back through previous levels of the proof, or select a "denoted" subgoal for the menu-driven tactic commands to use. * Rule-table - rule names for the current logic This buffer displays a formatted table of rule names for the logic in use. Mouse-clicking (or key-pressing in Emacs 18) on a rule name inserts it into the Isabelle interaction buffer, or displays the rule (as "prth" would) in a temporary buffer. In Emacs 19 varieties, each of the Isabelle interaction related buffers can appear in a separate X-window. In non-window environments, the pull-down menus degenerate to Emacs commands, and the special buffers are displayed in split Emacs "windows".