fixed indentation of subgoals for Show Script

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

3 files changed, 40 insertions, 50 deletions

diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index d42aaf1f37..d50e520f99 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -90,7 +90,8 @@ let pr_change gl =
   str"change " ++
   pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"."
 
-let rec print_decl_script tac_printer nochange sigma pf =
+let print_decl_script tac_printer ?(nochange=true) sigma pf =
+  let rec print_prf pf =
   match pf.ref with
     | None ->
 	(if nochange then 
@@ -99,46 +100,38 @@ let rec print_decl_script tac_printer nochange sigma pf =
 	   pr_change pf.goal)
 	++ fnl ()
     | Some (Daimon,[]) -> str "(* Some proof has been skipped here *)"
-    | Some (Prim Change_evars,[subpf]) ->   
-	print_decl_script tac_printer nochange sigma subpf
+    | Some (Prim Change_evars,[subpf]) -> print_prf subpf
     | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) ->
 	begin
 	  match instr.instr,subprfs with
 	    Pescape,[{ref=Some(_,subsubprfs)}] ->
 	      hov 7
 		(pr_rule_dot_fnl rule ++
-		   prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
-		if opened then mt () else str "return."
+		  prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++
+	      if opened then mt () else str "return."
 	  | Pclaim _,[body;cont] ->
-	      hov 2
-		(pr_rule_dot_fnl rule ++
-		   print_decl_script tac_printer nochange sigma body) ++ 
-		fnl () ++
-		if opened then mt () else str "end claim." ++ fnl () ++
-		  print_decl_script tac_printer nochange sigma cont
+	      hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++
+	      (if opened then mt () else str "end claim." ++ fnl ()) ++
+	      print_prf cont
 	  | Pfocus _,[body;cont] ->
-	      hov 2 
-		(pr_rule_dot_fnl rule ++
-		   print_decl_script tac_printer nochange sigma body) ++ 
-		fnl () ++
-		if opened then mt () else str "end focus." ++ fnl () ++
-		  print_decl_script tac_printer nochange sigma cont
+	      hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ 
+	      fnl () ++
+	      (if opened then mt () else str "end focus." ++ fnl ()) ++
+	      print_prf cont
 	  | (Psuppose _ |Pcase (_,_,_)),[body;cont] ->
-	      hov 2 
-		(pr_rule_dot_fnl rule ++
-		   print_decl_script tac_printer nochange sigma body) ++ 
-		fnl () ++
-		print_decl_script tac_printer nochange sigma cont 
+	      hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++
+	      print_prf cont 
 	  | _,[next] ->
-	      pr_rule_dot_fnl rule ++
-		print_decl_script tac_printer nochange sigma next
+	      pr_rule_dot_fnl rule ++ print_prf next
 	  | _,[] ->
 	      pr_rule_dot rule		
 	  | _,_ -> anomaly "unknown branching instruction"
 	end
-    | _ -> anomaly "Not Applicable"
+    | _ -> anomaly "Not Applicable" in
+  print_prf pf
 
-let rec print_script nochange sigma pf =
+let print_script ?(nochange=true) sigma pf =
+  let rec print_prf pf =
   match pf.ref with
     | None ->
         (if nochange then 
@@ -153,26 +146,25 @@ let rec print_script nochange sigma pf =
 	end ++
 	  begin
 	    hov 0 (str "proof." ++ fnl () ++ 
-		     print_decl_script (print_script nochange sigma) 
-		     nochange sigma (List.hd script))
+		     print_decl_script print_prf 
+		     ~nochange sigma (List.hd script))
 	  end ++ fnl () ++
 	  begin
 	    if opened then mt () else (str "end proof." ++ fnl ())
 	  end
     | Some(Daimon,spfl) ->
 	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
-	   prlist_with_sep pr_fnl
-           (print_script nochange sigma) spfl )
+	   prlist_with_sep pr_fnl print_prf spfl )
     | Some(rule,spfl) ->
 	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
 	   pr_rule_dot_fnl rule ++
-	   prlist_with_sep pr_fnl
-           (print_script nochange sigma) spfl )	
+	   prlist_with_sep pr_fnl print_prf spfl ) in
+  print_prf pf
 
 (* printed by Show Script command *)
 
-let print_treescript nochange sigma pf =
-  let rec aux pf =
+let print_treescript ?(nochange=true) sigma pf =
+  let rec print_prf pf =
     match pf.ref with
     | None ->
         if nochange then 
@@ -184,23 +176,21 @@ let print_treescript nochange sigma pf =
 	begin
 	  if nochange then mt () else pr_change pf.goal ++ fnl ()
 	end ++
-	  hov 0 
+	hov 0 
 	  begin str "proof." ++ fnl () ++
-	    print_decl_script aux
-	    nochange sigma (List.hd script) 
+	    print_decl_script print_prf ~nochange sigma (List.hd script) 
 	  end ++ fnl () ++ 
-	  begin
-	    if opened then mt () else (str "end proof." ++ fnl ())
-	  end
+	begin
+	  if opened then mt () else (str "end proof." ++ fnl ())
+	end
     | Some(Daimon,spfl) ->
-	((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
-	   prlist_with_sep pr_fnl
-           (print_script nochange sigma) spfl )
+	(if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
+	prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl
     | Some(r,spfl) ->
         let indent = if List.length spfl >= 2 then 1 else 0 in
-        (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
-        hv indent (pr_rule_dot_fnl r ++ prlist_with_sep mt aux spfl)
-  in hov 0 (aux pf)
+        (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
+        hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl)
+  in hov 0 (print_prf pf)
 
 let rec print_info_script sigma osign pf =
   let {evar_hyps=sign; evar_concl=cl} = pf.goal in
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index 842b852959..d46f19c64c 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -23,6 +23,6 @@ val pr_rule     : rule -> std_ppcmds
 val pr_tactic   : tactic_expr -> std_ppcmds
 val pr_proof_instr : Decl_expr.proof_instr -> Pp.std_ppcmds
 val print_script :
-  bool -> evar_map -> proof_tree -> std_ppcmds
+  ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds
 val print_treescript :
-  bool -> evar_map -> proof_tree -> std_ppcmds
+  ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d761472c9b..981e82b93b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -95,7 +95,7 @@ let show_script () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  msgnl_with !Pp_control.deep_ft (print_treescript true evc pf)
+  msgnl_with !Pp_control.deep_ft (print_treescript evc pf)
 
 let show_thesis () =
      msgnl (anomaly "TODO" )
@@ -1206,7 +1206,7 @@ let apply_subproof f occ =
   f evc (Global.named_context()) pf
 
 let explain_proof occ =
-  msg (apply_subproof (fun evd _ -> print_treescript true evd) occ)
+  msg (apply_subproof (fun evd _ -> print_treescript evd) occ)
 
 let explain_tree occ =
   msg (apply_subproof print_proof occ)