diff options
| author |  Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2005-10-20 08:13:19 +0000 |
|---|---|---|
| committer | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2005-10-20 08:13:19 +0000 |
| commit | 2c70e6f34a3f794feaebd44f42e367e794127a6e (patch) | |
| tree | 1a9ce8ada7b3e45443fb498b6625417bceda19d0 /phox | |
| parent | 3db20b5e170667464a58430f4386b1de02a329b0 (diff) | |
bug fix
Diffstat (limited to 'phox')
| -rw-r--r-- | phox/phox-pbrpm.el | 24 | ||||
| -rw-r--r-- | phox/phox.el | 2 |
2 files changed, 16 insertions, 10 deletions
diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el index 307d3592..80c5f748 100644 --- a/phox/phox-pbrpm.el +++ b/phox/phox-pbrpm.el @@ -17,7 +17,7 @@ pg-pbrpm-start-hyp-regexp "^\\([A-Za-z0-9_.']+\\) := " pg-pbrpm-start-hyp-regexp-par-num 1 pg-pbrpm-start-concl-regexp "^ *|- " - pg-pbrpm-auto-select-regexp "\\(\\(\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)\\)\\(_+\\(\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)\\)\\)*\\)\\|\\(\\?[0-9]+\\)" + pg-pbrpm-auto-select-regexp "\\(\\(\\(['a-zA-Z0-9]+\\)\\|\\([][><=/~&+*^%!{}:-]+\\)\\)\\(_+\\(\\(['a-zA-Z0-9]+\\)\\|\\([][><=/~&+*^%!{}:-]+\\)\\)\\)*\\)\\|\\(\\?[0-9]+\\)" ) @@ -78,10 +78,11 @@ (setq cmd (concat cmd ";; "))))) (if (> prev 0) (setq cmd (concat cmd "idt")))))) cmd) - -(defun phox-pbrpm-generate-menu (click-infos region-infos) -; This FAKE function will be replace by a real 'generate-menu' once the code will be judged stable + +(defun phox-pbrpm-get-region-name (region-info) + (if (= (nth 0 region-info) 1) (nth 1 region-info) (nth 2 region-info))) +(defun phox-pbrpm-generate-menu (click-infos region-infos) "Use informations to build a list of (name , rule)" ;click-infos = (goal-number, "whole"/hyp-name/"none", expression, depth-tree-list) ;region-infos = idem if in the goal buffer, (0, "none", expression, nil ) if in another buffer, do not display if no region available. @@ -132,7 +133,7 @@ (let ((tmp "")) (mapc (lambda (region-info) (setq tmp - (concat tmp " " (nth 1 region-info)))) + (concat tmp " " (phox-pbrpm-get-region-name region-info)))) region-infos) tmp)))))) @@ -192,18 +193,23 @@ (let ((tmp "")) (mapc (lambda (region-info) (setq tmp - (concat tmp " " (nth 1 region-info)))) + (concat tmp " " (phox-pbrpm-get-region-name region-info)))) region-infos) tmp)))))) - ; is clicking on a token - (if (not (string= (nth 2 click-infos) "")) + ; is clicking on a token with no selection + (if (and (not region-infos) (not (string= (nth 2 click-infos) ""))) (let ((r (proof-shell-invisible-cmd-get-result (concat "is_definition " (int-to-string (nth 0 click-infos)) " \"" (nth 2 click-infos) + "\""))) + (ri (proof-shell-invisible-cmd-get-result (concat "is_definition " + (int-to-string (nth 0 click-infos)) + " \"" + (concat "$" (nth 2 click-infos)) "\"")))) - (if (char= (string-to-char r) ?t) + (if (or (char= (string-to-char r) ?t) (char= (string-to-char ri) ?t)) (setq pbrpm-rules-list (append pbrpm-rules-list (list (list 1 (concat diff --git a/phox/phox.el b/phox/phox.el index 204854e7..fa25363a 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -129,7 +129,7 @@ phox-strict-comments-regexp phox-ident-regexp) proof-save-with-hole-result 8 - proof-ignore-for-undo-count "\\`\\(constraints\\|flag\\|goals\\|pri\\(nt\\(_sort\\)?\\|ority\\)\\|eshow\\|search\\|depend\\)" + proof-ignore-for-undo-count "\\`\\(constraints\\|flag\\|goals\\|pri\\(nt\\(_sort\\)?\\|ority\\)\\|eshow\\|search\\|depend\\|menu_\\|is_\\)" proof-non-undoables-regexp "\\`\\(undo\\|abort\\)" proof-shell-error-regexp "^\\([^ \n\t\r]* \\)?\\(\\(e\\|E\\)rror\\)\\|\\(\\(f\\|F\\)ailure\\)" proof-goal-command "goal %s." |