diff options
| author | Hugo Herbelin | 2020-09-04 19:04:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 23:19:32 +0200 |
| commit | 4c090da84c1cf2c4e37b9ddd5b2321c474f19e60 (patch) | |
| tree | 5076c75a07712b3120b6e3831681fb56b382b990 /interp/notation.ml | |
| parent | 5ef7598009bf49feafd632c0171a1bb14bef6448 (diff) | |
New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 04856a30f2..d57c4f3abf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1986,7 +1986,7 @@ let pr_scope_classes sc = spc() ++ prlist_with_sep spc pr_scope_class l) let pr_notation_info prglob ntn c = - str "\"" ++ str ntn ++ str "\" := " ++ + str "\"" ++ str ntn ++ str "\" :=" ++ brk (1,2) ++ prglob (Notation_ops.glob_constr_of_notation_constr c) let pr_notation_status on_parsing on_printing = @@ -2007,7 +2007,7 @@ let pr_non_empty spc pp = if pp = mt () then mt () else spc ++ pp let pr_notation_data prglob (on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) }) = - hov 0 (pr_notation_info prglob df r ++ pr_non_empty (spc ()) (pr_notation_status on_parsing on_printing)) + hov 0 (pr_notation_info prglob df r ++ pr_non_empty (brk(1,2)) (pr_notation_status on_parsing on_printing)) let extract_notation_data (main,extra) = let main = match main with @@ -2174,18 +2174,18 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - str "Notation" ++ fnl () ++ prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in prlist_with_sep fnl (fun (sc,(on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) })) -> hov 0 ( + str "Notation" ++ brk (1,2) ++ pr_notation_info prglob df r ++ (if String.equal sc default_scope then mt () - else (spc () ++ str ": " ++ str sc)) ++ + else (brk (1,2) ++ str ": " ++ str sc)) ++ (if Option.equal String.equal (Some sc) scope - then spc () ++ str "(default interpretation)" else mt ()) ++ - pr_non_empty (spc ()) (pr_notation_status on_parsing on_printing))) + then brk (1,2) ++ str "(default interpretation)" else mt ()) ++ + pr_non_empty (brk (1,2)) (pr_notation_status on_parsing on_printing))) l) ntns let collect_notation_in_scope scope sc known = |