From 073c68daada4d9aca39f24ded3e5a6321f9a4b8b Mon Sep 17 00:00:00 2001 From: ProofGeneral Bot <37002148+proofbot@users.noreply.github.com> Date: Fri, 23 Feb 2024 14:18:22 +0000 Subject: [PATCH] Auto-Update {userman, adaptingman} href: https://github.com/ProofGeneral/PG/commit/1f0724813a4eacb59b7a8d8905619c893d12f03b --- .../Beginning-with-a-New-Prover.html | 2 +- doc/master/adaptingman/Concept-Index.html | 2 +- .../Configuring-Editing-Syntax.html | 2 +- .../adaptingman/Configuring-Font-Lock.html | 2 +- ...figuring-Proof_002dTree-Visualization.html | 106 +++++------------- .../adaptingman/Configuring-Tokens.html | 2 +- .../Demonstration-Instantiations.html | 2 +- doc/master/adaptingman/Function-Index.html | 4 +- doc/master/adaptingman/Global-Constants.html | 2 +- .../adaptingman/Goals-Buffer-Settings.html | 2 +- .../adaptingman/Handling-Multiple-Files.html | 2 +- .../Internals-of-Proof-General.html | 2 +- doc/master/adaptingman/Introduction.html | 2 +- ...d-Toolbar-and-User_002dlevel-Commands.html | 2 +- doc/master/adaptingman/PG-adapting_abt.html | 4 +- doc/master/adaptingman/PG-adapting_toc.html | 2 +- doc/master/adaptingman/Plans-and-Ideas.html | 2 +- .../adaptingman/Proof-Script-Settings.html | 2 +- .../adaptingman/Proof-Shell-Settings.html | 2 +- .../adaptingman/Splash-Screen-Settings.html | 2 +- doc/master/adaptingman/Variable-Index.html | 6 +- .../adaptingman/Writing-More-Lisp-Code.html | 2 +- doc/master/adaptingman/index.html | 2 +- ...dvanced-Script-Management-and-Editing.html | 2 +- .../userman/Basic-Script-Management.html | 2 +- doc/master/userman/Bugs-and-Enhancements.html | 2 +- doc/master/userman/Concept-Index.html | 2 +- doc/master/userman/Coq-Proof-General.html | 6 +- .../userman/Customizing-Proof-General.html | 2 +- .../userman/EasyCrypt-Proof-General.html | 2 +- doc/master/userman/Function-Index.html | 2 +- ...raphical-Proof_002dTree-Visualization.html | 12 +- doc/master/userman/Hints-and-Tips.html | 2 +- .../userman/History-of-Proof-General.html | 2 +- .../userman/Introducing-Proof-General.html | 2 +- doc/master/userman/Keystroke-Index.html | 2 +- .../userman/Obtaining-and-Installing.html | 2 +- doc/master/userman/Preface.html | 2 +- doc/master/userman/ProofGeneral_22.html | 2 +- doc/master/userman/ProofGeneral_abt.html | 4 +- doc/master/userman/ProofGeneral_fot.html | 2 +- doc/master/userman/ProofGeneral_toc.html | 2 +- doc/master/userman/References.html | 2 +- doc/master/userman/Shell-Proof-General.html | 2 +- ...term-Activation-and-Proof-by-Pointing.html | 2 +- .../userman/Support-for-other-Packages.html | 2 +- ...de-symbols-and-special-layout-support.html | 2 +- doc/master/userman/Variable-Index.html | 2 +- doc/master/userman/index.html | 2 +- 49 files changed, 86 insertions(+), 140 deletions(-) diff --git a/doc/master/adaptingman/Beginning-with-a-New-Prover.html b/doc/master/adaptingman/Beginning-with-a-New-Prover.html index 6f427f3..ae95bee 100644 --- a/doc/master/adaptingman/Beginning-with-a-New-Prover.html +++ b/doc/master/adaptingman/Beginning-with-a-New-Prover.html @@ -258,7 +258,7 @@

1.3 Major modes used by Proof General

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Concept-Index.html b/doc/master/adaptingman/Concept-Index.html index 1b0522d..98c8a53 100644 --- a/doc/master/adaptingman/Concept-Index.html +++ b/doc/master/adaptingman/Concept-Index.html @@ -141,7 +141,7 @@

Concept Index

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Configuring-Editing-Syntax.html b/doc/master/adaptingman/Configuring-Editing-Syntax.html index ea7586b..4c586b6 100644 --- a/doc/master/adaptingman/Configuring-Editing-Syntax.html +++ b/doc/master/adaptingman/Configuring-Editing-Syntax.html @@ -86,7 +86,7 @@

9. Configuring Editing Syntax

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Configuring-Font-Lock.html b/doc/master/adaptingman/Configuring-Font-Lock.html index e3c809a..8219bc0 100644 --- a/doc/master/adaptingman/Configuring-Font-Lock.html +++ b/doc/master/adaptingman/Configuring-Font-Lock.html @@ -104,7 +104,7 @@

10. Configuring Font Lock

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html b/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html index b8d9c3a..265a141 100644 --- a/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html +++ b/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html @@ -19,6 +19,10 @@

12. Configuring Proof-Tree Visualization

+

Parts of this section are outdated. Please create an issue at +github.com/ProofGeneral/Proof General if you have a question for +adapting Prooftree for a new proof assistant. +

The proof-tree visualization feature was written with the idea of supporting Coq as well as other proof assistants. Nevertheless, supporting proof-tree visualization for a second proof assistant @@ -59,18 +63,9 @@

12.1 A layered set of proof trees

have been added to the proof after the first proof tree was completed. And so on.

-

To organize the layers, Prooftree must identify those proof -commands that add new goals to a proof. +

Prooftree assumes a new layer when it receives new goals in a state +where the number of open goals is zero.

-
-
Variable: proof-tree-new-layer-command-regexp
-

Regexp to match proof commands that add new goals to a proof.
-This regexp must match the command that turns the proof assistant -into prover mode, which adds the initial goal to the proof. It -must further match commands that add additional goals after all -previous goals have been proved. -

-
@@ -188,9 +183,7 @@

12.3.1 Organization of the Code

The main task of the Elisp code is to extract goals, undo events and information about existential variables from the proof-assistant output and to send all this data to Prooftree. -The Elisp code does also determine if additional output must be -requested from the proof assistant. In that case it adds -appropriate commands to proof-action-list, see section Proof script mode. These additional commands are flagged with +Additional commands inserted by Prooftree are flagged with proof-tree-show-subgoal, no-goals-display and no-response-display. The flag proof-tree-show-subgoal ensures that a number of internal @@ -198,52 +191,6 @@

12.3.1 Organization of the Code

ensure that their output is neither displayed in the goals nor the response buffer.

-

For the decision about which goals must be sent to Prooftree, the -Elisp code maintains the following two state variables. -

-
-
Variable: proof-tree-sequent-hash
-

Hash table to remember sequent ID’s.
-Needed because some proof assistants do not distinguish between -new subgoals, which have been created by the last proof command, -and older, currently unfocussed subgoals. If Proof General meets -a goal, it is treated as new subgoal if it is not in this hash yet. -

-

The hash is mostly used as a set of sequent ID’s. However, for -undo operations it is necessary to delete all those sequents from -the hash that have been created in a state later than the undo -state. For this purpose this hash maps sequent ID’s to the state -number in which the sequent has been created. -

-

The hash table is initialized in ‘proof-tree-start-process’. -

- - -
-
Variable: proof-tree-existentials-alist
-

Alist mapping existential variables to sequent ID’s.
-Used to remember which goals need a refresh when an existential -variable gets instantiated. To support undo commands the old -contents of this list must be stored in -‘proof-tree-existentials-alist-history’. To ensure undo is -properly working, this variable should only be changed by using -‘proof-tree-delete-existential-assoc’, -‘proof-tree-add-existential-assoc’ or -‘proof-tree-clear-existentials’. -

- -

When retracting these two variables must be set to their previous -state. For proof-tree-sequent-hash this is done with the -state numbers that are stored in the hash. For -proof-tree-existentials-alist a separate alist stores -previous states. -

-
-
Variable: proof-tree-existentials-alist-history
-

Alist mapping state numbers to old values of ‘proof-tree-existentials-alist’.
-Needed for undo. -

-

In Prooftree the separation between generic and proof-assistant specific code is less obvious. The Coq specific code is in the @@ -364,27 +311,28 @@

12.3.4 Urgent and Delayed Actions

speed, the amount of urgent code should be kept small.

-
Function: proof-tree-urgent-action flags
-

Handle urgent points before the next item is sent to the proof assistant.
-Schedule goal updates when existential variables have changed and -call ‘proof-tree-urgent-action-hook’. All this is only done if -the current output does not come from a command (with the -'proof-tree-show-subgoal flag) that this package inserted itself. -

-

Urgent actions are only needed if the external proof display is -currently running. Therefore this function should not be called -when ‘proof-tree-external-display’ is nil. -

-

This function assumes that the prover output is not suppressed. -Therefore, ‘proof-tree-external-display’ being t is actually a -necessary precondition. -

-

The not yet delayed output is in the region -[proof-shell-delayed-output-start, proof-shell-delayed-output-end]. +

Function: proof-tree-check-proof-finish last-item
+

Urgent action to delay processing at proof end.
+This function is called from ‘proof-shell-exec-loop’ after the +old item has been removed and before the next item from +‘proof-action-list’ is sent to the proof assistant. Of course +only when the proof-tree display is active. At the end of the +proof, this function delays items just following the previous +proof until all show-goal commands from prooftree and the +‘proof-tree-display-stop-command’ (which switches the dependent +evar line off for Coq) have been processed. +

+

If this function detects the end of the proof, it moves +non-priority items following in ‘proof-action-list’ to +‘proof-tree--delayed-actions’ and sets +‘proof-second-action-list-active’. When later the command from +‘proof-tree-display-stop-command’ is recognized, the items are +moved back. If no items follow the end of the previous proof, +‘proof-tree-display-stop-command’ is set to t.

-

The function proof-tree-urgent-action is called at a point +

The function proof-tree-check-proof-finish is called at a point where it is save to manipulate proof-action-list. This is essential, because proof-tree-urgent-action inserts goal display commands into proof-action-list when existential @@ -507,7 +455,7 @@

12.4.2 Prooftree Adaption

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Configuring-Tokens.html b/doc/master/adaptingman/Configuring-Tokens.html index 409e1af..b9ef7f8 100644 --- a/doc/master/adaptingman/Configuring-Tokens.html +++ b/doc/master/adaptingman/Configuring-Tokens.html @@ -78,7 +78,7 @@

11. Configuring Tokens

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Demonstration-Instantiations.html b/doc/master/adaptingman/Demonstration-Instantiations.html index 88856c2..cac5781 100644 --- a/doc/master/adaptingman/Demonstration-Instantiations.html +++ b/doc/master/adaptingman/Demonstration-Instantiations.html @@ -261,7 +261,7 @@

B.2 demoisa.el

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Function-Index.html b/doc/master/adaptingman/Function-Index.html index a146994..98d8c5c 100644 --- a/doc/master/adaptingman/Function-Index.html +++ b/doc/master/adaptingman/Function-Index.html @@ -79,9 +79,9 @@

Function and Command Index

proof-shell-process-urgent-message14.6.2 Output from the shell proof-shell-restart14.6 Proof shell mode proof-shell-start14.6 Proof shell mode +proof-tree-check-proof-finish12.3.4 Urgent and Delayed Actions proof-tree-external-display-toggle12.3.3 Guards proof-tree-handle-delayed-output12.3.4 Urgent and Delayed Actions -proof-tree-urgent-action12.3.4 Urgent and Delayed Actions proof-zap-commas10. Configuring Font Lock
@@ -104,7 +104,7 @@

Function and Command Index

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Global-Constants.html b/doc/master/adaptingman/Global-Constants.html index 36764e5..bf6f46c 100644 --- a/doc/master/adaptingman/Global-Constants.html +++ b/doc/master/adaptingman/Global-Constants.html @@ -55,7 +55,7 @@

7. Global Constants

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Goals-Buffer-Settings.html b/doc/master/adaptingman/Goals-Buffer-Settings.html index ace990f..125d921 100644 --- a/doc/master/adaptingman/Goals-Buffer-Settings.html +++ b/doc/master/adaptingman/Goals-Buffer-Settings.html @@ -102,7 +102,7 @@

5. Goals Buffer Settings

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Handling-Multiple-Files.html b/doc/master/adaptingman/Handling-Multiple-Files.html index 844279f..5e3de90 100644 --- a/doc/master/adaptingman/Handling-Multiple-Files.html +++ b/doc/master/adaptingman/Handling-Multiple-Files.html @@ -190,7 +190,7 @@

8. Handling Multiple Files

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Internals-of-Proof-General.html b/doc/master/adaptingman/Internals-of-Proof-General.html index 6685a0e..09644dc 100644 --- a/doc/master/adaptingman/Internals-of-Proof-General.html +++ b/doc/master/adaptingman/Internals-of-Proof-General.html @@ -1256,7 +1256,7 @@

14.7 Debugging

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Introduction.html b/doc/master/adaptingman/Introduction.html index bcd525d..7615369 100644 --- a/doc/master/adaptingman/Introduction.html +++ b/doc/master/adaptingman/Introduction.html @@ -121,7 +121,7 @@

Credits

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html b/doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html index 14d5b7d..103f458 100644 --- a/doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html +++ b/doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html @@ -179,7 +179,7 @@

2.3 Toolbar configuration

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/PG-adapting_abt.html b/doc/master/adaptingman/PG-adapting_abt.html index 25cc8f9..42289ba 100644 --- a/doc/master/adaptingman/PG-adapting_abt.html +++ b/doc/master/adaptingman/PG-adapting_abt.html @@ -14,7 +14,7 @@

About This Document

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.

The buttons in the navigation panels have the following meaning: @@ -124,7 +124,7 @@

About This Document

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/PG-adapting_toc.html b/doc/master/adaptingman/PG-adapting_toc.html index 8e4fb34..aaa28fe 100644 --- a/doc/master/adaptingman/PG-adapting_toc.html +++ b/doc/master/adaptingman/PG-adapting_toc.html @@ -129,7 +129,7 @@

Table of Contents

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Plans-and-Ideas.html b/doc/master/adaptingman/Plans-and-Ideas.html index 5796a69..339f484 100644 --- a/doc/master/adaptingman/Plans-and-Ideas.html +++ b/doc/master/adaptingman/Plans-and-Ideas.html @@ -167,7 +167,7 @@

A.3 Browser mode for script files and theories

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Proof-Script-Settings.html b/doc/master/adaptingman/Proof-Script-Settings.html index 319ca7a..203f125 100644 --- a/doc/master/adaptingman/Proof-Script-Settings.html +++ b/doc/master/adaptingman/Proof-Script-Settings.html @@ -843,7 +843,7 @@

3.11 Completions

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Proof-Shell-Settings.html b/doc/master/adaptingman/Proof-Shell-Settings.html index b031887..6c0912c 100644 --- a/doc/master/adaptingman/Proof-Shell-Settings.html +++ b/doc/master/adaptingman/Proof-Shell-Settings.html @@ -748,7 +748,7 @@

4.5 Hooks and other settings

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Splash-Screen-Settings.html b/doc/master/adaptingman/Splash-Screen-Settings.html index a18bb3e..8fdb148 100644 --- a/doc/master/adaptingman/Splash-Screen-Settings.html +++ b/doc/master/adaptingman/Splash-Screen-Settings.html @@ -55,7 +55,7 @@

6. Splash Screen Settings

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Variable-Index.html b/doc/master/adaptingman/Variable-Index.html index 93413dd..867ad06 100644 --- a/doc/master/adaptingman/Variable-Index.html +++ b/doc/master/adaptingman/Variable-Index.html @@ -204,11 +204,7 @@

Variable and User Option Index

proof-tokens-extra-modes11. Configuring Tokens proof-toolbar-entries-default2.3 Toolbar configuration proof-tree-configured12.3.3 Guards -proof-tree-existentials-alist12.3.1 Organization of the Code -proof-tree-existentials-alist-history12.3.1 Organization of the Code proof-tree-external-display12.3.3 Guards -proof-tree-new-layer-command-regexp12.1 A layered set of proof trees -proof-tree-sequent-hash12.3.1 Organization of the Code proof-undo-n-times-cmd3.4 Configuring undo behaviour proof-universal-keys7. Global Constants
@@ -237,7 +233,7 @@

Variable and User Option Index

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/Writing-More-Lisp-Code.html b/doc/master/adaptingman/Writing-More-Lisp-Code.html index e0d06b5..c396246 100644 --- a/doc/master/adaptingman/Writing-More-Lisp-Code.html +++ b/doc/master/adaptingman/Writing-More-Lisp-Code.html @@ -248,7 +248,7 @@

13.4 Useful functions and macros

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/adaptingman/index.html b/doc/master/adaptingman/index.html index 7e180dd..565a0a4 100644 --- a/doc/master/adaptingman/index.html +++ b/doc/master/adaptingman/index.html @@ -80,7 +80,7 @@

Proof General

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Advanced-Script-Management-and-Editing.html b/doc/master/userman/Advanced-Script-Management-and-Editing.html index d77d5bd..020e1a7 100644 --- a/doc/master/userman/Advanced-Script-Management-and-Editing.html +++ b/doc/master/userman/Advanced-Script-Management-and-Editing.html @@ -550,7 +550,7 @@

3.10 Editing features

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Basic-Script-Management.html b/doc/master/userman/Basic-Script-Management.html index 460b0ee..615203b 100644 --- a/doc/master/userman/Basic-Script-Management.html +++ b/doc/master/userman/Basic-Script-Management.html @@ -1109,7 +1109,7 @@

2.9 Interrupting during trace output

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Bugs-and-Enhancements.html b/doc/master/userman/Bugs-and-Enhancements.html index 2764ce9..5649491 100644 --- a/doc/master/userman/Bugs-and-Enhancements.html +++ b/doc/master/userman/Bugs-and-Enhancements.html @@ -50,7 +50,7 @@

B. Bugs and Enhancements

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Concept-Index.html b/doc/master/userman/Concept-Index.html index ff636a6..bcaeda1 100644 --- a/doc/master/userman/Concept-Index.html +++ b/doc/master/userman/Concept-Index.html @@ -285,7 +285,7 @@

Concept Index

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Coq-Proof-General.html b/doc/master/userman/Coq-Proof-General.html index b114197..1414765 100644 --- a/doc/master/userman/Coq-Proof-General.html +++ b/doc/master/userman/Coq-Proof-General.html @@ -1202,8 +1202,8 @@

10.9 Holes feature

10.10 Proof-Tree Visualization

-

Starting with Proof General version 4.2 and Coq version 8.4, Coq -Proof General has full support for proof-tree visualization, +

Starting with Proof General version 4.5 and Coq version 8.11, Coq +Proof General has (again) full support for proof-tree visualization, see section Graphical Proof-Tree Visualization. To find out which versions of Prooftree are compatible with this version of Proof General, see section Graphical Proof-Tree Visualization or the @@ -1312,7 +1312,7 @@

10.12 Opam-switch-mode support

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Customizing-Proof-General.html b/doc/master/userman/Customizing-Proof-General.html index dacd1a6..f81f298 100644 --- a/doc/master/userman/Customizing-Proof-General.html +++ b/doc/master/userman/Customizing-Proof-General.html @@ -774,7 +774,7 @@

8.6 Tweaking configuration settings

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/EasyCrypt-Proof-General.html b/doc/master/userman/EasyCrypt-Proof-General.html index 04e1e39..770dab3 100644 --- a/doc/master/userman/EasyCrypt-Proof-General.html +++ b/doc/master/userman/EasyCrypt-Proof-General.html @@ -101,7 +101,7 @@

11.3 EasyCrypt customizations

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Function-Index.html b/doc/master/userman/Function-Index.html index 5f02a36..02e2584 100644 --- a/doc/master/userman/Function-Index.html +++ b/doc/master/userman/Function-Index.html @@ -138,7 +138,7 @@

Function and Command Index

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Graphical-Proof_002dTree-Visualization.html b/doc/master/userman/Graphical-Proof_002dTree-Visualization.html index 67b5045..22726a2 100644 --- a/doc/master/userman/Graphical-Proof_002dTree-Visualization.html +++ b/doc/master/userman/Graphical-Proof_002dTree-Visualization.html @@ -20,12 +20,14 @@

7. Graphical Proof-Tree Visualization

-

Since version 4.2, Proof General supports proof-tree +

Since version 4.5, Proof General (again) supports proof-tree visualization on graphical desktops via the additional program -Prooftree. Currently, proof-tree visualization is only supported -for the Coq proof assistant. +Prooftree. Currently, proof-tree visualization is only supported for +the Coq proof assistant. (Proof-tree visualization was already +supported in version 4.2 but then discontinued in 2017 when Coq 8.7 +dropped the variant of Show Goal that prooftree relied on.)

-

This version of Proof General requires Prooftree version 0.11. +

This version of Proof General requires Prooftree version 0.14. Check the Prooftree website, to see if some later versions are also compatible. (Because of the communication protocol, Proof General is always only @@ -150,7 +152,7 @@

7.3 Prooftree Customization

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Hints-and-Tips.html b/doc/master/userman/Hints-and-Tips.html index e370101..e04754e 100644 --- a/doc/master/userman/Hints-and-Tips.html +++ b/doc/master/userman/Hints-and-Tips.html @@ -211,7 +211,7 @@

9.3 Using abbreviations

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/History-of-Proof-General.html b/doc/master/userman/History-of-Proof-General.html index 6ab718f..248ffa4 100644 --- a/doc/master/userman/History-of-Proof-General.html +++ b/doc/master/userman/History-of-Proof-General.html @@ -379,7 +379,7 @@

Old News for 3.7

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Introducing-Proof-General.html b/doc/master/userman/Introducing-Proof-General.html index fb08de5..1efe216 100644 --- a/doc/master/userman/Introducing-Proof-General.html +++ b/doc/master/userman/Introducing-Proof-General.html @@ -351,7 +351,7 @@

1.6 Organization of this manual

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Keystroke-Index.html b/doc/master/userman/Keystroke-Index.html index 04d69c0..b0b9044 100644 --- a/doc/master/userman/Keystroke-Index.html +++ b/doc/master/userman/Keystroke-Index.html @@ -77,7 +77,7 @@

Keystroke Index

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Obtaining-and-Installing.html b/doc/master/userman/Obtaining-and-Installing.html index b0d03de..4fa2c9f 100644 --- a/doc/master/userman/Obtaining-and-Installing.html +++ b/doc/master/userman/Obtaining-and-Installing.html @@ -187,7 +187,7 @@

Removing support for unwanted provers

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Preface.html b/doc/master/userman/Preface.html index e811e12..fb4c5a4 100644 --- a/doc/master/userman/Preface.html +++ b/doc/master/userman/Preface.html @@ -322,7 +322,7 @@

Credits

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/ProofGeneral_22.html b/doc/master/userman/ProofGeneral_22.html index f73c73e..5b3fb78 100644 --- a/doc/master/userman/ProofGeneral_22.html +++ b/doc/master/userman/ProofGeneral_22.html @@ -154,7 +154,7 @@

Concept Index: U – X

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/ProofGeneral_abt.html b/doc/master/userman/ProofGeneral_abt.html index 93a8a1c..550e37e 100644 --- a/doc/master/userman/ProofGeneral_abt.html +++ b/doc/master/userman/ProofGeneral_abt.html @@ -14,7 +14,7 @@

About This Document

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.

The buttons in the navigation panels have the following meaning: @@ -124,7 +124,7 @@

About This Document

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/ProofGeneral_fot.html b/doc/master/userman/ProofGeneral_fot.html index c75803c..27e51cc 100644 --- a/doc/master/userman/ProofGeneral_fot.html +++ b/doc/master/userman/ProofGeneral_fot.html @@ -51,7 +51,7 @@

(1)

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/ProofGeneral_toc.html b/doc/master/userman/ProofGeneral_toc.html index 8568fdd..6fcb02b 100644 --- a/doc/master/userman/ProofGeneral_toc.html +++ b/doc/master/userman/ProofGeneral_toc.html @@ -190,7 +190,7 @@

Table of Contents

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/References.html b/doc/master/userman/References.html index ebab8f7..6ec159c 100644 --- a/doc/master/userman/References.html +++ b/doc/master/userman/References.html @@ -64,7 +64,7 @@

References

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Shell-Proof-General.html b/doc/master/userman/Shell-Proof-General.html index 3d01a7a..e5d014f 100644 --- a/doc/master/userman/Shell-Proof-General.html +++ b/doc/master/userman/Shell-Proof-General.html @@ -60,7 +60,7 @@

12. Shell Proof General

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Subterm-Activation-and-Proof-by-Pointing.html b/doc/master/userman/Subterm-Activation-and-Proof-by-Pointing.html index a685368..07e2fae 100644 --- a/doc/master/userman/Subterm-Activation-and-Proof-by-Pointing.html +++ b/doc/master/userman/Subterm-Activation-and-Proof-by-Pointing.html @@ -124,7 +124,7 @@

6.1 Goals buffer commands

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Support-for-other-Packages.html b/doc/master/userman/Support-for-other-Packages.html index e713ef8..eae71bf 100644 --- a/doc/master/userman/Support-for-other-Packages.html +++ b/doc/master/userman/Support-for-other-Packages.html @@ -271,7 +271,7 @@

5.5 Support for tags

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Unicode-symbols-and-special-layout-support.html b/doc/master/userman/Unicode-symbols-and-special-layout-support.html index d543f97..ee98b3a 100644 --- a/doc/master/userman/Unicode-symbols-and-special-layout-support.html +++ b/doc/master/userman/Unicode-symbols-and-special-layout-support.html @@ -454,7 +454,7 @@

4.7 Selecting suitable fonts

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/Variable-Index.html b/doc/master/userman/Variable-Index.html index dbde492..18f6df3 100644 --- a/doc/master/userman/Variable-Index.html +++ b/doc/master/userman/Variable-Index.html @@ -123,7 +123,7 @@

Variable and User Option Index

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.
diff --git a/doc/master/userman/index.html b/doc/master/userman/index.html index f2059c9..af9bc4a 100644 --- a/doc/master/userman/index.html +++ b/doc/master/userman/index.html @@ -78,7 +78,7 @@

Proof General

- This document was generated on February 19, 2024 using texi2html 1.82. + This document was generated on February 23, 2024 using texi2html 1.82.