method parseTactical = CicTextualParser2.parse_tactical
end
-class disambiguator
- ~parserr ~dbd ~(chooseUris: MatitaTypes.choose_uris_callback)
- ~(chooseInterp: MatitaTypes.choose_interp_callback) ()
- =
+let parserr () = new parserr ()
+let parserr_instance = MatitaMisc.singleton parserr
+
+class disambiguator () =
+ let _chooseUris = ref mono_uris_callback in
+ let _chooseInterp = ref mono_interp_callback in
let disambiguate_term =
let module Callbacks =
struct
~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg
~id uris
=
- chooseUris ~selection_mode ~title ~msg
+ !_chooseUris ~selection_mode ~title ~msg
~nonvars_button:enable_button_for_non_vars uris
- let interactive_interpretation_choice = chooseInterp
+ let interactive_interpretation_choice interp = !_chooseInterp interp
+
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
+ let msg = match id with Some id -> id | _ -> "_" in
raise (Unbound_identifier msg)
end
in
Disambiguator.disambiguate_term
in
object (self)
- val mutable parserr: parserr = parserr
- method parserr = parserr
- method setParserr p = parserr <- p
-
val mutable _env = DisambiguateTypes.Environment.empty
method env = _env
method setEnv e = _env <- e
+ method chooseUris = !_chooseUris
+ method setChooseUris f = _chooseUris := f
+
+ method chooseInterp = !_chooseInterp
+ method setChooseInterp f = _chooseInterp := f
+
+ val parserr = parserr_instance ()
+ method parserr = parserr
+
+ val dbd = MatitaMisc.dbd_instance ()
+
method disambiguateTermAst ?(context = []) ?(metasenv = []) ?env termAst =
let (save_state, env) =
match env with
(parserr#parseTerm stream)
end
+let disambiguator () = new disambiguator ()
+let instance = MatitaMisc.singleton disambiguator
+