* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open Printf
open GrafiteTypes
class clickableMathView obj =
let text_width = 80 in
-let dummy_loc = DisambiguateTypes.dummy_floc in
object (self)
inherit GMathViewAux.multi_selection_math_view obj
let reduction_action kind () =
let pat = self#tactic_text_pattern_of_selection in
let statement =
- let loc = DisambiguateTypes.dummy_floc in
+ let loc = HExtlib.dummy_floc in
"\n" ^
GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
(Some (Some unsh_sequent,
ids_to_terms, ids_to_hypotheses, ids_to_father_ids,
Hashtbl.create 1, None));
- let name = "sequent_viewer.xml" in
- HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
- ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
+ if BuildTimeConf.debug then begin
+ let name = "sequent_viewer.xml" in
+ HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+ ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
+ end;
self#load_root ~root:mathml#get_documentElement
method load_object obj =
XmlDiff.update_dom ~from:current_mathml mathml;
self#thaw
| _ ->
- let name = "cic_browser.xml" in
- HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
- ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
+ if BuildTimeConf.debug then begin
+ let name = "cic_browser.xml" in
+ HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+ ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
+ end;
self#load_root ~root:mathml#get_documentElement;
current_mathml <- Some mathml);
end
goal2page <- [];
goal2win <- [];
_metasenv <- [];
- self#script#setGoal ~-1;
+ self#script#setGoal None
method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
_metasenv <- metasenv;
let goal_switch =
try List.assoc page page2goal with Not_found -> assert false
in
- self#script#setGoal (goal_of_switch goal_switch);
+ self#script#setGoal (Some (goal_of_switch goal_switch));
self#render_page ~page ~goal_switch))
method private render_page ~page ~goal_switch =
method private home () =
self#_showMath;
- match self#script#status.proof_status with
+ match self#script#grafite_status.proof_status with
| Proof (uri, metasenv, bo, ty) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in