diff options
| author |  Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2005-10-12 20:27:40 +0000 |
|---|---|---|
| committer | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2005-10-12 20:27:40 +0000 |
| commit | 3db20b5e170667464a58430f4386b1de02a329b0 (patch) | |
| tree | b1a99c68fe8abf657b41258ea3f1ca8e6d52b0de /phox | |
| parent | 06c64591dea79e8b71ca2d197f7695a8c6e55d5a (diff) | |
added lock and unlock for unification variables
Diffstat (limited to 'phox')
| -rw-r--r-- | phox/phox-lang.el | 10 | ||||
| -rw-r--r-- | phox/phox-pbrpm.el | 34 |
2 files changed, 41 insertions, 3 deletions
diff --git a/phox/phox-lang.el b/phox/phox-lang.el index a26f3bdc..d8456de8 100644 --- a/phox/phox-lang.el +++ b/phox/phox-lang.el @@ -34,6 +34,16 @@ (en (concat "Choose " s " = ")) (fr (concat "Choisissons " s " = ")))) +(defun phox-lang-lock (s) + (case phox-lang + (en (concat "Lock variable" s ".")) + (fr (concat "Vérouille la variable " s ".")))) + +(defun phox-lang-unlock (s) + (case phox-lang + (en (concat "Unlock variable" s ".")) + (fr (concat "Dévérouille la variable " s ".")))) + (defun phox-lang-prove () (case phox-lang (en "Let us prove \\[ \\].") diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el index 6a3dbdc7..307d3592 100644 --- a/phox/phox-pbrpm.el +++ b/phox/phox-pbrpm.el @@ -117,7 +117,16 @@ (if (and (string= (nth 1 click-infos) "none") region-infos) (setq pbrpm-rules-list (append pbrpm-rules-list - (phox-pbrpm-menu-from-string 1 + (phox-pbrpm-menu-from-string 0 + (concat "menu_intro " + (int-to-string (nth 0 click-infos)) + (let ((tmp "")) + (mapc (lambda (region-info) + (setq tmp + (concat tmp " \"" (nth 2 region-info) "\""))) + region-infos) + tmp))) + (phox-pbrpm-menu-from-string 1 (concat "menu_rewrite " (int-to-string (nth 0 click-infos)) " " (let ((tmp "")) @@ -209,7 +218,6 @@ "$" (nth 2 click-infos) ". "))))) - (message (nth 2 click-infos)) (if (and (char= (string-to-char (nth 2 click-infos)) ??) region-infos (not (cdr region-infos))) (setq pbrpm-rules-list @@ -223,7 +231,27 @@ (nth 2 click-infos) " " (nth 2 (car region-infos)) - ". "))))))))) + ". ")))))) + (if (char= (string-to-char (nth 2 click-infos)) ??) + (let ((r (proof-shell-invisible-cmd-get-result (concat "is_locked " + (nth 2 click-infos))))) + (if (char= (string-to-char r) ?t) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list 0 (phox-lang-unlock (nth 2 click-infos)) + (concat + goal-prefix + "unlock " + (nth 2 click-infos) + ". "))))) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list 0 (phox-lang-lock (nth 2 click-infos)) + (concat + goal-prefix + "lock " + (nth 2 click-infos) + ". "))))))))))) (setq pbrpm-rules-list |