diff options
| author | Jim Fehrle | 2020-08-23 16:09:10 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-09 19:25:25 -0700 |
| commit | 1d4bbefe5fe19306ab415e537863763a0a74134a (patch) | |
| tree | 5f7b0cdee92b519f312ad338af1ddfc101e643e3 /toplevel/g_toplevel.mlg | |
| parent | 6c5608acde0a9bbaa3e2f7317b9b5cf2de2699cd (diff) | |
Add an XML message for "Show Proof Diffs"
Add menu item that uses this
Diffstat (limited to 'toplevel/g_toplevel.mlg')
| -rw-r--r-- | toplevel/g_toplevel.mlg | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 1902103a3e..ef79f4562e 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -20,7 +20,7 @@ type vernac_toplevel = | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } - | VernacShowProofDiffs of bool + | VernacShowProofDiffs of Proof_diffs.diffOpt module Toplevel_ : sig val vernac_toplevel : vernac_toplevel option Entry.t @@ -52,7 +52,8 @@ GRAMMAR EXTEND Gram | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." -> - { Some (VernacShowProofDiffs (removed <> None)) } + { Some (VernacShowProofDiffs + (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) } | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None |