diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 15 | ||||
| -rw-r--r-- | printing/prettyp.ml | 7 | ||||
| -rw-r--r-- | printing/printer.ml | 10 |
3 files changed, 22 insertions, 10 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2ba972b5dc..eae6d09d69 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -389,7 +389,6 @@ let pr_priority = function (* Pretty printer for vernac commands *) (**************************************) let make_pr_vernac pr_constr pr_lconstr = - let pr_constrarg c = spc () ++ pr_constr c in let pr_lconstrarg c = spc () ++ pr_lconstr c in let pr_intarg n = spc () ++ int n in @@ -477,6 +476,13 @@ let rec pr_vernac = function | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v + (* Stm *) + | VernacStm JoinDocument -> str"Stm JoinDocument" + | VernacStm Finish -> str"Stm Finish" + | VernacStm (Observe id) -> + str"Stm Observe " ++ str(Stateid.string_of_state_id id) + | VernacStm (Command v) -> str"Stm Command " ++ pr_vernac v + (* Proof management *) | VernacAbortAll -> str "Abort All" | VernacRestart -> str"Restart" @@ -614,7 +620,7 @@ let rec pr_vernac = function let n = List.length (List.flatten (List.map fst (List.map snd l))) in hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ - pr_ne_params_list pr_lconstr_expr l) + pr_ne_params_list pr_lconstr_expr l) | VernacInductive (f,i,l) -> let pr_constructor (coe,(id,c)) = @@ -975,3 +981,8 @@ in pr_vernac let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end v + +let pr_vernac x = + try pr_vernac x + with e -> Errors.print e + diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9a084adc48..0f6a5e8937 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -420,11 +420,11 @@ let print_constant with_values sep sp = str"*** [ " ++ print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_univ_cstr cb.const_constraints + Printer.pr_univ_cstr (Future.force cb.const_constraints) | _ -> print_basename sp ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ - Printer.pr_univ_cstr cb.const_constraints) + Printer.pr_univ_cstr (Future.force cb.const_constraints)) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ @@ -566,7 +566,8 @@ let print_full_pure_context () = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Lazyconstr.force_opaque lc) + str "Proof " ++ pr_lconstr + (Lazyconstr.force_opaque (Future.force lc)) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ diff --git a/printing/printer.ml b/printing/printer.ml index 696f25695b..cc9356cda7 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -387,7 +387,7 @@ let default_pr_subgoal n sigma = | [] -> error "No such goal." | g::rest -> if Int.equal p 1 then - let pg = default_pr_goal { sigma=sigma ; it=g } in + let pg = default_pr_goal { sigma=sigma ; it=g; eff=Declareops.no_seff } in v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ str " is:" ++ cut () ++ pg) else @@ -438,7 +438,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = in let print_multiple_goals g l = if pr_first then - default_pr_goal { it = g ; sigma = sigma } ++ + default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } ++ pr_rec 2 l else pr_rec 1 (g::l) @@ -463,13 +463,13 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals = str "You can use Grab Existential Variables.") end | [g],[] when not !Flags.print_emacs -> - let pg = default_pr_goal { it = g ; sigma = sigma } in + let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in v 0 ( str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg ++ emacs_print_dependent_evars sigma seeds ) | [g],a::l when not !Flags.print_emacs -> - let pg = default_pr_goal { it = g ; sigma = sigma } in + let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in v 0 ( str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg ++ emacs_print_dependent_evars sigma seeds @@ -555,7 +555,7 @@ let pr_goal_by_id id = ++ pr_goal gs) in try - Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma}) + Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;eff=Declareops.no_seff}) with Not_found -> error "Invalid goal identifier." (* Elementary tactics *) |