Open
Conversation
a) not explicitly setting the default value and b) not repeating attributes that are already set. Example (omitting escape character): Old: E : [92;49;22;23;24;27mev[39;49;22;23;24;27m [39;49;22;23;24;27mn[39;49;22;23;24;27m New: E : [92mev[0m n (92 is bright green, the other codes set default attributes).
… CoqIDE. Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG. Also provides an option to generate diffs in HTML in a file. Diffs are computed for the hypotheses and conclusion of the first goal between the old and new proofs. Strings are split into tokens using the Coq lexer, then the list of tokens are diffed using the Myers algorithm. A fixup routine (Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases. Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or "-diffs on|off|removed" on the OS command line. The "on" option shows only the new item with added text, while "removed" shows each modified item twice--once with the old value showing removed text and once with the new value showing added text. The highlights use 4 tags to specify the color and underline/strikeout. These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The first two are for added or removed text; the last two are for unmodified parts of a modified item. Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and "end.diff.*", but only on the first and last strings of the span.
(cherry picked from commit 096afff)
Merged
2 tasks
jfehrle
force-pushed
the
diffs
branch
4 times, most recently
from
b0672f9 to
fca201d
Compare
jfehrle
force-pushed
the
diffs
branch
2 times, most recently
from
ca90aa1 to
6e2e2ed
Compare
jfehrle
force-pushed
the
diffs
branch
9 times, most recently
from
2439864 to
2cf033a
Compare
jfehrle
force-pushed
the
diffs
branch
2 times, most recently
from
b166ae5 to
7a844ad
Compare
jfehrle
force-pushed
the
diffs
branch
4 times, most recently
from
a45adb6 to
97069f6
Compare
jfehrle
pushed a commit
that referenced
this pull request
Jan 22, 2019
add some more material (preliminary provided in "tuto2" directory)
jfehrle
added a commit
that referenced
this pull request
Jul 19, 2020
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Generate an HTML file with proof diffs. It is probably not general enough to be merged yet. Code is extracted from rocq-prover#6801 to allow for a good discussion of what this should be.
This is based on the jfehrle/coq/diffs branch, which hasn't been merged. Not sure if this this PR is useful as such or if I need to wait until diffs is merged (advice welcome).