let addDebugSeparator () =
ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
in
+ addDebugItem "dump aliases" (fun _ ->
+ let status = script#lexicon_status in
+ HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases));
addDebugItem "dump environment to \"env.dump\"" (fun _ ->
let oc = open_out "env.dump" in
CicEnvironment.dump_to_channel oc;
(MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
with
| GrafiteTypes.No_proof -> (Cic.Implicit None)
- | Incomplete_proof i -> let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p
- | Proof p -> let _,_,_subst,p,_, _ = p in p
+ | Incomplete_proof i ->
+ let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in
+ Lazy.force p
+ | Proof p -> let _,_,_subst,p,_, _ = p in Lazy.force p
| Intermediate _ -> assert false)));
addDebugItem "Print current proof (natural language) to stderr"
(fun _ ->
| GrafiteTypes.No_proof -> assert false
| Incomplete_proof i ->
let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in
- Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
+ Cic.CurrentProof ("current (incomplete) proof",m,Lazy.force p,ty,[],attrs)
| Proof (_,m,_subst,p,ty, attrs) ->
- Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
+ Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs)
| Intermediate _ -> assert false)));
(* addDebugItem "ask record choice"
(fun _ ->
*)
addDebugSeparator ();
addDebugItem "enable multiple disambiguation passes (default)"
- (fun _ -> GrafiteDisambiguator.only_one_pass := false);
+ (fun _ -> MultiPassDisambiguator.only_one_pass := false);
addDebugItem "enable only one disambiguation pass"
- (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+ (fun _ -> MultiPassDisambiguator.only_one_pass := true);
addDebugItem "always show all disambiguation errors"
(fun _ -> MatitaGui.all_disambiguation_passes := true);
addDebugItem "prune disambiguation errors"