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/sphinx/proof-engine/proof-handling.rst13
-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
10 files changed, 13 insertions, 131 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/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 3f966755ca..ca7f037815 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
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-01-31 12:06:24 +0000