- 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"
- end
- in
- let module Disambiguator = Disambiguate.Make (Callbacks) in
- Disambiguator.disambiguate_term
- in
- object (self)
- val mutable parserr: parserr = parserr
- method parserr = parserr
- method setParserr p = parserr <- p
+let mono_uris_callback ~id = raise Ambiguous_input
+let mono_interp_callback _ = raise Ambiguous_input