Restore an indentation of Show Script

 Based on a patch contributed by D. de Rauglaudre on coq-dev.
 I've added some specific treatment of { } and bullets - + *.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15546 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 65 insertions, 4 deletions

diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index 24a056d738..d0f258fbf8 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -33,6 +33,7 @@ type info = {
   nproofs : int;
   prfname : identifier option;
   prfdepth : int;
+  ngoals : int;
   cmd : vernac_expr;
   mutable reachable : bool;
 }
@@ -74,6 +75,14 @@ let search test =
   with Found i ->
     while i != Stack.top history do pop () done
 
+(** An auxiliary function to retrieve the number of remaining subgoals *)
+
+let get_ngoals () =
+  try
+    let prf = Proof_global.give_me_the_proof () in
+    List.length (Evd.sig_it (Proof.V82.background_subgoals prf))
+  with Proof_global.NoCurrentProof -> 0
+
 (** Register the end of a command and store the current state *)
 
 let mark_command ast =
@@ -85,6 +94,7 @@ let mark_command ast =
       prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None);
       prfdepth = max 0 (Pfedit.current_proof_depth ());
       reachable = true;
+      ngoals = get_ngoals ();
       cmd = ast }
     history
 
@@ -175,6 +185,7 @@ let reset_initial () =
 	nproofs = 0;
 	prfname = None;
 	prfdepth = 0;
+	ngoals = 0;
 	reachable = true;
 	cmd = VernacNop }
       history
@@ -215,10 +226,10 @@ let get_script prf =
     | _ -> ()
   in
   (try Stack.iter select history with Not_found -> ());
-  (* Get rid of intermediate commands which don't grow the depth *)
+  (* Get rid of intermediate commands which don't grow the proof depth *)
   let rec filter n = function
     | [] -> []
-    | {prfdepth=d; cmd=c}::l when n < d -> c :: filter d l
+    | {prfdepth=d; cmd=c; ngoals=ng}::l when n < d -> (c,ng) :: filter d l
     | {prfdepth=d}::l -> filter d l
   in
   (* initial proof depth (after entering the lemma statement) is 1 *)
diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
index bfd3c47a06..0b9325bd61 100644
--- a/toplevel/backtrack.mli
+++ b/toplevel/backtrack.mli
@@ -76,7 +76,7 @@ val mark_unreachable : ?after:int -> Names.identifier list -> unit
 
 (** Parse the history stack for printing the script of a proof *)
 
-val get_script : Names.identifier -> Vernacexpr.vernac_expr list
+val get_script : Names.identifier -> (Vernacexpr.vernac_expr * int) list
 
 
 (** For debug purpose, a dump of the history *)
@@ -86,6 +86,7 @@ type info = {
   nproofs : int;
   prfname : Names.identifier option;
   prfdepth : int;
+  ngoals : int;
   cmd : Vernacexpr.vernac_expr;
   mutable reachable : bool;
 }
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index defa6e1935..ebe1e4fbed 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -61,10 +61,59 @@ let show_node () =
       could, possibly, be cleaned away. (Feb. 2010) *)
   ()
 
+(* indentation code for Show Script, initially contributed
+   by D. de Rauglaudre *)
+
+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 _ = assert (ng = ngprev - 1) in
+      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 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 =
+    (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 show_script () =
   let prf = Pfedit.get_current_proof_name () in
   let cmds = Backtrack.get_script prf in
-  msg_notice (Pp.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds)
+  let _,_,_,indented_cmds =
+    List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
+  in
+  let indented_cmds = List.rev (indented_cmds) in
+  msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds))
 
 let show_thesis () =
      msg_error (anomaly "TODO" )