- status,`New []
- | GrafiteAst.Print (_,_) -> status,`New []
- | GrafiteAst.Set (loc, name, value) -> status, `New []
+(* assert false (* MANCA SALVATAGGIO SU DISCO *) *)
+ status, [] (* capire [] XX *)
+ | GrafiteAst.Alias (loc, spec) ->
+ let diff =
+ (*CSC: Warning: this code should be factorized with the corresponding
+ code in DisambiguatePp *)
+ match spec with
+ | GrafiteAst.Ident_alias (id,uri) ->
+ [DisambiguateTypes.Id id,spec]
+ | GrafiteAst.Symbol_alias (symb, instance, desc) ->
+ [DisambiguateTypes.Symbol (symb,instance),spec]
+ | GrafiteAst.Number_alias (instance,desc) ->
+ [DisambiguateTypes.Num instance,spec]
+ in
+ let mode = assert false in (* VEDI SOPRA *)
+ LexiconEngine.set_proof_aliases status mode diff;
+ assert false (* MANCA SALVATAGGIO SU DISCO *)
+;;
+
+let eval_comment opts status (text,prefix_len,c) = status, []
+
+let rec eval_command opts status (text,prefix_len,cmd) =
+ let status,uris =
+ match cmd with
+ | GrafiteAst.Print (_,_) -> status,[]
+ | GrafiteAst.Set (loc, name, value) -> status, []