diff options
-rw-r--r-- | generic/proof-script.el | 6 | ||||
-rw-r--r-- | phox/example.phx | 15 | ||||
-rw-r--r-- | phox/phox-font.el | 4 | ||||
-rw-r--r-- | phox/phox.el | 51 |
4 files changed, 58 insertions, 18 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index d25e83f5..964f826c 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2000,6 +2000,10 @@ up to the end of the locked region." ;; steps. ;; FIXME: really, there shouldn't be more work to do: so ;; why call proof-find-and-forget-fn later? + (progn + (message (int-to-string (span-end span))) + (message (int-to-string (span-end target))) + (if (< (span-end span) (span-end target)) (progn ;; Skip comment spans at and immediately following target @@ -2021,7 +2025,7 @@ up to the end of the locked region." (proof-setup-retract-action (span-start span) end proof-kill-goal-command delete-region) - end (span-start span)))) + end (span-start span))))) ;; Check the start of the target span lies before the end ;; of the locked region (should always be true since we don't ;; make spans outside the locked region at the moment)... 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." |