Nous avons procédé ce jeudi matin 08 avril 2021 à une MAJ de sécurité urgente. Nous sommes passé de la version 13.9.3 à la version 13.9.5 les releases notes correspondantes sont ici:

Commit c92dfdd3 authored by Sylvain Dailler's avatar Sylvain Dailler

Added a real end of goal for PG.

On some examples, goal was cut when first end was encountered.
parent 57d3ba2c
......@@ -18,17 +18,14 @@
(defun set-shell-vars()
"configure Proof General shell for Why3ITP"
proof-shell-start-goals-regexp "====================== Task ====================="
proof-shell-start-goals-regexp "====================== Task ====================="
proof-shell-restart-cmd "r\n"
proof-shell-end-goals-regexp "end"
proof-shell-end-goals-regexp "================================================="
proof-shell-quit-cmd "q\n"
proof-shell-annotated-prompt-regexp "^> "
proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
proof-shell-init-cmd "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"))
(defun get-prog-name ()
(concat "why3shell " (replace-regexp-in-string ".whyitp" ".why" (buffer-file-name ()))))
(defun set-prog-name ()
(setq proof-prog-name (concat "why3shell " (replace-regexp-in-string ".whyitp" ".why" (buffer-file-name ())))))
......@@ -416,7 +416,7 @@ let print_sequent _args ?old:_ fmt =
let tables = build_name_tables task in
let ut = Task.used_symbols (Task.used_theories task) in
let ld = Task.local_decls task ut in
fprintf fmt "@[<v 0>%a@]"
fprintf fmt "@[<v 0>%a \n=================================================@]"
(Pp.print_list Pp.newline (print_decl tables)) ld)))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment