X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteTypes.mli;h=95e994350f95bc654f7719a0a67f90ad9ad2a3ec;hb=df7a2aa19e98dc28e7f22129275a175cead49e2d;hp=fd89f464880d3a3d85be4ea594ac5804d9fad8af;hpb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;p=helm.git diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index fd89f4648..95e994350 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -31,14 +31,17 @@ exception Command_error of string val command_error: string -> 'a (** @raise Command_error *) -class status : +class virtual status : string -> object ('self) (* Warning: #stack and #obj are meaningful iff #ng_mode is `ProofMode *) inherit NTacStatus.tac_status inherit NCicLibrary.dumpable_status inherit NCicLibrary.status + inherit NCicExtraction.status + inherit OcamlExtractionTable.status inherit GrafiteParser.status + inherit TermContentPres.status method baseuri: string method set_baseuri: string -> 'self method ng_mode: [`ProofMode | `CommandMode]