open GrafiteTypes
-exception AttemptToInsertAnAlias of #LexiconEngine.status
+exception AttemptToInsertAnAlias of LexiconEngine.status
let slash_n_RE = Pcre.regexp "\\n" ;;
(Helm_registry.get_bool "matita.paste_unicode_as_tex")
in
output_string och str
- | G.Executable (loc, G.Command (_, G.Include (_, false, _))) -> ()
+ | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
| stm ->
output_string och (pp_statement stm); nl (); nl ()
in
with
| [] -> grafite_status
| (g,None)::_ -> g
- | (g,Some _)::_ -> raise (AttemptToInsertAnAlias g)
+ | (g,Some _)::_ ->
+ raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
with MatitaEngine.EnrichedWithStatus
(GrafiteEngine.Macro (floc, f), grafite) as exn ->
match f (get_macro_context (Some grafite)) with
(* FG: we do not generate .moo when dumping .mma files *)
GrafiteMarshal.save_moo moo_fname moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
- NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
grafite_status#dump
end;
let tm = Unix.gmtime elapsed in