~parent:gui#main#toplevel ())
()
in
+ Predefined_virtuals.load_predefined_virtuals ();
+ Predefined_virtuals.load_predefined_classes ();
gui#sourceView#source_buffer#begin_not_undoable_action ();
s#reset ();
s#template ();
in
addDebugItem "dump aliases" (fun _ ->
let status = script#lexicon_status in
- HLog.debug (DisambiguatePp.pp_environment status.LexiconEngine.aliases));
+ HLog.debug (String.concat "\n"
+ (DisambiguateTypes.Environment.fold
+ (fun _ x l -> (LexiconAstPp.pp_alias x)::l)
+ status.LexiconEngine.aliases [])));
addDebugItem "dump environment to \"env.dump\"" (fun _ ->
let oc = open_out "env.dump" in
CicEnvironment.dump_to_channel oc;
(fun cmd ->
prerr_endline
(GrafiteAstPp.pp_command
- ~term_pp:(fun _ -> assert false)
+ ~term_pp:(fun t -> CicPp.ppterm t)
~obj_pp:(fun _ -> assert false)
cmd))
(List.rev moo));
(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"
~doc:(HExtlib.unopt (mview ())#get_document) ~name:"matita.xml" ())); *)
addDebugItem "load (sequent) MathML from matita.xml"
(fun _ -> (mview ())#load_uri ~filename:"matita.xml");
- addDebugItem "autoWin"
- (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
+ addDebugSeparator ();
+ addDebugItem "Expand virtuals"
+ (fun _ -> (MatitaScript.current ())#expandAllVirtuals);
end
(** Debugging }}} *)