From 3db20b5e170667464a58430f4386b1de02a329b0 Mon Sep 17 00:00:00 2001
From: Christophe Raffalli <christophe.raffalli@univ-savoie.fr>
Date: Wed, 12 Oct 2005 20:27:40 +0000
Subject: added lock and unlock for unification variables

---
 phox/phox-lang.el  | 10 ++++++++++
 phox/phox-pbrpm.el | 34 +++++++++++++++++++++++++++++++---
 2 files changed, 41 insertions(+), 3 deletions(-)

(limited to 'phox')

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
-- 
cgit v1.2.3