]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/getter.mli
Requires and Provides now fixed
[helm.git] / helm / interface / getter.mli
1 (******************************************************************************)
2 (*                                                                            *)
3 (*                               PROJECT HELM                                 *)
4 (*                                                                            *)
5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
6 (*                                 24/01/2000                                 *)
7 (*                                                                            *)
8 (*                                                                            *)
9 (******************************************************************************)
10
11 (* get : uri -> filename *)
12 (* If uri is the URI of an annotation, the annotated object is processed *)
13 val get : UriManager.uri -> string
14
15 (* get_ann : uri -> filename *)
16 (* If uri is the URI of an annotation, the annotation file is processed *)
17 val get_ann : UriManager.uri -> string
18
19 (* get_ann_file_name_and_uri : uri -> filename * annuri *)
20 (* If given an URI, it returns the name of the corresponding *)
21 (* annotation file and the annotation uri                    *)
22 val get_ann_file_name_and_uri : UriManager.uri -> string * UriManager.uri
23
24 (* synchronize with the servers *)
25 val update : unit -> unit