diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-02-20 16:01:29 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-02-20 16:01:29 +0100 |
commit | 2b4f249ed0a28cde876f18aacf19f646d8af8fae (patch) | |
tree | 785019647a01b9eaa0e662e08422df294ebb8dca /interp/notation.ml | |
parent | 278cebe6835512a5646eafcb13e1f020c0dc5d91 (diff) | |
parent | 9907e296e21fdd9dc3fab2b84fe7159b35af654c (diff) |
Merge PR#189: Remove tabulation support from pretty-printing.
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 948d624a2..66d3c9185 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -927,19 +927,19 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - t (str "Notation " ++ - tab () ++ str "Scope " ++ tab () ++ fnl () ++ + str "Notation" ++ fnl () ++ prlist (fun (ntn,l) -> let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> hov 0 ( - pr_notation_info prglob df r ++ tbrk (1,2) ++ - (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++ - tbrk (1,2) ++ - (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ()) + pr_notation_info prglob df r ++ + (if String.equal sc default_scope then mt () + else (spc () ++ str ": " ++ str sc)) ++ + (if Option.equal String.equal (Some sc) scope + then spc () ++ str "(default interpretation)" else mt ()) ++ fnl ())) - l) ntns) + l) ntns let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); |