aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/v8-syntax/syntax-v8.tex1
-rw-r--r--doc/changelog/07-commands-and-options/10277-no-show-script.rst2
-rw-r--r--doc/changelog/12-misc/10019-PG-proof-diffs.rst3
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst20
-rw-r--r--ide/coq_commands.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--stm/stm.ml119
-rw-r--r--vernac/g_proofs.mlg1
-rw-r--r--vernac/ppvernac.ml1
-rw-r--r--vernac/vernacentries.ml2
-rw-r--r--vernac/vernacexpr.ml1
11 files changed, 20 insertions, 134 deletions
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index dd3908c25f..601d52ddda 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1167,7 +1167,6 @@ $$
\nlsep \TERM{Show}~\OPT{\NT{num}}
\nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}}
\nlsep \TERM{Show}~\TERM{Node}
-\nlsep \TERM{Show}~\TERM{Script}
\nlsep \TERM{Show}~\TERM{Existentials}
\nlsep \TERM{Show}~\TERM{Tree}
\nlsep \TERM{Show}~\TERM{Conjecture}
diff --git a/doc/changelog/07-commands-and-options/10277-no-show-script.rst b/doc/changelog/07-commands-and-options/10277-no-show-script.rst
new file mode 100644
index 0000000000..7fdeb632b4
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10277-no-show-script.rst
@@ -0,0 +1,2 @@
+- Remove ``Show Script`` command (deprecated since 8.10)
+ (`#10277 <https://github.com/coq/coq/pull/10277>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/12-misc/10019-PG-proof-diffs.rst b/doc/changelog/12-misc/10019-PG-proof-diffs.rst
new file mode 100644
index 0000000000..b2d191be26
--- /dev/null
+++ b/doc/changelog/12-misc/10019-PG-proof-diffs.rst
@@ -0,0 +1,3 @@
+- Proof General can now display Coq-generated diffs between proof steps
+ in color. (`#10019 <https://github.com/coq/coq/pull/10019>`_ and (in Proof General)
+ `#421 <https://github.com/ProofGeneral/PG/pull/421>`_, by Jim Fehrle).
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 3f966755ca..0cff987a27 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -535,19 +535,6 @@ Requesting information
eexists ?[n].
Show n.
- .. cmdv:: Show Script
- :name: Show Script
-
- Displays the whole list of tactics applied from the
- beginning of the current proof. This tactics script may contain some
- holes (subgoals not yet proved). They are printed under the form
-
- ``<Your Tactic Text here>``.
-
- .. deprecated:: 8.10
-
- Please use a text editor.
-
.. cmdv:: Show Proof
:name: Show Proof
@@ -705,9 +692,10 @@ command in CoqIDE. You can change the background colors shown for diffs from th
lets you control other attributes of the highlights, such as the foreground
color, bold, italic, underline and strikeout.
-Note: As of this writing (August 2018), Proof General will need minor changes
-to be able to show diffs correctly. We hope it will support this feature soon.
-See https://github.com/ProofGeneral/PG/issues/381 for the current status.
+As of June 2019, Proof General can also display Coq-generated proof diffs automatically.
+Please see the PG documentation section
+"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_)
+for details.
How diffs are calculated
````````````````````````
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index b0bafb7930..7f68f24c22 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -126,7 +126,6 @@ let commands = [
"Show Intros";
"Show Programs";
"Show Proof";
- "Show Script";
"Show Tree";*)
"Structure";
"Syntactic Definition";
@@ -221,7 +220,6 @@ let state_preserving = [
"Show Intro";
"Show Intros";
"Show Proof";
- "Show Script";
"Show Tree";
"Test Printing If";
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 216be3797b..de1b592337 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1489,8 +1489,6 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
}
)
)) pstate in
- (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
-(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in
()
(* Pp.msgnl (fun _ _ -> str "eqn finished"); *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 21f5ece244..b2bfa552b4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1060,99 +1060,6 @@ end = struct (* {{{ *)
end (* }}} *)
-(* indentation code for Show Script, initially contributed
- * by D. de Rauglaudre. Should be moved away.
- *)
-
-module ShowScript = struct
-
-let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
- (* ng1 : number of goals remaining at the current level (before cmd)
- ngl1 : stack of previous levels with their remaining goals
- ng : number of goals after the execution of cmd
- beginend : special indentation stack for { } *)
- let ngprev = List.fold_left (+) ng1 ngl1 in
- let new_ngl =
- if ng > ngprev then
- (* We've branched *)
- (ng - ngprev + 1, ng1 - 1 :: ngl1)
- else if ng < ngprev then
- (* A subgoal have been solved. Let's compute the new current level
- by discarding all levels with 0 remaining goals. *)
- let rec loop = function
- | (0, ng2::ngl2) -> loop (ng2,ngl2)
- | p -> p
- in loop (ng1-1, ngl1)
- else
- (* Standard case, same goal number as before *)
- (ng1, ngl1)
- in
- (* When a subgoal have been solved, separate this block by an empty line *)
- let new_nl = (ng < ngprev)
- in
- (* Indentation depth *)
- let ind = List.length ngl1
- in
- (* Some special handling of bullets and { }, to get a nicer display *)
- let pred n = max 0 (n-1) in
- let ind, nl, new_beginend = match Vernacprop.under_control cmd with
- | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
- | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
- | VernacBullet _ -> pred ind, nl, beginend
- | _ -> ind, nl, beginend
- in
- let pp = Pp.(
- (if nl then fnl () else mt ()) ++
- (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)))
- in
- (new_ngl, new_nl, new_beginend, pp :: ppl)
-
-let get_script prf =
- let branch, test =
- match prf with
- | None -> VCS.Branch.master, fun _ -> true
- | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
- let rec find acc id =
- if Stateid.equal id Stateid.initial ||
- Stateid.equal id Stateid.dummy then acc else
- let view = VCS.visit id in
- match view.step with
- | `Fork((_,_,_,ns), _) when test ns -> acc
- | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
- | `Sideff (ReplayCommand x,_) ->
- find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
- | `Sideff (CherryPickEnv, id) -> find acc id
- | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
- find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
- | `Cmd _ -> find acc view.next
- | `Alias (id,_) -> find acc id
- | `Fork _ -> find acc view.next
- in
- find [] (VCS.get_branch_pos branch)
-
-let warn_show_script_deprecated =
- CWarnings.create ~name:"deprecated-show-script" ~category:"deprecated"
- (fun () -> Pp.str "The “Show Script” command is deprecated.")
-
-let show_script ?proof () =
- warn_show_script_deprecated ();
- try
- let prf =
- try match proof with
- | None -> Some (PG_compat.get_current_proof_name ())
- | Some (p,_) -> Some (p.Proof_global.id)
- with PG_compat.NoCurrentProof -> None
- in
- let cmds = get_script prf in
- let _,_,_,indented_cmds =
- List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
- in
- let indented_cmds = List.rev (indented_cmds) in
- msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
- with Vcs_aux.Expired -> ()
-
-end
-
(* Wrapper for Vernacentries.interp to set the feedback id *)
(* It is currently called 19 times, this number should be certainly
reduced... *)
@@ -1172,21 +1079,17 @@ let stm_vernac_interp ?proof ?route id st { verbose; expr } : Vernacstate.t =
| VernacAbortAll | VernacAbort _ -> true
| _ -> false
in
- let aux_interp st expr =
- (* XXX unsupported attributes *)
- let cmd = Vernacprop.under_control expr in
- if is_filtered_command cmd then
- (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
- else
- match cmd with
- | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *)
- | _ ->
- stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
- try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr
- with e ->
- let e = CErrors.push e in
- Exninfo.iraise Hooks.(call_process_error_once e)
- in aux_interp st expr
+ (* XXX unsupported attributes *)
+ let cmd = Vernacprop.under_control expr in
+ if is_filtered_command cmd then
+ (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
+ else begin
+ stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
+ try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr
+ with e ->
+ let e = CErrors.push e in
+ Exninfo.iraise Hooks.(call_process_error_once e)
+ end
(****************************** CRUFT *****************************************)
(******************************************************************************)
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index ecc7d3ff88..ea35ea782d 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -88,7 +88,6 @@ GRAMMAR EXTEND Gram
| IDENT "Show" -> { VernacShow (ShowGoal OpenSubgoals) }
| IDENT "Show"; n = natural -> { VernacShow (ShowGoal (NthGoal n)) }
| IDENT "Show"; id = ident -> { VernacShow (ShowGoal (GoalId id)) }
- | IDENT "Show"; IDENT "Script" -> { VernacShow ShowScript }
| IDENT "Show"; IDENT "Existentials" -> { VernacShow ShowExistentials }
| IDENT "Show"; IDENT "Universes" -> { VernacShow ShowUniverses }
| IDENT "Show"; IDENT "Conjectures" -> { VernacShow ShowProofNames }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e307c0c268..535a0fa02c 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -628,7 +628,6 @@ open Pputils
let pr_showable = function
| ShowGoal n -> keyword "Show" ++ pr_goal_reference n
| ShowProof -> keyword "Show Proof"
- | ShowScript -> keyword "Show Script"
| ShowExistentials -> keyword "Show Existentials"
| ShowUniverses -> keyword "Show Universes"
| ShowProofNames -> keyword "Show Conjectures"
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 22427621e6..337cb233a2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2169,7 +2169,6 @@ let vernac_show ~pstate =
begin function
| ShowProof -> show_proof ~pstate
| ShowMatch id -> show_match id
- | ShowScript -> assert false (* Only the stm knows the script *)
| _ ->
user_err (str "This command requires an open proof.")
end
@@ -2190,7 +2189,6 @@ let vernac_show ~pstate =
| ShowIntros all -> show_intro ~pstate all
| ShowProof -> show_proof ~pstate:(Some pstate)
| ShowMatch id -> show_match id
- | ShowScript -> assert false (* Only the stm knows the script *)
end
let vernac_check_guard ~pstate =
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index df1d08ad0f..b8946fad23 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -81,7 +81,6 @@ type locatable =
type showable =
| ShowGoal of goal_reference
| ShowProof
- | ShowScript
| ShowExistentials
| ShowUniverses
| ShowProofNames
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:14:22 +0000