From b63dd74e45d33d5493906b3c8caf00d0b84d8146 Mon Sep 17 00:00:00 2001
From: Christophe Raffalli <christophe.raffalli@univ-savoie.fr>
Date: Fri, 22 Dec 2000 14:03:10 +0000
Subject: *** empty log message ***

---
 phox/example.phx  | 15 ++++++++++++++-
 phox/phox-font.el |  4 ++--
 phox/phox.el      | 51 +++++++++++++++++++++++++++++++++++++--------------
 3 files changed, 53 insertions(+), 17 deletions(-)

(limited to 'phox')

diff --git a/phox/example.phx b/phox/example.phx
index 36ece411..a0edbe48 100644
--- a/phox/example.phx
+++ b/phox/example.phx
@@ -4,6 +4,19 @@
     $Id$
 *)
 
+(*
+goal /\n:N (ack n N1 >= N2).
+intro 2.
+elim H.
+trivial.
+elim -1 [case] H0.
+trivial.
+trivial.
+save ack_lem7.
+*)
+
 prop (* test *) (* just un test *) test /\X (X -> X).
+print $0.
 trivial.
-save.
\ No newline at end of file
+save.
+
diff --git a/phox/phox-font.el b/phox/phox-font.el
index 8c0816c9..29d40d9f 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -38,12 +38,12 @@
        "from\\|"
        "goals\\|"
        "in\\(tros?\\|stance\\)\\|"
-       "l\\(ocal\\|efts?\\)\\|"
+       "l\\(oc\\(al\\|k\\)\\|efts?\\)\\|"
        "next\\|"
        "r\\(e\\(write\\(_hyp\\)?\\|name\\)\\|mh\\)\\|"
        "slh\\|"
        "trivial\\|" 
-       "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\)\\)" 
+       "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)" 
        "\\)[ \t.]")
       '(0 'font-lock-type-face t))))
 
diff --git a/phox/phox.el b/phox/phox.el
index 87c1cdef..e0274faf 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -111,21 +111,44 @@
    proof-comment-start             "(*"
    proof-comment-end               "*)"
    proof-state-command             "goals."
-   proof-goal-command-regexp       "goal\\|prop\\(osition\\)?\\|em\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?"
-   proof-save-command-regexp       "save"
-   proof-goal-with-hole-regexp     (concat 
-     "\\(prop\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
-      phox-strict-comments-regexp
-      phox-ident-regexp)
-   proof-goal-with-hole-result     13
-   proof-save-with-hole-regexp     (concat 
-      "save"
-      phox-strict-comments-regexp
-      phox-ident-regexp)
-   proof-save-with-hole-result     8
-   proof-ignore-for-undo-count      "constraints\\|flag\\|goals\\|print\\(_sort\\)?\\|eshow\\|search\\|priority\\|depend"
+   proof-goal-command-regexp       
+   (concat
+    "^"
+    phox-comments-regexp
+    "\\(goal\\|prop\\(osition\\)?\\|em\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)")
+   proof-save-command-regexp       
+   (concat
+    "^"
+    phox-comments-regexp
+    "save")
+   proof-goal-with-hole-regexp  
+   (concat 
+    "^"
+    phox-comments-regexp
+    "\\(prop\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
+    phox-strict-comments-regexp
+    phox-ident-regexp)
+   proof-goal-with-hole-result     16
+   proof-save-with-hole-regexp     
+   (concat 
+    "^"
+    
+phox-comments-regexp
+    "save"
+    phox-strict-comments-regexp
+    phox-ident-regexp)
+   proof-save-with-hole-result     11
+   proof-ignore-for-undo-count         
+   (concat
+    "^"
+    phox-comments-regexp
+    "\\(constraints\\|flag\\|goals\\|print\\(_sort\\)?\\|eshow\\|search\\|priority\\|depend\\)")
+   proof-non-undoables-regexp       
+   (concat
+    "^"
+    phox-comments-regexp
+    "\\(undo\\|abort\\)")
    proof-shell-error-regexp        "^\\([^ \n\t\r]* \\)?\\(\\(e\\|E\\)rror\\)\\|\\(\\(f\\|F\\)ailure\\)"
-   proof-non-undoables-regexp      "undo\\|abort"
    proof-goal-command              "goal %s."
    proof-save-command              "save %s."
    proof-kill-goal-command         "abort."
-- 
cgit v1.2.3