X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2FdisambiguateTypes.mli;fp=matitaB%2Fcomponents%2Fdisambiguation%2FdisambiguateTypes.mli;h=0f557b1ea671a239e1e054b271bd958342f28e76;hb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;hp=5ebc835cb4ac3ca9602ae7db3cfab7070a538aa0;hpb=98f0fac6d03367be776303e7ba353b75878aaa40;p=helm.git diff --git a/matitaB/components/disambiguation/disambiguateTypes.mli b/matitaB/components/disambiguation/disambiguateTypes.mli index 5ebc835cb..0f557b1ea 100644 --- a/matitaB/components/disambiguation/disambiguateTypes.mli +++ b/matitaB/components/disambiguation/disambiguateTypes.mli @@ -22,11 +22,16 @@ * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) - +(* type domain_item = | Id of (string * string option) (* literal, opt. uri *) | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *) | Num of (string option * string) option (* opt. uri, interpretation *) + *) +type domain_item = + | Id of string (* literal *) + | Symbol of string (* literal *) + | Num (* module Domain: Set.S with type elt = domain_item *) module Environment: @@ -35,7 +40,12 @@ sig val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t end - (** to be raised when a choice is invalid due to some given parameter (e.g. +module InterprEnv: +sig + include Map.S with type key = Stdpp.location +end + +(** to be raised when a choice is invalid due to some given parameter (e.g. * wrong number of Cic.term arguments received) *) exception Invalid_choice of (Stdpp.location * string) Lazy.t @@ -54,6 +64,8 @@ type interactive_user_uri_choice_type = type interactive_interpretation_choice_type = string -> int -> (Stdpp.location list * string * string) list list -> int list +type interactive_ast_choice_type = string list -> int + type input_or_locate_uri_type = title:string -> ?id:string -> unit -> NReference.reference option