- addDebugItem "dump environment to \"env.dump\"" (fun _ ->
- let oc = open_out "env.dump" in
- CicEnvironment.dump_to_channel oc;
- close_out oc);
- addDebugItem "load environment from \"env.dump\"" (fun _ ->
- let ic = open_in "env.dump" in
- CicEnvironment.restore_from_channel ic;
- close_in ic);
- addDebugItem "dump universes" (fun _ ->
- List.iter (fun (u,_,g) ->
- prerr_endline (UriManager.string_of_uri u);
- CicUniv.print_ugraph g) (CicEnvironment.list_obj ())
- );
- addDebugItem "dump environment content" (fun _ ->
- List.iter (fun (u,_,_) ->
- prerr_endline (UriManager.string_of_uri u))
- (CicEnvironment.list_obj ()));
- addDebugItem "dump script status" script#dump;
- addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
- Helm_registry.save_to "./foo.conf.xml");
- addDebugItem "dump metasenv"
- (fun _ ->
- if script#onGoingProof () then
- HLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
- addDebugItem "print top-level grammar entries"
- CicNotationParser.print_l2_pattern;
- addDebugItem "dump moo to stderr" (fun _ ->
- let grafite_status = (MatitaScript.current ())#grafite_status in
- let moo = grafite_status.moo_content_rev in
- List.iter
- (fun cmd ->
- prerr_endline
- (GrafiteAstPp.pp_command
- ~term_pp:(fun _ -> assert false)
- ~obj_pp:(fun _ -> assert false)
- cmd))
- (List.rev moo));
+ addDebugItem "dump aliases" (fun _ ->
+ let status = script#grafite_status in
+ LexiconEngine.dump_aliases prerr_endline "" status);
+(* FG: DEBUGGING
+ addDebugItem "dump interpretations" (fun _ ->
+ let status = script#lexicon_status in
+ let filter =
+ List.filter (function LexiconAst.Interpretation _ -> true | _ -> false)
+ in
+ HLog.debug (String.concat "\n"
+ (List.fold_right
+ (fun x l -> (LexiconAstPp.pp_command x)::l)
+ (filter status.LexiconEngine.lexicon_content_rev) [])));
+*)