From 952e9aea47d3fad2d0f488d968ff0e90fa403ebc Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 3 May 2017 11:37:08 +0200
Subject: Adding an even more compact mode for goal display.

We want to print variables in vertical boxes as much as possible.

The criterion to distinguish "variable" from "hypothesis" is not
obvious. We chose this one but may change it in the future:

X:T is a variable if T is not of type Prop AND T is "simple" which
means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall
Ti:Type, but not Ti:nat).
---
 printing/printer.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 504392e35f..9c9f6e766a 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -111,6 +111,9 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 
 
 (** Contexts *)
+(** Display compact contexts of goals (simple hyps on the same line) *)
+val set_compact_context : bool -> unit
+val get_compact_context : unit -> bool
 
 val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
@@ -132,7 +135,7 @@ val pr_cpred               : Cpred.t -> std_ppcmds
 val pr_idpred              : Id.Pred.t -> std_ppcmds
 val pr_transparent_state   : transparent_state -> std_ppcmds
 
-(** Proofs *)
+(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
 val pr_goal                : goal sigma -> std_ppcmds
 val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
-- 
cgit v1.2.3


From 1fe73e6af81759fa8b78c8660745492ed886d477 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 26 Apr 2017 11:57:58 +0200
Subject: Adding an option "Printing Unfocused".

Off by default.

+ small refactoring of emacs hacks in printer.ml.
---
 printing/printer.mli | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 504392e35f..c282950545 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -18,6 +18,11 @@ open Glob_term
 
 (** These are the entry points for printing terms, context, tac, ... *)
 
+
+val enable_unfocused_goal_printing: bool ref
+val enable_goal_tags_printing      : bool ref
+val enable_goal_names_printing     : bool ref
+
 (** Terms *)
 
 val pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
@@ -135,7 +140,19 @@ val pr_transparent_state   : transparent_state -> std_ppcmds
 (** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
+
+(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
+   prints the goals of the list [goals] followed by the goals in
+   [unfocused], in a short way (typically only the conclusion) except
+   for the first goal if [pr_first] is true. This function can be
+   replaced by another one by calling [set_printer_pr] (see below),
+   typically by plugin writers. The default printer prints only the
+   focused goals unless the conrresponding option
+   [enable_unfocused_goal_printing] is set. [seeds] is for printing
+   dependent evars (mainly for emacs proof tree mode). *)
+val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list
+                             -> goal list -> goal list -> std_ppcmds
+
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -190,7 +207,7 @@ val pr_goal_by_id : Id.t -> std_ppcmds
 val pr_goal_by_uid : string -> std_ppcmds
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;
-- 
cgit v1.2.3