print_in_case as a flag rather than a function

lib/parser/builtins.ml

@@ -511,10 +511,8 @@ let pp_abs cube space ppf obs ws =
 let () =
   set_processor abs (process_abs `Normal);
   set_processor cubeabs (process_abs `Cube);
-  set_print abs (pp_abs `Normal);
-  set_print cubeabs (pp_abs `Cube);
-  set_print_as_case abs (pp_abs `Normal);
-  set_print_as_case cubeabs (pp_abs `Cube)
+  set_print abs ~in_case:true (pp_abs `Normal);
+  set_print cubeabs ~in_case:true (pp_abs `Cube)
 
 (* ********************
    The universe
@@ -699,9 +697,7 @@ let pp_tuple space ppf obs ws =
       pp_ws space ppf wsrparen;
       pp_close_box ppf ()
 
-let () =
-  set_print parens pp_tuple;
-  set_print_as_case parens pp_tuple
+let () = set_print parens ~in_case:true pp_tuple
 
 (* ********************
    Comatches
@@ -1392,11 +1388,11 @@ and pp_match box space ppf obs ws =
 
 (* Matches and comatches are only valid in case trees. *)
 let () =
-  set_print_as_case implicit_mtch (pp_match true);
-  set_print_as_case explicit_mtch (pp_match true);
-  set_print_as_case mtchlam (pp_match true);
-  set_print_as_case comatch (pp_match true);
-  set_print_as_case empty_co_match (pp_match true)
+  set_print implicit_mtch ~in_case:true (pp_match true);
+  set_print explicit_mtch ~in_case:true (pp_match true);
+  set_print mtchlam ~in_case:true (pp_match true);
+  set_print comatch ~in_case:true (pp_match true);
+  set_print empty_co_match ~in_case:true (pp_match true)
 
 (* ********************
    Codatatypes
@@ -1490,7 +1486,7 @@ let pp_codata space ppf obs ws =
   pp_ws space ppf wsrbrack;
   pp_close_box ppf ()
 
-let () = set_print codata pp_codata
+let () = set_print codata ~in_case:true pp_codata
 
 (* ********************
    Record types
@@ -1649,7 +1645,7 @@ let pp_record space ppf obs ws =
   pp_ws space ppf wsrparen;
   pp_close_box ppf ()
 
-let () = set_print record pp_record
+let () = set_print record ~in_case:true pp_record
 
 (* ********************
    Datatypes
@@ -1784,7 +1780,7 @@ let pp_data space ppf obs ws =
   pp_ws space ppf wsrbrack;
   pp_close_box ppf ()
 
-let () = set_print data pp_data
+let () = set_print data ~in_case:true pp_data
 
 (* ********************
    Forwards Lists

lib/parser/notation.ml

@@ -167,9 +167,9 @@ and ('left, 'tight, 'right) notation = {
   (* The remaining fields are mutable because they have to be able to refer to the notation object itself, so we have a circular data structure.  They aren't expected to mutate further after being set once.  Thus we store them as options, to record whether they have been set. *)
   mutable tree : ('left, 'tight) notation_entry option;
   mutable processor : processor option;
-  (* Some notations only make sense in terms, others only make sense in case trees, and some make sense in either.  Thus, a notation can supply either or both of these printing functions. *)
   mutable print : printer option;
-  mutable print_as_case : printer option;
+  (* Whether this notation can appear in a case tree.  Otherwise, encountering it terminates the case tree in a leaf. *)
+  mutable print_in_case : bool;
 }
 
 module Notation = struct
@@ -264,9 +264,11 @@ let set_processor n c =
   | None -> n.processor <- Some c
 
 let print n = n.print
-let set_print n p = n.print <- Some p
-let print_as_case n = n.print_as_case
-let set_print_as_case n p = n.print_as_case <- Some p
+let print_in_case n = n.print_in_case
+
+let set_print n ?(in_case = false) p =
+  n.print <- Some p;
+  n.print_in_case <- in_case
 
 (* Create a new notation with specified name, fixity, and tightness.  Its mutable fields must be set later. *)
 let make :
@@ -285,8 +287,8 @@ let make :
     right;
     tree = None;
     print = None;
-    print_as_case = None;
     processor = None;
+    print_in_case = false;
   }
 
 let rec split_last_whitespace (ws : Whitespace.alist) : Whitespace.alist * Whitespace.t list =

lib/parser/notation.mli

@@ -139,9 +139,8 @@ val set_tree : ('left, 'tight, 'right) notation -> ('left, 'tight) notation_entr
 val processor : ('left, 'tight, 'right) notation -> processor
 val set_processor : ('left, 'tight, 'right) notation -> processor -> unit
 val print : ('left, 'tight, 'right) notation -> printer option
-val set_print : ('left, 'tight, 'right) notation -> printer -> unit
-val print_as_case : ('left, 'tight, 'right) notation -> printer option
-val set_print_as_case : ('left, 'tight, 'right) notation -> printer -> unit
+val print_in_case : ('left, 'tight, 'right) notation -> bool
+val set_print : ('left, 'tight, 'right) notation -> ?in_case:bool -> printer -> unit
 val make : string -> ('left, 'tight, 'right) fixity -> ('left, 'tight, 'right) notation
 val equal : ('l1, 't1, 'r1) notation -> ('l2, 't2, 'r2) notation -> bool
 

lib/parser/print.ml

@@ -121,12 +121,10 @@ let pp_ws (space : space) (ppf : formatter) (ws : Whitespace.t list) : unit =
 (* Print a parse tree. *)
 let rec pp_term (space : space) (ppf : formatter) (wtr : observation) : unit =
   let (Term tr) = wtr in
-  match state () with
-  | `Case -> (
-      match tr.value with
-      | Notn n -> pp_notn_case space ppf (notn n) (args n) (whitespace n)
-      | _ -> as_term @@ fun () -> pp_term space ppf wtr)
-  | `Term -> (
+  match tr.value with
+  | Notn n when print_in_case (notn n) -> pp_notn space ppf (notn n) (args n) (whitespace n)
+  | _ -> (
+      Printconfig.as_term @@ fun () ->
       match tr.value with
       | Notn n -> pp_notn space ppf (notn n) (args n) (whitespace n)
       | App _ ->
@@ -168,19 +166,6 @@ and pp_superscript ppf str =
       pp_utf_8 ppf str;
       pp_utf_8 ppf ")"
 
-and pp_notn_case :
-    type left tight right.
-    space ->
-    formatter ->
-    (left, tight, right) notation ->
-    observation list ->
-    Whitespace.alist ->
-    unit =
- fun space ppf n obs ws ->
-  match print_as_case n with
-  | Some pp -> pp space ppf obs ws
-  | None -> as_term @@ fun () -> pp_notn space ppf n obs ws
-
 and pp_notn :
     type left tight right.
     space ->