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;
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"
- (DisambiguateTypes.Environment.fold
- (fun _ x l -> (LexiconAstPp.pp_alias x)::l)
- status.LexiconEngine.aliases [])));
+ (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));
~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 }}} *)