diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-15 12:10:34 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-15 12:10:34 +0000 |
| commit | 3e9fc0816fc333ff80d158afa26bb70e403e6b1f (patch) | |
| tree | 3ff9aaf8a4ee303893428e8a22d9e064fceb525a /lego | |
| parent | e5a5aa225eb864da82c00870698d79befca977d8 (diff) | |
made many minor changes to the documentation
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/example.l | 2 | ||||
| -rw-r--r-- | lego/lego.el | 18 |
2 files changed, 5 insertions, 15 deletions
diff --git a/lego/example.l b/lego/example.l index a15ea588..52643424 100644 --- a/lego/example.l +++ b/lego/example.l @@ -1,4 +1,4 @@ -Module Walkthrough Import lib_logic; +Module example Import lib_logic; Goal and_commutes: {A,B:Prop}(and A B) -> (and B A); intros; andI; diff --git a/lego/lego.el b/lego/lego.el index 7ccba295..69914599 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -41,8 +41,9 @@ (defcustom lego-help-menu-list '(["The LEGO Reference Card" (browse-url lego-www-refcard) t] ["The LEGO library (WWW)" (browse-url lego-library-www-page) t]) - "List of menu items, as defined in `easy-menu-define' for LEGO - specific help." + "List of menu itemsfor LEGO specific help. + +See the documentation of `easy-menu-define' " :type '(repeat sexp) :group 'lego) @@ -74,16 +75,6 @@ Activates extended printing routines required for Proof General.") (defconst lego-interrupt-regexp "Interrupt.." "Regexp corresponding to an interrupt") -(defvar lego-path-name "LEGOPATH" - "The name of the environmental variable to search for modules. This - is used by \\{legogrep} to find the files corresponding to a - search.") - -(defvar lego-path-separator ":" - "A character indicating how the items in the \\{lego-path-name} are - separated.") - - ;; ----- web documentation (defcustom lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/" @@ -262,7 +253,7 @@ Given is the first SPAN which needs to be undone." (defun lego-goal-hyp () (cond - ((looking-at proof-shell-goal-regexp) + ((looking-at lego-goal-regexp) (cons 'goal (match-string 1))) ((looking-at proof-shell-assumption-regexp) (cons 'hyp (match-string 1))) @@ -467,7 +458,6 @@ We assume that module identifiers coincide with file names." proof-shell-error-regexp lego-error-regexp proof-shell-interrupt-regexp lego-interrupt-regexp proof-shell-assumption-regexp lego-id - proof-shell-goal-regexp lego-goal-regexp proof-shell-first-special-char ?\360 proof-shell-wakeup-char ?\371 proof-shell-start-char ?\372 |