diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-05-31 12:16:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-02 16:45:39 +0200 |
| commit | e020cc70578b65609ac7337537f16a1c25254e77 (patch) | |
| tree | 3c69737afc2e5693d5ca65b14e169ac406adc187 /stm/stm.mli | |
| parent | 2d2d86c165cac7b051da1c5079d614a76550a20c (diff) | |
Move serialization functions out of Stm
Serialization should be specific to each particular backend, so we let
the Stm clients choose how the send the nodes.
This should be quite safe to pull in. Test suite passes.
Related to #180
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 6519a6254..6ffe0beb4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -76,7 +76,9 @@ val get_current_state : unit -> Stateid.t (* Misc *) val init : unit -> unit -val print_ast : Stateid.t -> Xml_datatype.xml + +(* This returns the node at that position *) +val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option (* Filename *) val set_compilation_hints : string -> unit |