* http://helm.cs.unibo.it/
*)
+open MatitaTypes
+
class parserr () =
object
method parseTerm = CicTextualParser2.parse_term
~nonvars_button:enable_button_for_non_vars uris
let interactive_interpretation_choice = chooseInterp
- let input_or_locate_uri ~(title:string) =
- (* TODO Zack: I try to avoid using this callback. I therefore assume
- * that the presence of an identifier that can't be resolved via
- * "locate" query is a syntax error *)
- MatitaTypes.not_implemented
- "MatitaDisambiguator: input_or_locate_uri callback"
+ let input_or_locate_uri ~(title:string) ?id =
+ (* Zack: I try to avoid using this callback. I therefore assume that
+ * the presence of an identifier that can't be resolved via "locate"
+ * query is a syntax error *)
+ let msg = match id with Some id -> id | _ -> "" in
+ raise (Unbound_identifier msg)
end
in
let module Disambiguator = Disambiguate.Make (Callbacks) in