Eliminate duplicate get_text function
commit1715b901d88e552773c423aaaf0ea2e0ac83273b
authorTed Spence <tspence@fb.com>
Thu, 15 Aug 2019 19:44:33 +0000 (15 12:44 -0700)
committerHhvm Bot <hhvm-bot@users.noreply.github.com>
Thu, 15 Aug 2019 19:47:36 +0000 (15 12:47 -0700)
treea21ebf9c74edaa4001d17f5d9e65574992790cfd
parent5fed38a31a73f1217cba8bf4145eb7c7c80f05c7
Eliminate duplicate get_text function

Summary:
The functions `get_text` and `text` inside full_fidelity_source_text had the same definition.

Let's remove one of them.  Since most pieces of code use the function named "text", let's standardize on that.

Reviewed By: dabek

Differential Revision: D16832464

fbshipit-source-id: b6c34f0413be92c168ab9bf487b6b73a010540ec
hphp/hack/src/hackfmt/debug/hackfmt_debug.ml
hphp/hack/src/parser/full_fidelity_source_text.ml
hphp/hack/src/parser/full_fidelity_source_text.mli