aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-06-02 16:11:03 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-06-02 16:13:30 +0200
commit9907e296e21fdd9dc3fab2b84fe7159b35af654c (patch)
treefc57dc4b3c6827655d3ce691248411838ace628b /interp/notation.ml
parent2d2d86c165cac7b051da1c5079d614a76550a20c (diff)
Remove tabulation support from pretty-printing.
This mechanism relied on functions that are deprecated in recent versions of ocaml. It was incorrectly used for the most part anyway. The only place that was using tabulations correctly is "print_loadpath", so there is a minor regression there: physical paths of short logical paths are no longer aligned.
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml14
1 files changed, 7 insertions, 7 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index b19fd9e1f..3a078143b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -898,19 +898,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));