Now printing body of abbreviations (i.e. notation with a name) with

full usage of notations instead of the previous cheap way to prevent
circularity in printing by deactivating all notations.

(Since "->" became a notation, printing abbreviations without
notations at all had become even more inconvenient).

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

5 files changed, 32 insertions, 8 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 84baefe61..7ba861704 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -61,9 +61,12 @@ let print_coercions = ref false
 (* This forces printing universe names of Type{.} *)
 let print_universes = Detyping.print_universes
 
-(* This suppresses printing of primitive tokens (e.g. numeral) and symbols *)
+(* This suppresses printing of primitive tokens (e.g. numeral) and notations *)
 let print_no_symbol = ref false
 
+(* This tells which notations still not to used if print_no_symbol is true *)
+let print_non_active_notations = ref ([] : interp_rule list)
+
 (* This governs printing of projections using the dot notation symbols *)
 let print_projections = ref false
 
@@ -73,8 +76,10 @@ let with_arguments f = Flags.with_option print_arguments f
 let with_implicits f = Flags.with_option print_implicits f
 let with_coercions f = Flags.with_option print_coercions f
 let with_universes f = Flags.with_option print_universes f
-let without_symbols f = Flags.with_option print_no_symbol f
 let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
+let without_symbols f = Flags.with_option print_no_symbol f
+let without_specific_symbols l f =
+  Flags.with_extra_values print_non_active_notations l f
 
 (**********************************************************************)
 (* Control printing of records *)
@@ -374,6 +379,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
+      if List.mem keyrule !print_non_active_notations then raise No_match;
       match t with
 	| PatCstr (loc,cstr,_,na) ->
 	  let p = apply_notation_to_pattern loc (ConstructRef cstr)
@@ -388,6 +394,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
+      if List.mem keyrule !print_non_active_notations then raise No_match;
       apply_notation_to_pattern Loc.ghost (IndRef ind)
 	(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
     with
@@ -802,6 +809,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | (keyrule,pat,n as _rule)::rules ->
       let loc = Glob_ops.loc_of_glob_constr t in
       try
+        if List.mem keyrule !print_non_active_notations then raise No_match;
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args,argsscopes,argsimpls) = match t,n with
 	  | GApp (_,f,args), Some n
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index de4b13b06..a98182fb8 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -72,8 +72,11 @@ val with_coercions : ('a -> 'b) -> 'a -> 'b
 (** This forces printing universe names of Type\{.\} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
 
-(** This suppresses printing of numeral and symbols *)
+(** This suppresses printing of primitive tokens and notations *)
 val without_symbols : ('a -> 'b) -> 'a -> 'b
 
+(** This suppresses printing of specific notations only *)
+val without_specific_symbols : interp_rule list -> ('a -> 'b) -> 'a -> 'b
+
 (** This prints metas as anonymous holes *)
 val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
diff --git a/lib/flags.ml b/lib/flags.ml
index d931ad987..d8355e3e1 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -8,14 +8,22 @@
 
 let with_option o f x =
   let old = !o in o:=true;
+   try let r = f x in o := old; r
+   with reraise ->
+     let reraise = Backtrace.add_backtrace reraise in
+     let () = o := old in
+     raise reraise
+
+let without_option o f x =
+  let old = !o in o:=false;
   try let r = f x in o := old; r
   with reraise ->
     let reraise = Backtrace.add_backtrace reraise in
     let () = o := old in
     raise reraise
 
-let without_option o f x =
-  let old = !o in o:=false;
+let with_extra_values o l f x =
+  let old = !o in o:=old@l;
   try let r = f x in o := old; r
   with reraise ->
     let reraise = Backtrace.add_backtrace reraise in
diff --git a/lib/flags.mli b/lib/flags.mli
index 8ff9deeaa..3965713fe 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -60,13 +60,16 @@ val is_program_mode : unit -> bool
 val make_warn : bool -> unit
 val if_warn : ('a -> unit) -> 'a -> unit
 
-(** Temporary activate an option (to activate option [o] on [f x y z],
+(** Temporarily activate an option (to activate option [o] on [f x y z],
    use [with_option o (f x y) z]) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
-(** Temporary deactivate an option *)
+(** Temporarily deactivate an option *)
 val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
+(** Temporarily extends the reference to a list *)
+val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
+
 (** If [None], no limit *)
 val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ee6a5e18d..bc9137ede 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -439,7 +439,9 @@ let gallina_print_syntactic_def kn =
        (str "Notation " ++ pr_qualid qid ++
         prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++
         spc () ++ str ":=") ++
-     spc () ++ Constrextern.without_symbols pr_glob_constr c)
+     spc () ++
+     Constrextern.without_specific_symbols
+       [Notation.SynDefRule kn] pr_glob_constr c)
 
 let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "