let disambiguate_command lexicon_status_ref grafite_status cmd =
let baseuri = grafite_status#baseuri in
- let lexicon_status,metasenv,cmd =
+ let lexicon_status,cmd =
GrafiteDisambiguate.disambiguate_command ~baseuri
- !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd
+ !lexicon_status_ref cmd
in
lexicon_status_ref := lexicon_status;
- GrafiteTypes.set_metasenv metasenv grafite_status,cmd
+ grafite_status,cmd
let eval_macro_screenshot (status : GrafiteTypes.status) name =
+ assert false (* MATITA 1.0
let _,_,metasenv,subst,_ = status#obj in
let sequent = List.hd metasenv in
let mathml =
Filename.quote (name^".png")));
HLog.debug ("generated " ^ name ^ ".png");
status, `New []
+ *)
;;
let eval_ast ?do_heavy_checks status (text,prefix_len,ast) =
let lexicon_status_ref = ref (status :> LexiconEngine.status) in
let baseuri = status#baseuri in
let new_status,new_objs =
- match ast with
- | G.Executable (_, G.Command (_, G.Coercion _)) when dump ->
-(* FG: some commands can not be executed when mmas are parsed *************)
-(* To be removed when mmas will be executed *)
- status, `Old []
- | ast ->
GrafiteEngine.eval_ast
- ~disambiguate_tactic:((* MATITA 1.0*) fun _ -> assert false)
~disambiguate_command:(disambiguate_command lexicon_status_ref)
- ~disambiguate_macro:((* MATITA 1.0*) fun _ -> assert false)
?do_heavy_checks status (text,prefix_len,ast)
in
let new_status =
let v = LexiconAst.description_of_alias value in
let b =
try
- (* this hack really sucks! *)
- UriManager.buri_of_uri (UriManager.uri_of_string v) = baseuri
+ let NReference.Ref (uri,_) = NReference.reference_of_string v in
+ NUri.baseuri_of_uri uri = baseuri
with
- UriManager.IllFormedUri _ ->
- try
- (* this too! *)
- let NReference.Ref (uri,_) = NReference.reference_of_string v in
- let ouri = NCic2OCic.ouri_of_nuri uri in
- UriManager.buri_of_uri ouri = baseuri
- with
- NReference.IllFormedReference _ ->
- false (* v is a description, not a URI *)
+ NReference.IllFormedReference _ ->
+ false (* v is a description, not a URI *)
in
if b then
status,acc