*** empty log message ***

4 files changed, 263 insertions, 69 deletions

diff --git a/phox/phox-extraction.el b/phox/phox-extraction.el
new file mode 100644
index 00000000..b488d43e
--- /dev/null
+++ b/phox/phox-extraction.el
@@ -0,0 +1,170 @@
+;; $State$ $Date$ $Revision$ 
+;;--------------------------------------------------------------------------;;
+;;--------------------------------------------------------------------------;;
+;; program extraction.
+;;
+;; note : program extraction is still experimental This file is very
+;; dependant of the actual state of program extraction in phox.
+;;--------------------------------------------------------------------------;;
+;; configuration :
+
+(defvar phox-prog-orig "phox -pg" "original name of phox binary.")
+
+(defun phox-prog-flags-modify(option)
+"ask for a string that are options to pass to phox binary"
+(interactive "soption :")
+; pas d'analyse de la réponse, 
+(let ((process))
+  (if  (and phox-prog-name
+	    (progn (string-match " \\|$" phox-prog-name)
+		   (setq process 
+			 (substring phox-prog-name 0 (match-beginning 0))
+			 )
+		   )
+	    (processp (get-process process))
+	  (eq (process-status process) 'run))
+    (error "Error : exit phox process first !")
+  )
+(if (string-match "^ *$" option)
+    (progn
+      (message 
+       "no option other than default ones will be passed to phox binary.")
+      (setq phox-prog-name phox-prog-orig))
+  (progn
+    (message (format  "option %s will be passed to phox binary." option ))
+    (setq phox-prog-name (concat phox-prog-orig " " option))
+    )
+  )
+)
+)
+
+
+(defun phox-prog-flags-extract()
+"pass option -f to phox binary. A program can be extracted from
+proof of theorem_name with :
+compile theorem_name.
+output."
+(interactive)
+(phox-prog-flags-modify "-f")
+(message 
+"WARNING : program extraction is experimental and can disturb the prover !")
+)
+
+(defun phox-prog-flags-erase()
+"no option to phox binary."
+(interactive)
+(phox-prog-flags-modify ""))
+
+; encore une fonction qui devrait être redéfinie en cas d'autres
+; options possibles que -f
+
+(defun phox-toggle-extraction()
+"toggle between extraction mode and ordinary mode for phox process."
+(interactive)
+(cond ((string-equal phox-prog-name phox-prog-orig) ;; à améliorer (espaces)
+       (phox-prog-flags-extract))
+      ((string-match "\-f$" phox-prog-name) (phox-prog-flags-erase))
+      (t (error "option must be empty or -f, use phox-prog-flags-modify.")))
+)
+
+;; commands
+
+; compilation
+(defun phox-compile-theorem(name)
+  "Interactive function : 
+ask for the name of a theorem and send a compile command to PhoX for it."
+  (interactive "stheorem : ")
+  (proof-shell-invisible-command (concat "compile " name)))
+
+(defun phox-compile-theorem-on-cursor()
+"Interactive function : 
+send a compile command to PhoX for the theorem which name is under the cursor."
+  (interactive)
+  (let (start end)
+    (save-excursion
+;      (modify-syntax-entry ?\. "w")
+      (forward-word 1)
+      (setq start (point))
+      (forward-word -1)
+      (setq end (point)))
+    (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1)))
+    (phox-compile-theorem (buffer-substring start end))))
+
+; extraction
+
+(defun phox-output ()
+
+"Interactive function : 
+send output command to phox in order to obtain programs 
+extracted from proofs of all compiled theorems."
+
+
+(interactive)
+(proof-shell-invisible-command  "output"))
+
+(defun phox-output-theorem (name)
+"Interactive function : 
+ask for the name of a theorem and send an output command to PhoX for it
+in order to obtain a programm extracted from the known proof of this theorem."
+  (interactive "stheorem : ")
+  (proof-shell-invisible-command (concat "output " name)))
+
+(defun phox-output-theorem-on-cursor()
+"Interactive function : 
+send an output command to PhoX for the theorem which name is under the cursor
+in order to obtain a programm extracted from the known proof of this theorem."
+  (interactive)
+  (let (start 
+	end 
+;	(syntax (char-to-string (char-syntax ?\.)))
+	)
+    (save-excursion
+;      (modify-syntax-entry ?\. "w") ; à modifier globablement ?
+      (forward-word 1)
+      (setq start (point))
+      (forward-word -1)
+      (setq end (point)))
+;      (modify-syntax-entry ?\.  syntax)
+      (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1)))
+    (phox-output-theorem (buffer-substring start end))))
+
+; Definitions of lambda-mu terms (tdef nom_de_term = terme.) and
+; normalization (eval term.) have to be "visible" proof commands.
+
+;; menu
+
+  (defvar phox-extraction-menu
+    '("Extraction"
+      ["Program extraction enabled"
+       phox-toggle-extraction
+       :style radio
+       :selected(string-match "\-f$" phox-prog-name)
+       ]
+      ["------------------------------" nil nil
+       ]
+      ["Compile theorem on cursor" phox-compile-theorem-on-cursor 
+       :active(string-match "\-f$" phox-prog-name)
+       ]
+      ["Extraction for theorem on cursor" phox-output-theorem-on-cursor
+       :active(string-match "\-f$" phox-prog-name)
+       ]
+      ["Extraction for all compiled theorems" phox-output
+       :active(string-match "\-f$" phox-prog-name)
+       ]
+      ["------------------------------" nil nil
+       ]
+      ["Compile theorem : " phox-compile-theorem
+       :active(string-match "\-f$" phox-prog-name)
+       ]
+      ["Extraction for theorem : " phox-output-theorem
+       :active(string-match "\-f$" phox-prog-name)
+       ]
+      )
+"A list of menu items to deal with program extraction.
+Warning, program extraction is still experimental
+and can disturb the prover !"
+)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(provide 'phox-extraction)
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index 1c2735dd..f1ffa464 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -1,28 +1,5 @@
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;; program extraction.
-;;
-;; note : program extraction is still experimental
-;;--------------------------------------------------------------------------;;
-
-(defun phox-compile-theorem(name)
-  "Interactive function : 
-ask for the name of a theorem and send a compile command to PhoX for it."
-  (interactive "stheorem : ")
-  (proof-shell-invisible-command (concat "compile " name ".\n")))
-
-(defun phox-compile-theorem-around-point()
-"Interactive function : 
-send a compile command to PhoX for the theorem which name is under the cursor."
-  (interactive)
-  (let (start end)
-    (save-excursion
-      (forward-word 1)
-      (setq start (point))
-      (forward-word -1)
-      (setq end (point)))
-    (phox-compile-theorem (buffer-substring start end))))
-
+;; $State$ $Date$ $Revision$ 
+;; syntax
 
 (setq
  phox-forget-id-command "del %s.\n"
@@ -59,6 +36,23 @@ send a compile command to PhoX for the theorem which name is under the cursor."
    "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]")
 )
 
+
+(defun phox-init-syntax-table ()
+  "Set appropriate values for syntax table in current buffer."
+;; useful for using forward-word
+  (modify-syntax-entry ?_  "w")
+  (modify-syntax-entry ?\. "w")
+;; Configure syntax table for block comments
+  (modify-syntax-entry ?\* ". 23")
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4")
+;; à compléter éventuellement
+)
+
+
+
+
+
 (defun phox-find-and-forget (span)
   (let (str ans tmp (lsp -1))
     (while span 
@@ -107,20 +101,37 @@ send a compile command to PhoX for the theorem which name is under the cursor."
 
       (or ans proof-no-command)))
 
+;;
+;; Doing commands
+;;
+
+(defun phox-assert-next-command-interactive ()
+  "Process until the end of the next unprocessed command after point.
+If inside a comment, just process until the start of the comment."
+  (interactive)
+  (message "test")
+  (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n"))
+  (proof-with-script-buffer
+   (proof-maybe-save-point
+    (goto-char (proof-queue-or-locked-end))
+    (proof-assert-next-command))
+   (proof-maybe-follow-locked-end)))
+
+
 ;;--------------------------------------------------------------------------;;
 ;;
 ;;    Deleting symbols
 ;;
 ;;--------------------------------------------------------------------------;;
-
+;; obsolète probablement, sinon à modifier pour en étendre la portée.
 
 (defun phox-delete-symbol(symbol)
   "Interactive function : 
 ask for a symbol and send a delete command to PhoX for it."
   (interactive "ssymbol : ")
-  (proof-shell-invisible-command (concat "del " symbol ".\n")))
+  (proof-shell-invisible-command (concat "del " symbol)))
 
-(defun phox-delete-symbol-around-point()
+(defun phox-delete-symbol-on-cursor()
 "Interactive function : 
 send a delete command to PhoX for the symbol whose name is under the cursor."
   (interactive)
@@ -133,21 +144,9 @@ send a delete command to PhoX for the symbol whose name is under the cursor."
     (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1)))
     (phox-delete-symbol (buffer-substring start end))))
 
-;;
-;; Doing commands
-;;
 
-(defun phox-assert-next-command-interactive ()
-  "Process until the end of the next unprocessed command after point.
-If inside a comment, just process until the start of the comment."
-  (interactive)
-  (message "test")
-  (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n"))
-  (proof-with-script-buffer
-   (proof-maybe-save-point
-    (goto-char (proof-queue-or-locked-end))
-    (proof-assert-next-command))
-   (proof-maybe-follow-locked-end)))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (provide 'phox-fun)
 
+
diff --git a/phox/phox-tags.el b/phox/phox-tags.el
index f2b5959a..c983c347 100644
--- a/phox/phox-tags.el
+++ b/phox/phox-tags.el
@@ -1,3 +1,4 @@
+;; $State$ $Date$ $Revision$ 
 ;;--------------------------------------------------------------------------;;
 ;;--------------------------------------------------------------------------;;
 ;;                         gestion des TAGS
@@ -26,7 +27,7 @@
 					; gnu emacs
     (if (member table tags-table-list)
 	(message (concat table " already loaded."))
-;    (make-local-variable 'tags-table-list) ; ne focntionne pas
+;    (make-local-variable 'tags-table-list) ; ne fonctionne pas
       (setq tags-table-list (cons table tags-table-list))
       )
     )
@@ -51,7 +52,7 @@
 (defun phox-tags-add-lib-table()
   "Add tags in libraries."
   (interactive)
-  (phox-tags-add-table (concat phox-lib-dir "TAGS"))
+  (phox-tags-add-table (concat phox-lib-dir "/TAGS"))
   )
  
 (defun phox-tags-add-local-table()
@@ -70,8 +71,41 @@
 			 (file-name-nondirectory (buffer-file-name))))
   )
 
+
+(defun phox-complete-tag()
+"Complete symbol using tags table. Works with FSF emacs.
+ Problems with xemacs."
+;; xemacs build a table for completion, tag-completion-table
+;; this table donnot contains key words that use ".", probably a
+;; problem with syntax table.
+
+(if proof-running-on-XEmacs
+    (complete-tag)
+  (tag-complete-symbol)))
+
+;; menu
+
+(defvar phox-tags-menu
+     '("Tags"
+       ["create a tags table for local buffer" phox-tags-create-local-table t]
+       ["------------------" nil nil]
+       ["add table"               phox-tags-add-table       t]
+       ["add local table"         phox-tags-add-local-table t]
+       ["add table for libraries" phox-tags-add-lib-table   t]
+       ["add table for text doc"  phox-tags-add-doc-table   t]
+       ["reset tags table list"   phox-tags-reset-table     t]
+       ["------------------" nil nil]
+       ["Find theorem, definition ..." find-tag t]
+       ["complete theorem, definition ..." phox-complete-tag t]
+      )
+"Phox menu for dealing with tags"
+)
+
 ;; default
 
 (if phox-tags-doc (add-hook 'phox-mode-hook 'phox-tags-add-doc-table))
 
-(provide 'phox-tags)
\ No newline at end of file
+(provide 'phox-tags)
+
+
+
diff --git a/phox/phox.el b/phox/phox.el
index 0341b664..1a2ade5e 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -1,3 +1,5 @@
+;; $State$ $Date$ $Revision$ 
+
 (require 'proof)			; load generic parts
 
 ;; Adjust toolbar entries.  (Must be done
@@ -71,6 +73,7 @@
   :type 'string
   :group 'phox-config)
 
+(require 'phox-extraction)
 (require 'phox-tags)
 (require 'phox-outline)
 (require 'phox-font)
@@ -79,25 +82,15 @@
 ;; ----- PhoX specific menu
 
 (defpgdefault menu-entries
-  '(    
-    ["Delete symbol around cursor" phox-delete-symbol-around-point t]
-    ["Delete symbol" phox-delete-symbol t]
-    ["Compile theorem under cursor" phox-compile-theorem-around-point t]
-    "----"
-    ("Tags"
-     ["create a tags table for local buffer" phox-tags-create-local-table t]
-     ["------------------" nil nil]
-;    ["load table" phox-tags-load-table t]
-     ["add table"               phox-tags-add-table       t]
-     ["add local table"         phox-tags-add-local-table t]
-     ["add table for libraries" phox-tags-add-lib-table   t]
-     ["add table for text doc"  phox-tags-add-doc-table   t]
-     ["reset tags table list"   phox-tags-reset-table     t]
-     ["------------------" nil nil]
-     ["Find theorem, definition ..." find-tag t]
-     ["complete theorem, definition ..." complete-tag t]
-     )
-    ))
+  (cons
+   phox-tags-menu
+   (cons
+    phox-extraction-menu
+;; not useful ?
+;    '(["Delete symbol around cursor" phox-delete-symbol-around-point t]
+;    ["Delete symbol" phox-delete-symbol t])
+      nil))
+  )
 
 ;;
 ;; ======== Configuration of generic modes ========
@@ -139,6 +132,7 @@
    proof-auto-multiple-files       nil
    font-lock-keywords              phox-font-lock-keywords 
    )
+  (phox-init-syntax-table)
 )
 
 (defun phox-shell-config ()
@@ -177,11 +171,8 @@
     ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed"
 
     (define-key phox-mode-map [(control c) (meta d)] 
-      'phox-delete-symbol-around-point)  
-    ;; Configure syntax table for block comments
-    (modify-syntax-entry ?\* ". 23")
-    (modify-syntax-entry ?\( "()1")
-    (modify-syntax-entry ?\) ")(4"))
+      'phox-delete-symbol-on-cursor)  
+)
 
 (define-derived-mode phox-shell-mode proof-shell-mode
    "PhoX shell" nil