~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 ();
sequents_viewer#goto_sequent goal
with Failure _ -> script#setGoal None);
| Proof proof -> sequents_viewer#load_logo_with_qed
- | No_proof -> sequents_viewer#load_logo
+ | No_proof ->
+ (match grafite_status.ng_status with
+ ProofMode nstatus ->
+ sequents_viewer#nload_sequents nstatus;
+ (try
+ script#setGoal (Some (Continuationals.Stack.find_goal nstatus.NTacStatus.gstatus));
+ let goal =
+ match script#goal with
+ None -> assert false
+ | Some n -> n
+ in
+ sequents_viewer#goto_sequent goal
+ with Failure _ -> script#setGoal None);
+ | CommandMode _ -> sequents_viewer#load_logo
+ )
| Intermediate _ -> assert false (* only the engine may be in this state *)
in
script#addObserver sequents_observer;
let addDebugSeparator () =
ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
in
+ addDebugItem "dump aliases" (fun _ ->
+ let status = script#lexicon_status in
+ LexiconEngine.dump_aliases HLog.debug "" 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) [])));
+*)
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 _ ->
prerr_endline
- (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative ""
+ (ApplyTransformation.txt_of_cic_object 120 []
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
(match
| 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 }}} *)