1 files changed, 41 insertions, 42 deletions
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)
 
+