From 6a5dcbbfea1af0308a4d49e7c5bcea26d74a739d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 31 May 2019 13:09:23 +0200 Subject: Remove Show Script (deprecated in 8.10) --- dev/v8-syntax/syntax-v8.tex | 1 - .../10277-no-show-script.rst | 2 + doc/sphinx/proof-engine/proof-handling.rst | 13 --- ide/coq_commands.ml | 2 - plugins/funind/recdef.ml | 2 - stm/stm.ml | 119 ++------------------- vernac/g_proofs.mlg | 1 - vernac/ppvernac.ml | 1 - vernac/vernacentries.ml | 2 - vernac/vernacexpr.ml | 1 - 10 files changed, 13 insertions(+), 131 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/10277-no-show-script.rst 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 `_, 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 - - ````. - - .. 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 -- cgit v1.2.3