diff options
| author | Regis-Gianas | 2014-11-04 14:50:06 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:36 +0100 |
| commit | 678b17b52b0b59a5470d8272474e692b2fe023e3 (patch) | |
| tree | 9cae63a5e14dea376ce82c16643aeb110c95eddb /printing | |
| parent | db9b17d55f539fcfda799a9fe15caa2530cc727f (diff) | |
lib/Pp.tag: New.
A combinator to introduce tags.
printing/{Ppconstr, Ppvernac}: Use it.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 12 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 9 |
2 files changed, 5 insertions, 16 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index ad95d99693..2039fdaa44 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -818,15 +818,9 @@ end) = struct include Make (struct open Ppannotation - - let tag_keyword t = - Pp.open_tag (Indexer.index AKeyword) ++ t ++ Pp.close_tag () - - let tag_unparsing unp t = - Pp.open_tag (Indexer.index (AUnparsing unp)) ++ t ++ Pp.close_tag () - - let tag_constr_expr e t = - Pp.open_tag (Indexer.index (AConstrExpr e)) ++ t ++ Pp.close_tag () + let tag_keyword = Pp.tag (Indexer.index AKeyword) + let tag_unparsing unp = Pp.tag (Indexer.index (AUnparsing unp)) + let tag_constr_expr e = Pp.tag (Indexer.index (AConstrExpr e)) end) end diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index dafbc3d820..7420f2784e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1276,13 +1276,8 @@ end) = struct include Make (Ppconstr.RichPp (Indexer)) (struct open Ppannotation - - let tag_keyword t = - Pp.open_tag (Indexer.index AKeyword) ++ t ++ Pp.close_tag () - - let tag_vernac v t = - Pp.open_tag (Indexer.index (AVernac v)) ++ t ++ Pp.close_tag () - + let tag_keyword = Pp.tag (Indexer.index AKeyword) + let tag_vernac v = Pp.tag (Indexer.index (AVernac v)) end) end |